merge changes from master

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/math/lp/lar_solver.cpp

@@ -1077,12 +1077,14 @@ namespace lp {
     bool lar_solver::init_model() const {
         CTRACE("lar_solver_model",!m_columns_with_changed_bounds.empty(), tout << "non-empty changed bounds\n");
         TRACE("lar_solver_model", tout << get_status() << "\n");
-        if (get_status() != lp_status::OPTIMAL && get_status() != lp_status::FEASIBLE)
+        auto status = get_status();
+        SASSERT((status != lp_status::OPTIMAL && status != lp_status::FEASIBLE) 
+            || m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
+        if (status != lp_status::OPTIMAL && status != lp_status::FEASIBLE)
             return false;
         if (!m_columns_with_changed_bounds.empty())
             return false;
 
-        lp_assert(m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis());
         m_delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1));
         unsigned j;
         unsigned n = m_mpq_lar_core_solver.m_r_x.size();

src/smt/theory_lra.cpp

@@ -2115,6 +2115,9 @@ class theory_lra::imp {
         flush_bound_axioms();
         // disabled in master:
         propagate_nla(); 
+        if (ctx().inconsistent())
+            return true;
+
         if (!can_propagate_core()) 
             return false;
 
@@ -2212,6 +2215,9 @@ class theory_lra::imp {
     }
 
     void propagate_bounds_with_lp_solver() {
+        if (!should_propagate()) 
+            return;
+
         m_bp.init();
         lp().propagate_bounds_for_touched_rows(m_bp);
 
@@ -3546,7 +3552,6 @@ class theory_lra::imp {
         if (r == l_true) {
             nctx.display_asserted_formulas(std::cout);
             std::cout.flush();
-            std::cout.flush();
         }
         return l_true != r;
     }

src/smt/theory_user_propagator.cpp

@@ -62,8 +62,7 @@ void theory_user_propagator::add_expr(expr* term, bool ensure_enode) {
     enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e);
     if (is_attached_to_var(n))
         return;
-
-
+
     theory_var v = mk_var(n);
     m_var2expr.reserve(v + 1);
     m_var2expr[v] = term;
@@ -146,7 +145,7 @@ final_check_status theory_user_propagator::final_check_eh() {
         return FC_DONE;
     force_push();
     unsigned sz1 = m_prop.size();
-    unsigned sz2 = m_expr2var.size();
+    unsigned sz2 = get_num_vars();
     try {
         m_final_eh(m_user_context, this);
     }
@@ -157,7 +156,7 @@ final_check_status theory_user_propagator::final_check_eh() {
     propagate();
     CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n");
     // check if it became inconsistent or something new was propagated/registered
-    bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
+    bool done = (sz1 == m_prop.size()) && (sz2 == get_num_vars()) && !ctx.inconsistent();
     return done ? FC_DONE : FC_CONTINUE;
 }
 

src/solver/simplifier_solver.cpp

@@ -24,6 +24,7 @@ Module Name:
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/simplifiers/dependent_expr_state.h"
 #include "ast/simplifiers/then_simplifier.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "solver/solver.h"
 #include "solver/simplifier_solver.h"
 #include "solver/solver_preprocess.h"
@@ -62,7 +63,16 @@ class simplifier_solver : public solver {
             if (s.m.is_false(f))
                 s.set_inconsistent();
         }        
-        void replay(unsigned qhead, expr_ref_vector& assumptions) { m_reconstruction_trail.replay(qhead, assumptions, *this); }
+        void replay(unsigned qhead, expr_ref_vector& assumptions) {
+            m_reconstruction_trail.replay(qhead, assumptions, *this);
+            th_rewriter rw(s.m);
+            expr_ref tmp(s.m);
+            for (unsigned i = 0; i < assumptions.size(); ++i) {
+                tmp = assumptions.get(i);
+                rw(tmp);
+                assumptions[i] = tmp;
+            }                    
+        }
         void flatten_suffix() override {
             expr_mark seen;
             unsigned j = qhead();
@@ -109,15 +119,16 @@ class simplifier_solver : public solver {
         unsigned qhead = m_preprocess_state.qhead();
         expr_ref_vector orig_assumptions(assumptions);
         m_core_replace.reset();
-        if (qhead < m_fmls.size() || !assumptions.empty()) {
-            m_preprocess_state.replay(qhead, assumptions);   
-            m_preprocess_state.freeze(assumptions);
+        if (qhead < m_fmls.size()) {
             m_preprocess.reduce();
             if (!m.inc())
                 return;
             TRACE("solver", tout << "qhead " << qhead << "\n";
                   m_preprocess_state.display(tout));
             m_preprocess_state.advance_qhead();
+        }
+        if (!assumptions.empty()) {
+            m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions);   
             for (unsigned i = 0; i < assumptions.size(); ++i) 
                 m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));            
         }
@@ -203,6 +214,7 @@ class simplifier_solver : public solver {
     lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override { 
         expr_ref_vector _assumptions(m, num_assumptions, assumptions);
         flush(_assumptions);
+        TRACE("simplifier", tout << _assumptions);
         return s->check_sat_core(num_assumptions, _assumptions.data()); 
     }