mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Update theory_lra.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-08 15:41:08 -08:00
parent 270c127407
commit f9ce41bd2b
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -272,9 +272,8 @@ class theory_lra::imp {
continue;
if (a.is_numeral(x) || a.is_numeral(y))
continue;
if (x == n->get_expr()) {
std::swap(x, y);
}
if (x == n->get_expr())
std::swap(x, y);
if (y != n->get_expr())
continue;
@ -282,7 +281,6 @@ class theory_lra::imp {
continue;
expr_ref k(a.mk_numeral(get_value(v), a.is_int(y)), m);
expr_ref eq(a.mk_eq(y, k), m);
literal eq1 = th.mk_eq(y, k, false);
literal eq2 = th.mk_eq(e, a.mk_mul(x, k), false);
ctx().mk_th_axiom(get_id(), ~eq1, eq2);