From c230d89a3a6c1cf4ad657ee5a1a6a4c087926686 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 May 2021 09:59:50 -0700 Subject: [PATCH] fix #5294 Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/recover_01_tactic.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index a50e6fef3..bbc8aa007 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -307,8 +307,7 @@ class recover_01_tactic : public tactic { new_goal->add(g->mc()); new_goal->add(g->pc()); - unsigned sz = g->size(); - for (unsigned i = 0; i < sz; i++) { + for (unsigned i = 0; i < g->size(); i++) { expr * f = g->form(i); if (save_clause(f)) { saved = true; @@ -356,8 +355,7 @@ class recover_01_tactic : public tactic { m_rw.set_substitution(subst); expr_ref new_curr(m); proof_ref new_pr(m); - unsigned size = new_goal->size(); - for (unsigned idx = 0; idx < size; idx++) { + for (unsigned idx = 0; idx < new_goal->size(); idx++) { expr * curr = new_goal->form(idx); m_rw(curr, new_curr); new_goal->update(idx, new_curr);