mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 13:39:28 +00:00
Code Activity

fix unsound axiom for lower-bounding

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-21 19:23:55 +03:00
parent dcdae5a61c
commit e26f7b900c
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -2640,12 +2640,12 @@ public:
if (a.is_band(n)) { if (a.is_band(n)) {
// x&y <= x // 0 <= x => x&y <= x
// x&y <= y // 0 <= y => x&y <= y
// TODO? x = y => x&y = x // TODO? x = y => x&y = x
ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, x))); ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(x, a.mk_int(0))), mk_literal(a.mk_le(n, x)));
ctx().mk_th_axiom(get_id(), mk_literal(mk_le(n, y))); ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_ge(y, a.mk_int(0))), mk_literal(a.mk_le(n, y)));
} }
else if (a.is_shl(n)) { else if (a.is_shl(n)) {
// y >= sz => n = 0 // y >= sz => n = 0