From e454ae275c20ce2724f24de7f096f80ee52128a8 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Sun, 19 May 2024 04:01:35 +0200 Subject: [PATCH] intblast: fix translation of sign_ext (#7230) --- src/sat/smt/intblast_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 421966377c0..f91113d591c 100644 --- 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: