diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index bc5b47f7a..db387bf4c 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -525,6 +525,8 @@ void asserted_formulas::commit(unsigned new_qhead) {
 }
 
 void asserted_formulas::propagate_values() {
+    if (m.proofs_enabled())
+        return;
     flush_cache();
 
     unsigned num_prop = 0;
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 8ecee4ccf..6cf340e57 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -146,6 +146,9 @@ class propagate_values_tactic : public tactic {
         if (m_max_rounds == 0)
             goto end;
 
+        if (m_goal->proofs_enabled())
+            goto end;
+
         m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled());
         m_r.set_substitution(m_subst.get());
         m_occs(*m_goal);