fix #3924

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

src/math/lp/lar_solver.cpp

@@ -194,7 +194,6 @@ 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)) {
         unsigned ext_var_or_term = m_var_register.local_to_external(j);
-        TRACE("arith", tout << j << " " << ext_var_or_term << "\n";);
         j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
     }
     return j;

src/math/lp/lp_types.h

@@ -70,6 +70,8 @@ class tv {
         return strm.str();
     }
 
+    bool is_null() const { return m_index == UINT_MAX; }
+
 };
 
 class column_index {

src/sat/sat_config.cpp

@@ -244,7 +244,7 @@ namespace sat {
             throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected");
 
         m_card_solver = p.cardinality_solver();
-        m_xor_solver = p.xor_solver();
+        m_xor_solver = false && p.xor_solver(); // hide this option until thoroughly tested
 
         sat_simplifier_params sp(_p);
         m_elim_vars = sp.elim_vars();

src/smt/theory_dense_diff_logic_def.h

@@ -210,7 +210,7 @@ namespace smt {
     }
 
     template<typename Ext>
-    bool theory_dense_diff_logic<Ext>::internalize_term(app * term) {
+    bool theory_dense_diff_logic<Ext>::internalize_term(app * term) {        
         if (memory::above_high_watermark()) {
             found_non_diff_logic_expr(term); // little hack... TODO: change to no_memory and return l_undef if SAT
             return false;
@@ -225,6 +225,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_dense_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
+        TRACE("ddl", tout << "eq-eh: " << mk_pp(atom, get_manager()) << "\n";);
         if (memory::above_high_watermark())
             return;
         context & ctx  = get_context();
@@ -243,8 +244,10 @@ namespace smt {
             enode * n1 = ctx.get_enode(lhs);
             enode * n2 = ctx.get_enode(rhs);
             if (n1->get_th_var(get_id()) != null_theory_var &&
-                n2->get_th_var(get_id()) != null_theory_var)
-                m_arith_eq_adapter.mk_axioms(n1, n2);
+                n2->get_th_var(get_id()) != null_theory_var) {
+                m_arith_eq_adapter.mk_axioms(n1, n2); 
+                return;
+            }
         }
     }
 

src/smt/theory_lra.cpp

@@ -789,10 +789,6 @@ class theory_lra::imp {
         return v;
     }
 
-    bool theory_var_is_registered_in_lar_solver(theory_var v) const {
-        return lp().external_is_used(v);
-    }
-
     bool const has_int() const { return lp().has_int_var(); }
 
     lpvar register_theory_var_in_lar_solver(theory_var v) {
@@ -957,9 +953,7 @@ class theory_lra::imp {
 
     theory_var internalize_linearized_def(app* term, scoped_internalize_state& st) {
         theory_var v = mk_var(term);
-        TRACE("arith", 
-              tout << mk_bounded_pp(term, m) << " v" << v << "\n";
-              tout << st.offset() << " " << st.coeffs().size() << " " << st.coeffs()[0] << "\n";);
+        TRACE("arith", tout << mk_bounded_pp(term, m) << " v" << v << "\n";);
 
         if (is_unit_var(st) && v == st.vars()[0]) {
             return st.vars()[0];
@@ -1510,6 +1504,12 @@ class theory_lra::imp {
         return can_get_bound(v);
     }
 
+    void ensure_column(theory_var v) {
+        if (!lp().external_is_used(v)) {
+            register_theory_var_in_lar_solver(v);
+        }
+    }
+
     mutable vector<std::pair<lp::tv, rational>> m_todo_terms;
 
     lp::impq get_ivalue(theory_var v) const {
@@ -1596,16 +1596,13 @@ class theory_lra::imp {
         svector<lpvar> vars;
         theory_var sz = static_cast<theory_var>(th.get_num_vars());
         for (theory_var v = 0; v < sz; ++v) {
-            if (!can_get_ivalue(v)) {
-                continue;
-            }
             enode * n1 = get_enode(v);
             if (!th.is_relevant_and_shared(n1)) {
                 continue;
             }
+            ensure_column(v);
             lp::column_index vj = lp().to_column_index(v);
-            if (vj.is_null()) 
-                continue;
+            SASSERT(!vj.is_null());
             theory_var other = m_model_eqs.insert_if_not_there(v);
             if (other == v) {
                 continue;
@@ -3830,7 +3827,7 @@ class theory_lra::imp {
             auto t = get_tv(v);
             if (!ctx().is_relevant(get_enode(v))) out << "irr: ";
             out << "v" << v << " ";
-            out << (t.is_term() ? "t":"j") << t.id();
+            if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << t.id();
             if (can_get_value(v)) out << " = " << get_value(v); 
             if (is_int(v)) out << ", int";
             if (ctx().is_shared(get_enode(v))) out << ", shared";