mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-27 09:22:41 +00:00
Code Activity

Update theory_lra.cpp

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-07-08 14:15:11 -07:00 • committed by GitHub
parent 02a1aec6ca
commit f13411d71d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_lra.cpp
View file

@ -3325,10 +3325,7 @@ public:
lp::lconstraint_kind kT = bound2constraint_kind(v_is_int, bk, true);
lp::lconstraint_kind kF = bound2constraint_kind(v_is_int, bk, false);
if (eps.is_zero())
cT = lp().mk_var_bound(vi, kT, bound);
else
cT = lp().mk_var_bound(vi, kT, bound, eps);
cT = lp().mk_var_bound(vi, kT, bound, eps);
if (v_is_int) {
rational boundF = (bk == lp_api::lower_t) ? bound - 1 : bound + 1;
cF = lp().mk_var_bound(vi, kF, boundF);