diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index f635acca1..58507a850 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -110,8 +110,6 @@ public:
         try {
             if (!in->proofs_enabled() || m_simp->supports_proofs())
                 m_simp->reduce();
-            if (m.inc())
-                advance_qhead();
         }
         catch (rewriter_exception& ex) {
             throw tactic_exception(ex.msg());