fix #7582

src/ast/simplifiers/elim_unconstrained.cpp

@@ -411,13 +411,14 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
         case generic_model_converter::instruction::HIDE:
             break;
         case generic_model_converter::instruction::ADD:
-            new_def = entry.m_def;
+            //            new_def = entry.m_def;
-            (*rp)(new_def);           
+            // (*rp)(new_def);
-            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
+            new_def = m.mk_const(entry.m_f);
+            sub->insert(new_def, new_def, nullptr, nullptr);
             break;
         }
     }
-    trail.push(sub.detach(), old_fmls);
+    trail.push(sub.detach(), old_fmls, true);
 }
 
 void elim_unconstrained::reduce() {

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -75,7 +75,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
         // loose entries that intersect with free vars are deleted from the trail
         // and their removed formulas are added to the resulting constraints.
 
-        if (t->is_loose() && !t->is_def() && t->is_subst()) {
+        if (t->is_loose_subst()) {                
             for (auto const& [k, v] : t->m_subst->sub()) {
                 add_vars(v, free_vars);
                 st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr));
@@ -83,6 +83,17 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
             t->m_active = false;
             continue;
         }
+        
+        if (t->is_loose_constraint()) {                
+            for (auto r : t->m_removed) {
+                add_vars(r, free_vars);
+                TRACE("simplifier", tout << "replay removed " << r << "\n");
+                st.add(r);
+            }
+            t->m_active = false;
+            continue;
+        }
+
 
         bool all_const = true;
         for (auto const& [d, def, dep] : t->m_defs) 

src/ast/simplifiers/model_reconstruction_trail.h

@@ -36,30 +36,37 @@ class dependent_expr_state;
 class model_reconstruction_trail {
 
     struct entry {
+        enum entry_t { loose_subst, loose_constraints, hide, defined};
+
+        entry_t                       m_ty;
         scoped_ptr<expr_substitution> m_subst;
         vector<dependent_expr>        m_removed;
         func_decl_ref                 m_decl;
         vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> m_defs;
         bool                          m_active = true;
 
-        entry(ast_manager& m, expr_substitution* s, vector<dependent_expr> const& rem) :
+        entry(ast_manager& m, expr_substitution* s, vector<dependent_expr> const& rem, bool replay_constraints) :
-            m_subst(s), m_removed(rem), m_decl(m) {}
+            m_ty(replay_constraints ? loose_constraints : loose_subst), m_subst(s), m_removed(rem), m_decl(m) {}
 
-        entry(ast_manager& m, func_decl* h) : m_decl(h, m) {}
+        entry(ast_manager& m, func_decl* h) : m_ty(hide), m_decl(h, m) {}
 
         entry(ast_manager& m, func_decl* f, expr* def, expr_dependency* dep, vector<dependent_expr> const& rem) :
+            m_ty(defined), 
             m_removed(rem),
             m_decl(m){
             m_defs.push_back({ func_decl_ref(f, m), expr_ref(def, m), expr_dependency_ref(dep, m) });
         }
 
         entry(ast_manager& m, vector<std::tuple<func_decl_ref, expr_ref, expr_dependency_ref>> const& defs, vector<dependent_expr> const& rem) :
+            m_ty(defined), 
             m_removed(rem),
             m_decl(m),
             m_defs(defs) {
         }
 
         bool is_loose() const { return !m_removed.empty(); }
+        bool is_loose_subst() const { return m_ty == loose_subst; }
+        bool is_loose_constraint() const { return m_ty == loose_constraints; }
 
         bool intersects(ast_mark const& free_vars) const {
             if (is_hide())
@@ -141,8 +148,8 @@ public:
     /**
     * add a new substitution to the trail
     */
-    void push(expr_substitution* s, vector<dependent_expr> const& removed) {
+    void push(expr_substitution* s, vector<dependent_expr> const& removed, bool replay_constraints) {
-        m_trail.push_back(alloc(entry, m, s, removed));
+        m_trail.push_back(alloc(entry, m, s, removed, replay_constraints));
         m_trail_stack.push(push_back_vector(m_trail));     
         for (auto& [k, v] : s->sub())
             add_model_var(to_app(k)->get_decl());

src/ast/simplifiers/solve_eqs.cpp

@@ -306,7 +306,7 @@ namespace euf {
 
     void solve_eqs::save_subst(vector<dependent_expr> const& old_fmls) {
         if (!m_subst->empty())   
-            m_fmls.model_trail().push(m_subst.detach(), old_fmls);                
+            m_fmls.model_trail().push(m_subst.detach(), old_fmls, false);                
     }
 
     void solve_eqs::filter_unsafe_vars() {