mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix #5136, regression when removing variable registration for mod/div operations

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-30 13:45:54 -07:00
parent c629f09f21
commit c71bbb6391
2 changed files with 10 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/arith_decl_plugin.h
View file

@ -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);

8
src/smt/theory_lra.cpp
View file

@ -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 {