From d6ad371934ab24ade0cb99fe6c7e85d2bd51196f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 May 2020 16:36:59 -0700 Subject: [PATCH] avoid div/mod axioms on 0 Signed-off-by: Nikolaj Bjorner --- src/smt/seq_regex.cpp | 2 +- src/smt/theory_lra.cpp | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 3f65184c4..44c6187fb 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -93,7 +93,7 @@ namespace smt { if (false && !sk().is_tail(s)) { expr_ref is_empty(m.mk_eq(r, re().mk_empty(m.get_sort(s))), m); rewrite(is_empty); - literal is_emptyl = mk_literal(is_empty); + literal is_emptyl = th.mk_literal(is_empty); if (ctx.get_assignment(is_emptyl) != l_false) { th.propagate_lit(nullptr, 1, &lit, ~is_emptyl); return true; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ee0c05afc..b5595749b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1326,6 +1326,15 @@ public: expr_ref div(a.mk_idiv(p, q), m); expr_ref mod(a.mk_mod(p, q), m); expr_ref zero(a.mk_int(0), m); + if (a.is_zero(p)) { + literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); + literal q_le_0 = mk_literal(a.mk_le(q, zero)); + mk_axiom(~q_ge_0, ~q_le_0, mk_literal(a.mk_ge(div, zero))); + mk_axiom(~q_ge_0, ~q_le_0, mk_literal(a.mk_le(div, zero))); + mk_axiom(~q_ge_0, ~q_le_0, mk_literal(a.mk_ge(mod, zero))); + mk_axiom(~q_ge_0, ~q_le_0, mk_literal(a.mk_le(mod, zero))); + return; + } literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); literal div_ge_0 = mk_literal(a.mk_ge(div, zero));