diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp
index d9c387c5a..145ea71f5 100644
--- a/src/ast/simplifiers/card2bv.cpp
+++ b/src/ast/simplifiers/card2bv.cpp
@@ -29,7 +29,7 @@ void card2bv::reduce() {
                         
     expr_ref new_f1(m), new_f2(m);
     proof_ref new_pr(m);
-    for (unsigned idx = 0; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
+    for (unsigned idx = m_qhead; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) {
         auto [f, d] = m_fmls[idx]();
         rw1(f, new_f1);        
         rw2(false, new_f1, new_f2, new_pr);        
@@ -48,6 +48,8 @@ void card2bv::reduce() {
     func_decl_ref_vector const& fns = rw2.fresh_constants();
     for (func_decl* f : fns)
         m_fmls.model_trail().hide(f);    
+
+    advance_qhead(m_fmls.size());
 }
 
 void card2bv::collect_statistics(statistics& st) const {
diff --git a/src/ast/simplifiers/max_bv_sharing.cpp b/src/ast/simplifiers/max_bv_sharing.cpp
index b28b5ebdb..ca11f9a1b 100644
--- a/src/ast/simplifiers/max_bv_sharing.cpp
+++ b/src/ast/simplifiers/max_bv_sharing.cpp
@@ -253,7 +253,7 @@ public:
     void reduce() override {
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        for (unsigned idx = 0; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
+        for (unsigned idx = m_qhead; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) {
             auto [curr, d] = m_fmls[idx]();
             m_rw(curr, new_curr, new_pr);
             // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr);
@@ -261,6 +261,7 @@ public:
             m_fmls.update(idx, dependent_expr(m, new_curr, d));            
         }
         m_rw.cfg().cleanup();
+        advance_qhead(m_fmls.size());
     }        
 };