From f06deca7e0af941c1a30da5f90f4d694b9b1b38c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Mar 2020 20:21:04 -0700
Subject: [PATCH] fix #3347

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/ctx_simplify_tactic.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 7cad0d71e..81a1364f9 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -523,6 +523,7 @@ struct ctx_simplify_tactic::imp {
     void process_goal(goal & g) {
         SASSERT(scope_level() == 0);
         // go forwards
+        expr_ref_vector pinned(m);
         unsigned old_lvl = scope_level();
         unsigned sz = g.size();
         expr_ref r(m);
@@ -532,6 +533,7 @@ struct ctx_simplify_tactic::imp {
             if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) {
                 r = m.mk_false();
             }
+            pinned.push_back(r);
             g.update(i, r, nullptr, g.dep(i));
         }
         pop(scope_level() - old_lvl);
@@ -570,12 +572,16 @@ struct ctx_simplify_tactic::imp {
 
     void operator()(goal & g) {
         m_occs.reset();
+        expr_ref_vector pinned(m);
         m_occs(g);
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            pinned.push_back(g.form(i));
+        }
         m_num_steps = 0;
         tactic_report report("ctx-simplify", g);
         if (g.proofs_enabled()) {
             expr_ref r(m);
-            unsigned sz = g.size();
             for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
                 expr * t = g.form(i);
                 process(t, r);