fix issues for user-propagator from new core

src/sat/sat_solver/inc_sat_solver.cpp

@@ -657,7 +657,8 @@ class inc_sat_solver : public solver {
     }
 
     euf::solver* ensure_euf() {
-        auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+        m_goal2sat.init(m, m_params, m_solver, m_map, m_dep2asm, is_incremental());
+        auto* ext = m_goal2sat.ensure_euf();
         return ext;
     }
 

src/sat/smt/euf_solver.cpp

@@ -778,7 +778,7 @@ namespace euf {
         }
         for (auto const& thv : enode_th_vars(n)) {
             auto* th = m_id2solver.get(thv.get_id(), nullptr);
-            if (th && !th->is_fixed(thv.get_var(), val, explain))
+            if (th && th->is_fixed(thv.get_var(), val, explain))
                 return true;
         }
         return false;
@@ -1067,10 +1067,7 @@ namespace euf {
         user_propagator::fresh_eh_t& fresh_eh) {
         m_user_propagator = alloc(user_solver::solver, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
-        for (unsigned i = m_scopes.size(); i-- > 0; )
-            m_user_propagator->push();
-        m_solvers.push_back(m_user_propagator);
-        m_id2solver.setx(m_user_propagator->get_id(), m_user_propagator, nullptr);
+        add_solver(m_user_propagator);
     }
 
     bool solver::watches_fixed(enode* n) const {

src/sat/tactic/goal2sat.cpp

@@ -1013,6 +1013,11 @@ goal2sat::~goal2sat() {
     dealloc(m_imp);
 }
 
+euf::solver* goal2sat::ensure_euf() {
+    return m_imp->ensure_euf();
+}
+
+
 void goal2sat::collect_param_descrs(param_descrs & r) {
     insert_max_memory(r);
     r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");

src/sat/tactic/goal2sat.h

@@ -33,6 +33,10 @@ Module Name:
 #include "sat/smt/atom2bool_var.h"
 #include "sat/smt/sat_internalizer.h"
 
+namespace euf {
+    class solver;
+}
+
 class goal2sat {
 public:
     typedef obj_map<expr, sat::literal> dep2asm_map;
@@ -41,7 +45,6 @@ class goal2sat {
     imp *  m_imp;
     unsigned m_scopes = 0;
 
-    void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external);
 
 public:
     goal2sat();
@@ -66,6 +69,9 @@ class goal2sat {
 
     void operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false);
 
+    void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external);
+
+
     void assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false);
 
     void get_interpreted_funs(func_decl_ref_vector& funs);
@@ -82,4 +88,6 @@ class goal2sat {
 
     void user_pop(unsigned n);
 
+    euf::solver* ensure_euf();
+
 };