diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index 4b89028f3..56e27ee9a 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -96,7 +96,8 @@ public: 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(); } void cleanup() override {