fix bug reported by Nuno

qhead should not be changed after tactic execution. It should remain 0 so the same tactic can be applied repeatedly on the entire state
Z3Prover · Dec 9, 2022 · 96a2c04 · 96a2c04
1 parent a96f5a9
commit 96a2c04
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
@@ -110,8 +110,6 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         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());