diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 1890acaae..31dda24ad 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-    // track_id(n, 70);
+    //track_id(n, 1354);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
@@ -1920,19 +1920,6 @@ ast * ast_manager::register_node_core(ast * n) {
         break;
     }
 
-#if 0
-    // std::cout << n->m_id << " " << n->hash() << "\n";
-    if (n->m_id == 1523) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-    }
-    if (n->m_id == 1524) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-        VERIFY(false);
-    }
-    if (n->m_id == 1525) {
-        std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n";
-    }
-#endif
     return n;
 }
 
diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index d53b14840..a3d37171d 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -66,6 +66,8 @@ std::ostream& expr_substitution::display(std::ostream& out) {
 
 void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
     obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, nullptr); 
+    SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(0) == c);
+    SASSERT(!def_pr || to_app(m_manager.get_fact(def_pr))->get_arg(1) == def);
     if (entry->get_data().m_value == nullptr) {
         // new entry
         m_manager.inc_ref(c);
diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp
index 7e646871c..551e59e0e 100644
--- a/src/ast/rewriter/rewriter.cpp
+++ b/src/ast/rewriter/rewriter.cpp
@@ -42,6 +42,16 @@ void rewriter_core::del_cache_stack() {
     }
 }
 
+bool rewriter_core::rewrites_from(expr* t, proof* p) {
+    return !p || (to_app(m().get_fact(p))->get_arg(0) == t);
+}
+
+bool rewriter_core::rewrites_to(expr* t, proof* p) {
+    return !p || (to_app(m().get_fact(p))->get_arg(1) == t); 
+}
+
+
+
 void rewriter_core::cache_shifted_result(expr * k, unsigned offset, expr * v) {
 #if 0
     // trace for tracking cache usage
diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h
index 6895f7218..952a081c6 100644
--- a/src/ast/rewriter/rewriter.h
+++ b/src/ast/rewriter/rewriter.h
@@ -87,6 +87,8 @@ protected:
         push_frame_core(t, must_cache(t), st);
     } 
 
+    bool rewrites_to(expr* t, proof* p);
+    bool rewrites_from(expr* t, proof* p);
     void init_cache_stack();
     void del_cache_stack();
     void reset_cache();
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index f228a216b..bb46e1d39 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -100,6 +100,8 @@ bool rewriter_tpl<Config>::process_const(app * t0) {
     case BR_DONE:
         result_stack().push_back(m_r.get());
         if (ProofGen) {
+            SASSERT(rewrites_from(t0, m_pr));
+            SASSERT(rewrites_to(m_r, m_pr));
             if (m_pr)
                 result_pr_stack().push_back(m_pr);
             else
@@ -139,6 +141,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
         SASSERT(m().get_sort(t) == m().get_sort(new_t));
         result_stack().push_back(new_t);
         set_new_child_flag(t, new_t);
+        SASSERT(rewrites_from(t, new_t_pr));
+        SASSERT(rewrites_to(new_t, new_t_pr));
         if (ProofGen)
             result_pr_stack().push_back(new_t_pr);
         return true;
@@ -167,6 +171,8 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
             if (ProofGen) {
                 proof * pr = get_cached_pr(t);
                 result_pr_stack().push_back(pr);
+                SASSERT(rewrites_from(t, pr));
+                SASSERT(rewrites_to(r, pr));
             }
             return true;
         }
@@ -286,14 +292,20 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             else {
                 new_t = m().mk_app(f, new_num_args, new_args);
                 m_pr  = m().mk_congruence(t, new_t, num_prs, result_pr_stack().c_ptr() + fr.m_spos);
+                SASSERT(rewrites_from(t, m_pr));
+                SASSERT(rewrites_to(new_t, m_pr));
             }
         }
         br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);       
+        
         CTRACE("reduce_app", st != BR_FAILED,
-              tout << mk_bounded_pp(t, m()) << "\n";
-              tout << "st: " << st;
-              if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
-              tout << "\n";);
+               tout << mk_bounded_pp(t, m()) << "\n";
+               tout << "st: " << st;
+               if (m_r) tout << " --->\n" << mk_bounded_pp(m_r, m());
+               tout << "\n";
+               if (m_pr2) tout << mk_bounded_pp(m_pr2, m()) << "\n";
+              );
+        SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2));
         SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
         if (st != BR_FAILED) {
             result_stack().shrink(fr.m_spos);
@@ -491,6 +503,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
     }
 }
 
