about summary refs log tree commit diff homepage
path: root/lib/Solver/MetaSMTBuilder.h
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver/MetaSMTBuilder.h')
-rw-r--r--lib/Solver/MetaSMTBuilder.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h
index ba7ea03b..a166db5a 100644
--- a/lib/Solver/MetaSMTBuilder.h
+++ b/lib/Solver/MetaSMTBuilder.h
@@ -450,7 +450,7 @@ MetaSMTBuilder<SolverContext>::constructSDivByConstant(
   int32_t mprime, dsign, shpost;
   ComputeSDivConstants32(d, mprime, dsign, shpost);
   typename SolverContext::result_type expr_dsign = bvConst32(32, dsign);
-  typename SolverContext::result_type expr_shpost = bvConst32(32, shpost);
+  typename SolverContext::result_type expr_shpost = bvConst32(64, shpost);
 
   // q0 = n + MULSH( mprime, n ) = n + (( (int64_t)mprime * (int64_t)n ) >> 32)
   int64_t mprime_64 = (int64_t)mprime;