#5454

src/sat/sat_extension.h

@@ -120,7 +120,7 @@ namespace sat {
         virtual bool check_model(model const& m) const { return true; }
         virtual void gc_vars(unsigned num_vars) {}
         virtual bool should_research(sat::literal_vector const& core) { return false;}
-        virtual void add_assumptions() {}
+        virtual void add_assumptions(literal_set& ext_assumptions) {}
         virtual bool tracking_assumptions() { return false; }
         virtual bool enable_self_propagate() const { return false; }
 

src/sat/sat_solver.cpp

@@ -1895,9 +1895,7 @@ namespace sat {
             m_ext_assumption_set.reset();
             unsigned trail_size = m_trail.size();
             if (!inconsistent())
-                m_ext->add_assumptions();
-            for (unsigned i = trail_size; i < m_trail.size(); ++i)
-                m_ext_assumption_set.insert(m_trail[i]);
+                m_ext->add_assumptions(m_ext_assumption_set);
         }
     }
 

src/sat/smt/euf_solver.cpp

@@ -699,9 +699,9 @@ namespace euf {
         return result;
     }
 
-    void solver::add_assumptions() {
+    void solver::add_assumptions(sat::literal_set& assumptions) {
         for (auto* e : m_solvers)
-            e->add_assumptions();
+            e->add_assumptions(assumptions);
     }
 
     bool solver::tracking_assumptions() {

src/sat/smt/euf_solver.h

@@ -276,7 +276,7 @@ namespace euf {
         bool propagated(literal l, ext_constraint_idx idx) override;
         bool unit_propagate() override;
         bool should_research(sat::literal_vector const& core) override;
-        void add_assumptions() override;
+        void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override;
 
         void propagate(literal lit, ext_justification_idx idx);

src/sat/smt/recfun_solver.cpp

@@ -279,13 +279,18 @@ namespace recfun {
         return true;
     }
 
-    void solver::add_assumptions() {
+    void solver::add_assumptions(sat::literal_set& assumptions) {
         if (u().has_defs() || m_disabled_guards.empty()) {
             app_ref dlimit = m_util.mk_num_rounds_pred(m_num_rounds);
             TRACEFN("add_theory_assumption " << dlimit);
-            s().assign_scoped(mk_literal(dlimit));
-            for (auto g : m_disabled_guards)
-                s().assign_scoped(~mk_literal(g));
+            sat::literal assumption = mk_literal(dlimit); 
+            assumptions.insert(assumption);
+            s().assign_scoped(assumption);
+            for (auto g : m_disabled_guards) {
+                assumption = ~mk_literal(g);
+                assumptions.insert(assumption);
+                s().assign_scoped(assumption);
+            }
         }
     }
 

src/sat/smt/recfun_solver.h

@@ -108,7 +108,7 @@ namespace recfun {
         bool is_shared(euf::theory_var v) const override { return true; }
         void init_search() override {}
         bool should_research(sat::literal_vector const& core) override;
-        void add_assumptions() override;
+        void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override { return true; }
     };
 }