partial fix to make computed term integer well-formed for solve_for f…

…unctionality
Z3Prover · Dec 6, 2024 · 1ab0962 · 1ab0962
1 parent bcb61ee
commit 1ab0962
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
@@ -619,13 +619,15 @@ namespace lp {
 
     bool lar_solver::solve_for(unsigned j, lar_term& t, mpq& coeff) {
         t.clear();        
+        IF_VERBOSE(10, verbose_stream() << column_is_fixed(j) << " " << is_base(j) << "\n");
         if (column_is_fixed(j)) {
             coeff = get_value(j);
             return true;
         }
         if (!is_base(j)) {
             for (const auto & c : A_r().m_columns[j]) {
                 lpvar basic_in_row = r_basis()[c.var()];
+                IF_VERBOSE(10, verbose_stream() << "c.var() = " << c.var() << " basic_in_row = " << basic_in_row << "\n");
                 pivot(j, basic_in_row);
                 break;
             }

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -3638,9 +3638,21 @@ class theory_lra::imp {
         rational coeff;
         if (!lp().solve_for(vi, t, coeff))
             return false;
+        rational lc(1);
+        if (is_int(v)) {
+            lc = denominator(coeff);
+            for (auto const& cv : t)
+                lc = lcm(denominator(cv.coeff()), lc);
+            if (lc != 1) {
+                coeff *= lc;
+                t *= lc;
+            }
+        }
         term = mk_term(t, is_int(v));
         if (coeff != 0)
             term = a.mk_add(a.mk_numeral(coeff, is_int(v)), term);
+        if (lc != 1)
+            term = a.mk_idiv(term, a.mk_numeral(lc, true));
         return true;
     }