From e26f7b900cdd81103bfc1846f40aa54c8e169a69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Sep 2025 19:23:55 +0300 Subject: [PATCH] fix unsound axiom for lower-bounding --- src/smt/theory_lra.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0325413f4..2c58400ba 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2640,12 +2640,12 @@ public: if (a.is_band(n)) { - // x&y <= x - // x&y <= y + // 0 <= x => x&y <= x + // 0 <= y => x&y <= y // 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(mk_le(n, y))); + 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(a.mk_ge(y, a.mk_int(0))), mk_literal(a.mk_le(n, y))); } else if (a.is_shl(n)) { // y >= sz => n = 0