diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index fa4bbdd49..b94b422ad 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -46,6 +46,7 @@ public:
     virtual unsigned size() const = 0;
     virtual dependent_expr const& operator[](unsigned i) = 0;
     virtual void update(unsigned i, dependent_expr const& j) = 0;
+    virtual void add(dependent_expr const& j) = 0;
     virtual bool inconsistent() = 0;
     virtual model_reconstruction_trail& model_trail() = 0;
 
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index d3f77b773..efe28c30d 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/src/tactic/dependent_expr_state_tactic.h
@@ -60,10 +60,16 @@ public:
         m_dep = dependent_expr(m, m_goal->form(i), m_goal->dep(i));
         return m_dep;
     }
+    
     void update(unsigned i, dependent_expr const& j) override {
         auto [f, d] = j();
         m_goal->update(i, f, nullptr, d);
     }
+    
+    void add(dependent_expr const& j) override {
+        auto [f, d] = j();
+        m_goal->assert_expr(f, nullptr, d);
+    }
 
     bool inconsistent() override {
         return m_goal->inconsistent();