diff options
| author | MartinNowack <martin.nowack@gmail.com> | 2016-06-28 15:58:03 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-06-28 15:58:03 +0200 |
| commit | e5a958a8e10fa2f52e071dffc6c77dcc6356f074 (patch) | |
| tree | 7346bcb2e04c40c2b95e7c608e743a890783de34 | |
| parent | a49c6fabebb91718b54489e7c09cb7bddc9795b2 (diff) | |
| parent | 5b893715d020165f69062273741b7db99eb47624 (diff) | |
| download | klee-e5a958a8e10fa2f52e071dffc6c77dcc6356f074.tar.gz | |
Merge pull request #417 from hoangmle/fix_constructSDIvByConstant_metaSMT
Fix #416
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ba7ea03b..ad26f2ed 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; @@ -540,6 +540,9 @@ MetaSMTBuilder<SolverContext>::bvVarLeftShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + typename SolverContext::result_type res = bvZero(width); // construct a big if-then-elif-elif-... with one case per possible shift @@ -566,6 +569,9 @@ MetaSMTBuilder<SolverContext>::bvVarRightShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + typename SolverContext::result_type res = bvZero(width); // construct a big if-then-elif-elif-... with one case per possible shift @@ -593,6 +599,9 @@ MetaSMTBuilder<SolverContext>::bvVarArithRightShift( typename SolverContext::result_type expr, typename SolverContext::result_type shift, unsigned width) { + assert(_solver.get_bv_width(expr) == width); + assert(_solver.get_bv_width(shift) == width); + // get the sign bit to fill with typename SolverContext::result_type signedBool = bvBoolExtract(expr, width - 1); |