cosmetic changes

Z3Prover · Oct 8, 2023 · 1ba0f5a · 1ba0f5a
1 parent 3aac528
commit 1ba0f5a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
@@ -447,7 +447,7 @@ namespace lp {
 
         case column_type::lower_bound: {
             const auto& l = lcs.m_r_lower_bounds()[j];
-            if (val != lcs.m_r_lower_bounds()[j]) {
+            if (val != l) {
                 set_value_for_nbasic_column(j, l);
                 return true;
             }

diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
@@ -370,7 +370,7 @@ namespace nla {
     rational monomial_bounds::fixed_var_product(monic const& m) {
         rational r(1);
         for (lpvar v : m) {
-            //  we have to use the column bounds here, because the value of the column value may be outside the bounds
+            //  we have to use the column bounds here, because the column value may be outside the bounds
             if (c().var_is_fixed(v))
                 r *= c().lra.get_lower_bound(v).x;            
         }