From f13411d71d839d6fccf7617d4066150b563bae74 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jul 2026 14:15:11 -0700 Subject: [PATCH] Update theory_lra.cpp --- src/smt/theory_lra.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b878d7e231..4999dcd265 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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);