diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index faf5ce0ef..1acfcdf57 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
     proof_ref_vector new_prs1(m_manager);
     expr_ref_vector  new_exprs2(m_manager);
     proof_ref_vector new_prs2(m_manager);
-    unsigned i  = 0;
+    unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);