From 3c9ada54b64e5516e0cf869c5de7881686df8fd0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Nov 2020 11:25:09 -0800 Subject: [PATCH] tune hoist-rewriter Signed-off-by: Nikolaj Bjorner --- src/tactic/core/solve_eqs_tactic.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index a12cd6425..f4a73daec 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -690,7 +690,6 @@ class solve_eqs_tactic : public tactic { expr* f = g.form(idx); proof_ref pr1(m()), pr2(m()); thrw(f, tmp, pr1); - tmp2 = tmp; rw(tmp, tmp2, pr2); TRACE("solve_eqs", tout << mk_pp(f, m()) << " " << tmp << "\n" << tmp2 << "\n" << pr1 << "\n" << pr2 << "\n" << mk_pp(g.pr(idx), m()) << "\n";);