path fix #3747, this patches incoherent behavior of terms / ival from lar_solver. The variables occurring in terms are mapped to columns and not as original variables/terms. theory_lra has to interact with the column_corresponds_to_term test instead of relying on the terms themselves carrying the relevant information

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/lar_solver.cpp

@@ -192,10 +192,12 @@ void lar_solver::calculate_implied_bounds_for_row(unsigned i, lp_bound_propagato
 }
 
 unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
-    if (tv::is_term(j))
+    if (!tv::is_term(j)) {
-        return j;
+        unsigned ext_var_or_term = m_var_register.local_to_external(j);
-    unsigned ext_var_or_term = m_var_register.local_to_external(j);
+        TRACE("arith", tout << j << " " << ext_var_or_term << "\n";);
-    return !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
+        j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
+    }
+    return j;
 }
 
 unsigned lar_solver::map_term_index_to_column_index(unsigned j) const {
@@ -1689,9 +1691,20 @@ bool lar_solver::term_coeffs_are_ok(const vector<std::pair<mpq, var_index>> & co
 }
 #endif
 void lar_solver::push_term(lar_term* t) {
+    // SASSERT(well_formed(*t));
     m_terms.push_back(t);
 }
 
+bool lar_solver::well_formed(lar_term const& t) const {
+    for (auto const& ti : t) {
+        if (!ti.var().is_term() && 
+            column_corresponds_to_term(ti.var().index())) {
+            return false;
+        }
+    }
+    return true;
+}
+
 
 // terms
 bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs) {
@@ -2374,10 +2387,11 @@ std::pair<constraint_index, constraint_index> lar_solver::add_equality(lpvar j,
 
     if (tv::is_term(k))
         k = map_term_index_to_column_index(k);
-    
+
     coeffs.push_back(std::make_pair(mpq(1),j));
     coeffs.push_back(std::make_pair(mpq(-1),k));    
     unsigned term_index = add_term(coeffs, UINT_MAX); // UINT_MAX is the external null var
+
     if (get_column_value(j) != get_column_value(k))
         set_status(lp_status::UNKNOWN);
 

src/math/lp/lar_solver.h

@@ -147,6 +147,8 @@ public:
 
     bool column_is_fixed(unsigned j) const;
     bool column_is_free(unsigned j) const;
+
+    bool well_formed(lar_term const& t) const;
 public:
 
     // init region

src/math/lp/lp_types.h

@@ -54,3 +54,7 @@ public:
 
 };
 }
+
+inline std::ostream& operator<<(lp::tv const& t, std::ostream& out) {
+    return out << (t.is_term() ? "t":"j") << t.id() << "\n";
+}

src/smt/theory_lra.cpp

@@ -3644,18 +3644,26 @@ public:
     }
 
     void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
+        TRACE("arith", lp().print_term(term, tout) << "\n";);
         for (const auto & ti : term) {
             theory_var w;
             if (ti.var().is_term()) {
-                //w = m_term_index2theory_var.get(lp::tv::unmask_term(ti.m_key), null_theory_var);
-                //if (w == null_theory_var) // if extracting expressions directly from nested term
                 lp::lar_term const& term1 = lp().get_term(ti.var().index());
                 rational coeff2 = coeff * ti.coeff();
                 term2coeffs(term1, coeffs, coeff2);
                 continue;
             }
+            else if (lp().column_corresponds_to_term(ti.var().index())) {
+                lp::tv t = lp::tv::term(ti.var().index());
+                lp::lar_term const& term1 = lp().get_term(t.index());
+                rational coeff2 = coeff * ti.coeff();
+                term2coeffs(term1, coeffs, coeff2);
+                continue;                
+            }
             else {
                 w = lp().local_to_external(ti.var().index());
+                SASSERT(w >= 0);
+                TRACE("arith", tout << (ti.var().index()) << ": " << w << "\n";);
             }
             rational c0(0);
             coeffs.find(w, c0);