From c6f9c09d70b7202ecb2b1492493e6d7bec392253 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Fri, 9 Dec 2022 11:34:53 +0000
Subject: [PATCH] cleanup more in dependent_expr_state_tactic to reduce mem
 consumption

---
 src/ast/simplifiers/dependent_expr.h     | 1 -
 src/tactic/dependent_expr_state_tactic.h | 8 +++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h
index 55f8d8f4695..c1ba9dd2dac 100644
--- a/src/ast/simplifiers/dependent_expr.h
+++ b/src/ast/simplifiers/dependent_expr.h
@@ -32,7 +32,6 @@ class dependent_expr {
         m_fml(fml),
         m_proof(p),
         m_dep(d) {
-        SASSERT(fml);
         m.inc_ref(fml);
         m.inc_ref(d);
         m.inc_ref(p);
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index 9da9c1965e0..f635acca1ae 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -49,7 +49,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         m(m),
         m_params(p),
         m_factory(f),
-        m_dep(m, m.mk_true(), nullptr, nullptr)
+        m_dep(m, nullptr, nullptr, nullptr)
     {}
 
     /**
@@ -115,13 +115,13 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
         }
         catch (rewriter_exception& ex) {
             throw tactic_exception(ex.msg());
-        }       
+        }
         m_goal->elim_true();
         m_goal->elim_redundancies();
         m_goal->inc_depth();
         if (in->models_enabled())
             in->add(m_model_trail->get_model_converter().get());
-        result.push_back(in.get());   
+        result.push_back(in.get());
         cleanup();
     }
 
@@ -130,6 +130,8 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
             m_simp->collect_statistics(m_st);
         m_simp = nullptr;
         m_model_trail = nullptr;
+        m_goal = nullptr;
+        m_dep = dependent_expr(m, nullptr, nullptr, nullptr);
     }
 
     void collect_statistics(statistics & st) const override {