force int bound on int columns, call term_is_int() after subst

Signed-off-by: Lev Nachmanson <[email protected]>

Author: levnach

src/math/lp/lar_solver.cpp

@@ -1641,12 +1641,12 @@ namespace lp {
     var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i) {
         TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
         SASSERT(!m_var_register.external_is_used(ext_i));
-        m_term_register.add_var(ext_i, term_is_int(coeffs));
-        lp_assert(all_vars_are_registered(coeffs));
-        if (strategy_is_undecided())
-            return add_term_undecided(coeffs);
+        SASSERT(all_vars_are_registered(coeffs));
         lar_term* t = new lar_term(coeffs);
         subst_known_terms(t);
+        m_term_register.add_var(ext_i, term_is_int(t));
+        if (strategy_is_undecided())
+            return add_term_undecided(coeffs);
         push_term(t);
         SASSERT(m_terms.size() == m_term_register.size());
         unsigned adjusted_term_index = m_terms.size() - 1;
@@ -1938,10 +1938,11 @@ namespace lp {
                     tout << std::endl;
                 }
             });
+        mpq rs = adjust_bound_for_int(j, kind, right_side);
         if (column_has_upper_bound(j))
-            update_column_type_and_bound_with_ub(j, kind, right_side, dep);
+            update_column_type_and_bound_with_ub(j, kind, rs, dep);
         else
-            update_column_type_and_bound_with_no_ub(j, kind, right_side, dep);
+            update_column_type_and_bound_with_no_ub(j, kind, rs, dep);
 
         if (is_base(j) && column_is_fixed(j))
             m_fixed_base_var_set.insert(j);