+
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 0753312a3..a19c3abf8 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -571,7 +571,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
-    void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+    void log_rewrite_axiom_instantiation(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
         family_id fid = f->get_family_id();
         if (fid == m_b_rw.get_fid()) {
             decl_kind k = f->get_decl_kind();
@@ -587,8 +587,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         app_ref tmp(m());
         tmp = m().mk_app(f, num, args);
         m().trace_stream() << "[inst-discovered] theory-solving " << static_cast<void *>(nullptr) << " " << m().get_family_name(fid) << "# ; #" << tmp->get_id() << "\n";
-        if (m().proofs_enabled())
-            result_pr = m().mk_rewrite(tmp, result);
         tmp = m().mk_eq(tmp, result);
         m().trace_stream() << "[instance] " << static_cast<void *>(nullptr) << " #" << tmp->get_id() << "\n";
 
@@ -618,7 +616,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         br_status st = reduce_app_core(f, num, args, result);
 
         if (st != BR_FAILED && m().has_trace_stream()) {
-            log_rewrite_axiom_instantiation(f, num, args, result, result_pr);
+            log_rewrite_axiom_instantiation(f, num, args, result);
         }
 
         if (st != BR_DONE && st != BR_FAILED) {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index ae66764be..3b84afbf7 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -578,7 +578,7 @@ public:
     }
 
     void subs_term_columns(lar_term& t) {
-        vector<std::pair<unsigned,unsigned>> columns_to_subs;
+        svector<std::pair<unsigned,unsigned>> columns_to_subs;
         for (const auto & m : t) {
             unsigned tj = adjust_column_index_to_term_index(m.var().index());
             if (tj == m.var().index()) continue;
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 66ee46b86..24b971590 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -158,26 +158,28 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = nullptr;
         family_id fid = f->get_family_id();
-        bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
+        bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
         br_status st = BR_FAILED;
-        if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)) {
+        if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
             expr * val = m_model.get_const_interp(f);
+            func_decl* g = nullptr;
             if (val != nullptr) {
                 result = val;
                 st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
                 TRACE("model_evaluator", tout << result << "\n";);
                 return st;
             }
-            else if (m_model_completion && !m_ar.is_as_array(f)) {
+            if (!m_model_completion)
+                return BR_FAILED;
+
+            if (!m_ar.is_as_array(f, g) || g->get_family_id() == null_family_id) {
                 sort * s   = f->get_range();
                 expr * val = m_model.get_some_value(s);
                 m_model.register_decl(f, val);
                 result = val;
                 return BR_DONE;
             }
-            else {
-                return BR_FAILED;
-            }
+            return BR_FAILED;            
         }
 
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 8f3f91888..21642323d 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -374,7 +374,7 @@ namespace opt {
     void context::set_model(model_ref& m) { 
         m_model = m; 
         opt_params optp(m_params);
-        if (optp.dump_models()) {
+        if (optp.dump_models() && m) {
             model_ref md = m->copy();
             fix_model(md);
         }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 6446c9c56..ea827319a 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1729,6 +1729,7 @@ namespace sat {
 
         for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
             literal lit = lits[i];
+            set_external(lit.var());
             SASSERT(is_external(lit.var()));
             add_assumption(lit);
             assign_scoped(lit);
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index a2a7f2a32..1caeede92 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -19,6 +19,7 @@ Notes:
 #include "util/debug.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/ast_util.h"
+#include "ast/ast_ll_pp.h"
 #include "smt/smt_kernel.h"
 #include "smt/params/smt_params.h"
 #include "smt/params/smt_params_helper.hpp"
@@ -249,8 +250,11 @@ public:
                         lcore = m.mk_join(lcore, m.mk_leaf(d));
                     }
                 }
-                if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
+
+                if (m.proofs_enabled() && !pr) pr = m.mk_asserted(m.mk_false()); // bail out
+                if (pr && m.get_fact(pr) != m.mk_false()) pr = m.mk_asserted(m.mk_false()); // could happen in clause_proof mode
                 in->assert_expr(m.mk_false(), pr, lcore);
+                
                 result.push_back(in.get());
                 return;
             }
diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 9be3dd83a..75ec17dd4 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -40,7 +40,9 @@ struct unit_subsumption_tactic : public tactic {
     void cleanup() override {}
 
     void operator()(/* in */  goal_ref const & in, 
-                    /* out */ goal_ref_buffer & result) override {        
+                    /* out */ goal_ref_buffer & result) override {  
+        tactic_report report("unit-subsume-simplify", *in);
+        fail_if_proof_generation("unit-subsume-simplify", in);
         reduce_core(in, result);
     }
 
@@ -75,7 +77,8 @@ struct unit_subsumption_tactic : public tactic {
 
     void assert_clauses(goal_ref const& g) {
         for (unsigned i = 0; i < g->size(); ++i) {
-            m_context.assert_expr(m.mk_iff(new_clause(), g->form(i)));
+            expr_ref fml(m.mk_iff(new_clause(), g->form(i)), m);
+            m_context.assert_expr(fml);
         }
     }
 
@@ -106,7 +109,7 @@ struct unit_subsumption_tactic : public tactic {
     }
 
     void insert_result(goal_ref& result) {        
-        for (auto  d : m_deleted) result->update(d, m.mk_true()); // TBD proof?
+        for (auto  d : m_deleted) result->update(d, m.mk_true()); 
     }
 
     void init(goal_ref const& g) {
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 597adc191..1e1b259fc 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -184,7 +184,7 @@ public:
 
         m_bounds(*g);
 
-        if (m_bounds.inconsistent()) {
+        if (m_bounds.inconsistent() || g->proofs_enabled()) {
             g->inc_depth();
             result.push_back(g.get());
             return;
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index a29a5c595..8ecee4ccf 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -60,13 +60,13 @@ class propagate_values_tactic : public tactic {
         if (m.is_value(arg1) && is_shared(arg2)) {
             lhs   = arg2;
             value = arg1;
-            inverted = false;
+            inverted = true;
             return true;
         }
         if (m.is_value(arg2) && is_shared(arg1)) {
             lhs   = arg1;
             value = arg2;
-            inverted = true;
+            inverted = false;
             return true;
         }
         return false;
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 90c307d8c..812e6797d 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -75,7 +75,7 @@ class quasi_macros_tactic : public tactic {
             for (unsigned i = 0; i < new_forms.size(); i++)
                 g->assert_expr(forms.get(i),
                                produce_proofs ? proofs.get(i) : nullptr,
-                               produce_unsat_cores ? deps.get(i) : nullptr);
+                               produce_unsat_cores ? deps.get(i, nullptr) : nullptr);
 
             generic_model_converter * evmc = alloc(generic_model_converter, mm.get_manager(), "quasi_macros");
             unsigned num = mm.get_num_macros();