mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-21 10:41:35 +00:00
Code Activity

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-03 12:02:57 -07:00
parent 20a259cfaa
commit c4158ebc33
1 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/arith_internalize.cpp
View file

@ -336,21 +336,18 @@ namespace arith {
} }
else if (a.is_le(atom, n1, n2)) { else if (a.is_le(atom, n1, n2)) {
expr_ref n3(a.mk_sub(n1, n2), m); expr_ref n3(a.mk_sub(n1, n2), m);
rewrite(n3);
v = internalize_def(n3); v = internalize_def(n3);
k = lp_api::upper_t; k = lp_api::upper_t;
r = 0; r = 0;
} }
else if (a.is_ge(atom, n1, n2)) { else if (a.is_ge(atom, n1, n2)) {
expr_ref n3(a.mk_sub(n1, n2), m); expr_ref n3(a.mk_sub(n1, n2), m);
rewrite(n3);
v = internalize_def(n3); v = internalize_def(n3);
k = lp_api::lower_t; k = lp_api::lower_t;
r = 0; r = 0;
} }
else if (a.is_lt(atom, n1, n2)) { else if (a.is_lt(atom, n1, n2)) {
expr_ref n3(a.mk_sub(n1, n2), m); expr_ref n3(a.mk_sub(n1, n2), m);
rewrite(n3);
v = internalize_def(n3); v = internalize_def(n3);
k = lp_api::lower_t; k = lp_api::lower_t;
r = 0; r = 0;
@ -358,7 +355,6 @@ namespace arith {
} }
else if (a.is_gt(atom, n1, n2)) { else if (a.is_gt(atom, n1, n2)) {
expr_ref n3(a.mk_sub(n1, n2), m); expr_ref n3(a.mk_sub(n1, n2), m);
rewrite(n3);
v = internalize_def(n3); v = internalize_def(n3);
k = lp_api::upper_t; k = lp_api::upper_t;
r = 0; r = 0;