diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 8dc892f9d..a6072df0e 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -606,7 +606,7 @@ void asserted_formulas::propagate_values() {
     proof_ref_vector new_prs2(m_manager);
     unsigned sz = m_asserted_formulas.size();
     for (unsigned i = 0; i < sz; i++) {
-        expr * n    = m_asserted_formulas.get(i);
+        expr_ref n(m_asserted_formulas.get(i), m_manager);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
         TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
         if (m_manager.is_eq(n)) {