From cc799bbfc11d2a4279d4d267f1a103133ff2c053 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Tue, 14 May 2024 10:57:25 +0200 Subject: [PATCH] fix sign_extend --- src/sat/smt/polysat_internalize.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp index 8e3c08ce0..082af36d8 100644 --- a/src/sat/smt/polysat_internalize.cpp +++ b/src/sat/smt/polysat_internalize.cpp @@ -635,8 +635,8 @@ namespace polysat { sat::literal lt0 = ctx.mk_literal(bv.mk_slt(arg, bv.mk_numeral(0, arg_sz))); // arg < 0 ==> e = concat(1...1, arg) // arg >= 0 ==> e = concat(0...0, arg) - add_axiom(name, { lt0, eq_internalize(e, bv.mk_concat(bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2), arg)) }); - add_axiom(name, { ~lt0, eq_internalize(e, bv.mk_concat(bv.mk_numeral(0, sz2), arg)) }); + add_axiom(name, { ~lt0, eq_internalize(e, bv.mk_concat(bv.mk_numeral(rational::power_of_two(sz2) - 1, sz2), arg)) }); + add_axiom(name, { lt0, eq_internalize(e, bv.mk_concat(bv.mk_numeral(0, sz2), arg)) }); } }