From 96a2c0402657d2b836e23428a4c95c3ff8637070 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Dec 2022 07:56:51 -0800 Subject: [PATCH] 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 --- src/tactic/dependent_expr_state_tactic.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index f635acca1ae..58507a850a8 100644 --- 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());