From 8ab8b63a4ccc897149036f34011cbe7a9ff2d193 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Jun 2022 12:32:04 -0700 Subject: [PATCH] fix incorrect mod axiomatization #6116 --- src/sat/smt/arith_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 47eb4499d..517efcfe3 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -133,7 +133,7 @@ namespace arith { expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m); literal eqz = mk_literal(m.mk_eq(q, zero)); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); - literal mod_lt_q = mk_literal(a.mk_lt(a.mk_sub(mod, abs_q), mone)); + literal mod_lt_q = mk_literal(a.mk_le(a.mk_sub(mod, abs_q), mone)); // q = 0 or p = (p mod q) + q * (p div q) // q = 0 or (p mod q) >= 0