mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove not-handled clause from mod with non-numerals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-22 09:46:04 -08:00
parent 49a51a0757
commit f9195c77a7
1 changed files with 0 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_lra.cpp
View file

@ -483,22 +483,6 @@ class theory_lra::imp {
if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod);
} }
else if (a.is_mod(n, n1, n2)) { else if (a.is_mod(n, n1, n2)) {
bool is_num = a.is_numeral(n2, r) && !r.is_zero();
if (!is_num) {
found_not_handled(n);
}
#if 0
else {
app_ref div(a.mk_idiv(n1, n2), m);
mk_enode(div);
theory_var w = mk_var(div);
theory_var u = mk_var(n1);
// add axioms:
// u = v + r*w
// abs(r) > v >= 0
assert_idiv_mod_axioms(u, v, w, r);
}
#endif
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)) { else if (a.is_rem(n, n1, n2)) {