use monomial variable, not the fixed variable

Z3Prover · Jan 14, 2025 · 89ed4d6 · 89ed4d6
1 parent a08a3ee
commit 89ed4d6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
@@ -69,7 +69,7 @@ namespace nla {
         }
         vector<std::pair<lp::mpq, lpvar>> coeffs;
         coeffs.push_back({coeff, free_var});
-        coeffs.push_back({mpq(-1), v});
+        coeffs.push_back({mpq(-1), m.var()});
         lpvar j = lra.add_term(coeffs, UINT_MAX);
         lra.update_column_type_and_bound(j, llc::EQ, mpq(0), d);
     }