diff options
| -rw-r--r-- | lib/Solver/MetaSMTBuilder.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index a166db5a..ad26f2ed 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -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); |