mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix incorrect mod axiomatization #6116

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-29 12:32:04 -07:00
parent f6932f9a75
commit 8ab8b63a4c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/arith_axioms.cpp
View file

@ -133,7 +133,7 @@ namespace arith {
expr_ref abs_q(m.mk_ite(a.mk_ge(q, zero), q, a.mk_uminus(q)), m); 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 eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, 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 = (p mod q) + q * (p div q)
// q = 0 or (p mod q) >= 0 // q = 0 or (p mod q) >= 0