intblast: fix translation of sign_ext (#7230)

Z3Prover · May 19, 2024 · e454ae2 · e454ae2
1 parent 18a95d8
commit e454ae2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
@@ -881,10 +881,10 @@ namespace intblast {
             SASSERT(bv.get_bv_size(e) >= bv.get_bv_size(bv_expr));
             unsigned arg_sz = bv.get_bv_size(bv_expr);
             unsigned sz = bv.get_bv_size(e);
-            rational N = rational::power_of_two(sz);
+            // rational N = rational::power_of_two(sz);
             rational M = rational::power_of_two(arg_sz);
             expr* signbit = a.mk_ge(r, a.mk_int(M / 2));
-            r = m.mk_ite(signbit, a.mk_uminus(r), r);
+            r = m.mk_ite(signbit, a.mk_sub(r, a.mk_int(M)), r);
             break;
         }
         case OP_INT2BV: