mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix sign_extend

Browse source
This commit is contained in:
Jakob Rath 2024-05-14 10:57:25 +02:00
parent b640ea775a
commit cc799bbfc1
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat_internalize.cpp
View file

@ -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)) });
}
}