diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index b28a0ea5f..597ecf4e4 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -83,6 +83,8 @@ protected:
 
 
     void reduce(goal& g) {
+        if (m.proofs_enabled())
+            return;
         TRACE("ctx_solver_simplify_tactic", g.display(tout););
         expr_ref fml(m);
         tactic_report report("ctx-solver-simplify", g);
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 8a2e3dca9..90ca58980 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -21,6 +21,7 @@ Revision History:
 #include "tactic/core/propagate_values_tactic.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "ast/expr_substitution.h"
 #include "tactic/goal_shared_occs.h"
 #include "tactic/tactic_params.hpp"
@@ -52,18 +53,20 @@ class propagate_values_tactic : public tactic {
         return is_shared(atom);
     }
 
-    bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
+    bool is_shared_eq(expr * t, expr * & lhs, expr * & value, bool& inverted) {
         expr* arg1, *arg2;
         if (!m.is_eq(t, arg1, arg2))
             return false;
         if (m.is_value(arg1) && is_shared(arg2)) {
             lhs   = arg2;
             value = arg1;
+            inverted = false;
             return true;
         }
         if (m.is_value(arg2) && is_shared(arg1)) {
             lhs   = arg1;
             value = arg2;
+            inverted = true;
             return true;
         }
         return false;
@@ -71,7 +74,7 @@ class propagate_values_tactic : public tactic {
 
     void push_result(expr * new_curr, proof * new_pr) {
         if (m_goal->proofs_enabled()) {
-            proof * pr = m_goal->pr(m_idx);
+            proof * pr = m_goal->pr(m_idx);            
             new_pr     = m.mk_modus_ponens(pr, new_pr);
         }
         
@@ -95,8 +98,10 @@ class propagate_values_tactic : public tactic {
             m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d);
         }
         expr * lhs, * value;
-        if (is_shared_eq(new_curr, lhs, value)) {
-            TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";);
+        bool inverted = false;
+        if (is_shared_eq(new_curr, lhs, value, inverted)) {
+            TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n" << mk_ismt2_pp(new_pr, m) << "\n";);
+            if (inverted && new_pr) new_pr = m.mk_symmetry(new_pr);
             m_subst->insert(lhs, value, new_pr, new_d);
         }
     }
@@ -105,6 +110,7 @@ class propagate_values_tactic : public tactic {
         expr * curr = m_goal->form(m_idx);
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
+        std::cout << m_goal->pr(m_idx) << "\n";
         
         if (!m_subst->empty()) {
             m_r(curr, new_curr, new_pr);
@@ -115,7 +121,7 @@ class propagate_values_tactic : public tactic {
                 new_pr   = m.mk_reflexivity(curr);
         }
 
-        TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
+        TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << new_curr << "\n" << new_pr << "\n";);
         if (new_curr != curr) {
             m_modified = true;
         }
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 57ae78d75..e7e4e3b8e 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -115,6 +115,7 @@ void goal::copy_to(goal & target) const {
 }
 
 void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(!m().proofs_enabled() || pr);
     if (m().is_true(f))
         return;
     if (m().is_false(f)) {
@@ -252,6 +253,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
     if (m_inconsistent) {
         return;
     }
+    SASSERT(!m().proofs_enabled() || pr);
     if (pr) {
         SASSERT(f == m().get_fact(pr));
         slow_process(f, pr, d);
@@ -301,6 +303,7 @@ void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
         }
     }
     else {
+        SASSERT(!m().proofs_enabled());
         expr_ref fr(f, m());
         quick_process(true, fr, d);
         if (!m_inconsistent) {