diff --git a/src/ast/simplifiers/dependent_expr.h b/src/ast/simplifiers/dependent_expr.h
index 55f8d8f46..c1ba9dd2d 100644
--- a/src/ast/simplifiers/dependent_expr.h
+++ b/src/ast/simplifiers/dependent_expr.h
@@ -32,7 +32,6 @@ public:
         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 9da9c1965..f635acca1 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -49,7 +49,7 @@ public:
         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 @@ public:
         }
         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 @@ public:
             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 {