From c71bbb6391e7cfbba704a63350513dc0977ea922 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Mar 2021 13:45:54 -0700 Subject: [PATCH] fix #5136, regression when removing variable registration for mod/div operations --- src/ast/arith_decl_plugin.h | 4 ++++ src/smt/theory_lra.cpp | 8 ++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index a27314f56..444af81b0 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -345,6 +345,10 @@ public: MATCH_BINARY(is_rem); MATCH_BINARY(is_div); MATCH_BINARY(is_idiv); + MATCH_BINARY(is_mod0); + MATCH_BINARY(is_rem0); + MATCH_BINARY(is_div0); + MATCH_BINARY(is_idiv0); MATCH_BINARY(is_power); MATCH_UNARY(is_sin); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 216afc1b9..b64e95ba7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -438,7 +438,7 @@ class theory_lra::imp { } else if (a.is_mod(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); - if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); + if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); } else if (a.is_rem(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n); @@ -450,7 +450,11 @@ class theory_lra::imp { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } - else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) { + if (a.is_idiv0(n, n1, n2) || a.is_mod0(n, n1, n2) || a.is_rem0(n, n1, n2)) { + st.to_ensure_var().push_back(n1); + st.to_ensure_var().push_back(n2); + } + else if (!a.is_div0(n)) { found_unsupported(n); } else {