From 1ab0962d43f97c61e4420425fda035a1ea2ba040 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Dec 2024 17:10:52 -0800
Subject: [PATCH] partial fix to make computed term integer well-formed for
 solve_for functionality

---
 src/math/lp/lar_solver.cpp |  2 ++
 src/smt/theory_lra.cpp     | 12 ++++++++++++
 2 files changed, 14 insertions(+)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 20c6d9f30..90c1e9537 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -619,6 +619,7 @@ 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;
@@ -626,6 +627,7 @@ namespace lp {
         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
index d7df4ea22..7a73905b7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3638,9 +3638,21 @@ public:
         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;
     }