fix #4174

src/ast/num_occurs.cpp

@@ -59,6 +59,12 @@ void num_occurs::process(expr * t, expr_fast_mark1 & visited) {
     }
 }
 
+void num_occurs::validate() {
+    for (auto & kv : m_num_occurs) {
+        SASSERT(0 < kv.m_key->get_ref_count());
+    }
+}
+
 void num_occurs::operator()(expr * t) {
     expr_fast_mark1   visited;
     process(t, visited);

src/ast/num_occurs.h

@@ -38,7 +38,8 @@ public:
         m_ignore_quantifiers(ignore_quantifiers) {
     }
 
-    void reset() { m_num_occurs.reset(); }
+    void validate();
+    virtual void reset() { m_num_occurs.reset(); }
     
     void operator()(expr * t);
     void operator()(unsigned num, expr * const * ts);

src/tactic/core/ctx_simplify_tactic.cpp

@@ -168,7 +168,7 @@ struct ctx_simplify_tactic::imp {
         m(_m),
         m_simp(simp),
         m_allocator("context-simplifier"),
-        m_occs(true, true),
+        m_occs(m, true, true),
         m_mk_app(m, p) {
         updt_params(p);
         m_simp->set_occs(m_occs);
@@ -522,7 +522,6 @@ 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,7 +531,6 @@ 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);
@@ -571,13 +569,9 @@ 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;
+        unsigned sz = g.size();
         tactic_report report("ctx-simplify", g);
         if (g.proofs_enabled()) {
             expr_ref r(m);

src/tactic/goal_num_occurs.cpp

@@ -22,6 +22,7 @@ void goal_num_occurs::operator()(goal const & g) {
     expr_fast_mark1   visited;
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; i++) {
+        m_pinned.push_back(g.form(i));
         process(g.form(i), visited);
     }
 }

src/tactic/goal_num_occurs.h

@@ -23,11 +23,14 @@ Revision History:
 class goal;
 
 class goal_num_occurs : public num_occurs { 
+    expr_ref_vector m_pinned;
 public:
-    goal_num_occurs(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
+    goal_num_occurs(ast_manager& m, bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
-        num_occurs(ignore_ref_count1, ignore_quantifiers) {
+        num_occurs(ignore_ref_count1, ignore_quantifiers), 
+        m_pinned(m) {
     }
 
+    void reset() override { num_occurs::reset(); m_pinned.reset(); }
     void operator()(goal const & s);
 };