mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix bug reported by Nuno

Browse source 
qhead should not be changed after tactic execution. It should remain 0 so the same tactic can be applied repeatedly on the entire state
This commit is contained in:
Nikolaj Bjorner 2022-12-09 07:56:51 -08:00
parent a96f5a9b42
commit 96a2c04026
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/dependent_expr_state_tactic.h
View file

@ -110,8 +110,6 @@ public:
try { try {
if (!in->proofs_enabled() || m_simp->supports_proofs()) if (!in->proofs_enabled() || m_simp->supports_proofs())
m_simp->reduce(); m_simp->reduce();
if (m.inc())
advance_qhead();
} }
catch (rewriter_exception& ex) { catch (rewriter_exception& ex) {
throw tactic_exception(ex.msg()); throw tactic_exception(ex.msg());