diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 05edb36b1..c31f649f7 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -227,7 +227,7 @@ namespace Microsoft.Z3
         /// <returns>A string representation of the Goal.</returns>
         public string ToDimacs(bool include_names = true)
         {
-            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, include_names);
+            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
         }
 
         /// <summary>
diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 1bb193e86..c12815bfa 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -341,6 +341,28 @@ namespace euf {
             n->invariant();
     }
 
+    std::ostream& egraph::display(std::ostream& out, unsigned max_args, enode* n) const {
+        out << std::setw(5)
+            << n->get_owner_id() << " := ";
+        out << n->get_root()->get_owner_id() << " ";
+        expr* f = n->get_owner();
+        if (is_app(f))
+            out << to_app(f)->get_decl()->get_name() << " ";
+        else if (is_quantifier(f))
+            out << "q ";
+        else
+            out << "v ";
+        for (enode* arg : enode_args(n))
+            out << arg->get_owner_id() << " ";
+        for (unsigned i = n->num_args(); i < max_args; ++i)
+            out << "   ";
+        out << "\t";
+        for (enode* p : enode_parents(n))
+            out << p->get_owner_id() << " ";
+        out << "\n";
+        return out;
+    }
+
     std::ostream& egraph::display(std::ostream& out) const {
         m_table.display(out);
         unsigned max_args = 0;
@@ -348,24 +370,7 @@ namespace euf {
             max_args = std::max(max_args, n->num_args());
 
         for (enode* n : m_nodes) {
-            out << std::setw(5)
-                << n->get_owner_id() << " := ";
-            out << n->get_root()->get_owner_id() << " ";
-            expr* f = n->get_owner();
-            if (is_app(f)) 
-                out << to_app(f)->get_decl()->get_name() << " ";
-            else if (is_quantifier(f)) 
-                out << "q ";
-            else 
-                out << "v ";
-            for (enode* arg : enode_args(n)) 
-                out << arg->get_owner_id() << " ";   
-            for (unsigned i = n->num_args(); i < max_args; ++i)
-                out << "   ";
-            out << "\t";
-            for (enode* p : enode_parents(n)) 
-                out << p->get_owner_id() << " ";
-            out << "\n";            
+            display(out, max_args, n);          
         }
         return out;
     }
@@ -392,16 +397,16 @@ namespace euf {
             }
             expr*  e2 = tr(e1);
             enode* n2 = mk(e2, args.size(), args.c_ptr());
-            m_exprs.push_back(e2);
-            m_nodes.push_back(n2);
             old_expr2new_enode.setx(e1->get_id(), n2, nullptr);
         }
-        for (unsigned i = 0; i < src.m_nodes.size(); ++i) {            
+        for (unsigned i = 0; i < src.m_nodes.size(); ++i) {             
             enode* n1 = src.m_nodes[i];
-            enode* n1t = n1->m_target;
+            enode* n1t = n1->m_target;      
             enode* n2 = m_nodes[i];
-            enode* n2t = n1t ? old_expr2new_enode[n1t->get_owner_id()] : nullptr;
+            enode* n2t = n1t ? old_expr2new_enode[n1->get_owner_id()] : nullptr;
             SASSERT(!n1t || n2t);
+            SASSERT(!n1t || src.m.get_sort(n1->get_owner()) == src.m.get_sort(n1t->get_owner()));
+            SASSERT(!n1t || m.get_sort(n2->get_owner()) == m.get_sort(n2t->get_owner()));
             if (n1t && n2->get_root() != n2t->get_root()) {
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
             }
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 76f946ee1..b68ee0b20 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -101,6 +101,8 @@ namespace euf {
         }
         template <typename T>
         void explain_todo(ptr_vector<T>& justifications);
+
+        std::ostream& display(std::ostream& out, unsigned max_args, enode* n) const;
         
     public:
         egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {}
@@ -140,9 +142,17 @@ namespace euf {
         enode_vector const& nodes() const { return m_nodes; }
         void invariant();
         void copy_from(egraph const& src, std::function<void*(void*)>& copy_justification);
-        std::ostream& display(std::ostream& out) const;        
+        struct e_pp {
+            egraph const& g;
+            enode*  n;
+            e_pp(egraph const& g, enode* n) : g(g), n(n) {}
+            std::ostream& display(std::ostream& out) const { return g.display(out, 0, n); }
+        };
+        e_pp pp(enode* n) const { return e_pp(*this, n); }
+        std::ostream& display(std::ostream& out) const; 
         void collect_statistics(statistics& st) const;
     };
 
     inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); }
+    inline std::ostream& operator<<(std::ostream& out, egraph::e_pp const& p) { return p.display(out); }
 }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 119abeead..264f087c4 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -32,9 +32,10 @@ namespace euf {
     * retrieve extension that is associated with Boolean variable.
     */
     sat::th_solver* solver::get_solver(sat::bool_var v) {
-        if (v >= m_var2node.size())
+        unsigned idx = literal(v, false).index();
+        if (idx >= m_lit2node.size())
             return nullptr;
-        euf::enode* n = m_var2node[v].first;
+        euf::enode* n = m_lit2node[idx];
         if (!n)
             return nullptr;
         return get_solver(n->get_owner());
@@ -53,6 +54,8 @@ namespace euf {
         auto* ext = m_id2solver.get(fid, nullptr);
         if (ext)
             return ext;
+        if (fid == m.get_basic_family_id())
+            return nullptr;
         pb_util pb(m);
         if (pb.get_family_id() == fid) {
             ext = alloc(sat::ba_solver, m, si);
@@ -74,8 +77,11 @@ namespace euf {
     }
 
     void solver::unhandled_function(func_decl* f) {
+        if (m_unhandled_functions.contains(f))
+            return;
+        m_unhandled_functions.push_back(f);
+        m_trail.push_back(new (m_region) push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
         IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
-        // TBD: set some state with the unhandled function.
     }
 
     bool solver::propagate(literal l, ext_constraint_idx idx) { 
@@ -88,7 +94,7 @@ namespace euf {
     void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector& r) {
         auto* ext = sat::constraint_base::to_extension(idx);
         if (ext == this)
-            get_antecedents(l, *constraint::from_idx(idx), r);
+            get_antecedents(l, constraint::from_idx(idx), r);
         else
             ext->get_antecedents(l, idx, r);
     }
@@ -96,8 +102,6 @@ namespace euf {
     void solver::get_antecedents(literal l, constraint& j, literal_vector& r) {
         m_explain.reset();
         euf::enode* n = nullptr;
-        bool sign = false;
-        enode_bool_pair p;
 
         // init_ackerman();
 
@@ -107,20 +111,19 @@ namespace euf {
             m_egraph.explain<unsigned>(m_explain);
             break;
         case constraint::kind_t::eq:
-            n = m_var2node[l.var()].first;
+            n = m_lit2node[l.index()];
             SASSERT(n);
             SASSERT(m_egraph.is_equality(n));
             m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
             break;
         case constraint::kind_t::lit:
-            p = m_var2node[l.var()];
-            n = p.first;
-            sign = l.sign() != p.second;
+            n = m_lit2node[l.index()];
             SASSERT(n);
             SASSERT(m.is_bool(n->get_owner()));
-            m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? mk_false() : mk_true()), false);
+            m_egraph.explain_eq<unsigned>(m_explain, n, (l.sign() ? mk_false() : mk_true()), false);
             break;
         default:
+            std::cout << (unsigned)j.kind() << "\n";
             UNREACHABLE();
         }
         for (unsigned* idx : m_explain) 
@@ -135,20 +138,22 @@ namespace euf {
             return;
         }
 
-        auto p = m_var2node.get(l.var(), enode_bool_pair(nullptr, false));
-        if (!p.first)
+        bool sign = l.sign();
+        unsigned idx = sat::literal(l.var(), false).index();
+        auto n = m_lit2node.get(idx, nullptr);
+        if (!n)
             return;
         force_push();
-        bool sign = p.second != l.sign();
-        euf::enode* n = p.first;
+        
         expr* e = n->get_owner();
         if (m.is_eq(e) && !sign) {
             euf::enode* na = n->get_arg(0);
             euf::enode* nb = n->get_arg(1);
             m_egraph.merge(na, nb, base_ptr() + l.index());
         }
-        else {
+        else {            
             euf::enode* nb = sign ? mk_false() : mk_true();
+            std::cout << "merge " << n->get_owner_id() << " " << sign << " " << nb->get_owner_id() << "\n";
             m_egraph.merge(n, nb, base_ptr() + l.index());
         }
         // TBD: delay propagation?
@@ -216,39 +221,36 @@ namespace euf {
     }
 
     void solver::push() {
-        ++m_num_scopes;
+		scope s;
+		s.m_lit_lim = m_lit_trail.size();
+		s.m_trail_lim = m_trail.size();
+		m_scopes.push_back(s);
+		m_region.push_scope();
+		for (auto* e : m_solvers)
+			e->push();
+		m_egraph.push();
     }
 
     void solver::force_push() {
         for (; m_num_scopes > 0; --m_num_scopes) {
-            scope s;
-            s.m_bool_var_lim = m_bool_var_trail.size();
-            s.m_trail_lim = m_trail.size();
-            m_scopes.push_back(s);
-            for (auto* e : m_solvers)
-                e->push();
-            m_egraph.push();
+
         }
     }
 
     void solver::pop(unsigned n) {
-        if (n <= m_num_scopes) {
-            m_num_scopes -= n;
-            return;
-        }
-        n -= m_num_scopes;
         m_egraph.pop(n);
         for (auto* e : m_solvers)
             e->pop(n);
 
-        scope & s = m_scopes[m_scopes.size() - n];
+        scope const & s = m_scopes[m_scopes.size() - n];
 
-        for (unsigned i = m_bool_var_trail.size(); i-- > s.m_bool_var_lim; )
-            m_var2node[m_bool_var_trail[i]] = enode_bool_pair(nullptr, false);
-        m_bool_var_trail.shrink(s.m_bool_var_lim);
+        for (unsigned i = m_lit_trail.size(); i-- > s.m_lit_lim; )
+            m_lit2node[m_lit_trail[i]] = nullptr;
+        m_lit_trail.shrink(s.m_lit_lim);
         
         undo_trail_stack(*this, m_trail, s.m_trail_lim);
-        
+
+        m_region.pop_scope(n);
         m_scopes.shrink(m_scopes.size() - n);
     }
 
@@ -278,6 +280,10 @@ namespace euf {
 
     std::ostream& solver::display(std::ostream& out) const {
         m_egraph.display(out);
+        for (unsigned idx : m_lit_trail) {
+            euf::enode* n = m_lit2node[idx];
+            out << sat::to_literal(idx) << ": " << m_egraph.pp(n);
+        }
         for (auto* e : m_solvers)
             e->display(out);
         return out; 
@@ -363,8 +369,8 @@ namespace euf {
     unsigned solver::max_var(unsigned w) const { 
         for (auto* e : m_solvers)
             w = e->max_var(w);
-        for (unsigned sz = m_var2node.size(); sz-- > 0; ) {
-            euf::enode* n = m_var2node[sz].first;
+        for (unsigned sz = m_lit2node.size(); sz-- > 0; ) {
+            euf::enode* n = m_lit2node[sz];
             if (n && m.is_bool(n->get_owner())) {
                 w = std::max(w, sz);
                 break;
@@ -452,13 +458,12 @@ namespace euf {
             return n;
         if (si.is_bool_op(e)) {
             sat::literal lit = si.internalize(e);
-            enode_bool_pair bp(nullptr, false);
-            n = m_var2node.get(lit.var(), bp).first;
+            n = m_lit2node.get(lit.index(), nullptr);
             if (n)
                 return n;
             
             n = m_egraph.mk(e, 0, nullptr);
-            attach_bool_var(lit.var(), lit.sign(), n);
+            attach_lit(lit, n);
             if (!m.is_true(e) && !m.is_false(e)) 
                 s().set_external(lit.var());
             return n;
@@ -476,15 +481,16 @@ namespace euf {
         expr* e = n->get_owner();
         if (m.is_bool(e)) {
             sat::bool_var v = si.add_bool_var(e);
-            attach_bool_var(v, false, n);
+            attach_lit(literal(v, false),  n);
         }
     }
 
-    void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
-        m_var2node.reserve(v + 1, enode_bool_pair(nullptr, false));
-        SASSERT(m_var2node[v].first == nullptr);
-        m_var2node[v] = euf::enode_bool_pair(n, sign);
-        m_bool_var_trail.push_back(v);
+    void solver::attach_lit(literal lit, euf::enode* n) {
+        unsigned v = lit.index();
+        m_lit2node.reserve(v + 1, nullptr);
+        SASSERT(m_lit2node[v] == nullptr);
+        m_lit2node[v] = n;
+        m_lit_trail.push_back(v);
     }
 
     bool solver::to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index f5fe6170f..8bc69644b 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -42,7 +42,9 @@ namespace euf {
     public:
         constraint(kind_t k) : m_kind(k) {}
         kind_t kind() const { return m_kind; }
-        static constraint* from_idx(size_t z) { return reinterpret_cast<constraint*>(z); }
+        static constraint& from_idx(size_t z) { 
+            return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z)); 
+        }
         size_t to_index() const { return sat::constraint_base::mem2base(this); }
     };
 
@@ -54,11 +56,11 @@ namespace euf {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
-		struct scope {
-			unsigned m_bool_var_lim;
-			unsigned m_trail_lim;
-		};
-		typedef ptr_vector<trail<solver> > trail_stack;
+        struct scope {
+            unsigned m_lit_lim;
+            unsigned m_trail_lim;
+        };
+        typedef ptr_vector<trail<solver> > trail_stack;
 
         ast_manager&          m;
         atom2bool_var&        m_expr2var;
@@ -66,8 +68,9 @@ namespace euf {
         smt_params            m_config;
         euf::egraph           m_egraph;
         stats                 m_stats;
-		
-		trail_stack           m_trail;
+        region                m_region;
+        func_decl_ref_vector  m_unhandled_functions;
+        trail_stack           m_trail;
 
         sat::solver*           m_solver { nullptr };
         sat::lookahead*        m_lookahead { nullptr };
@@ -76,13 +79,13 @@ namespace euf {
         sat::sat_internalizer* m_to_si;
         scoped_ptr<euf::ackerman>   m_ackerman;
 
-        svector<euf::enode_bool_pair>                   m_var2node;
+        ptr_vector<euf::enode>                          m_lit2node;
         ptr_vector<unsigned>                            m_explain;
         euf::enode_vector                               m_args;
         svector<sat::frame>                             m_stack;
         unsigned                                        m_num_scopes { 0 };
-        unsigned_vector                                 m_bool_var_trail;
-		svector<scope>                                  m_scopes;
+        unsigned_vector                                 m_lit_trail;
+        svector<scope>                                  m_scopes;
         scoped_ptr_vector<sat::th_solver>               m_solvers;
         ptr_vector<sat::th_solver>                      m_id2solver;
 
@@ -96,7 +99,7 @@ namespace euf {
         // internalization
         euf::enode* visit(expr* e);
         void attach_bool_var(euf::enode* n);
-        void attach_bool_var(sat::bool_var v, bool sign, euf::enode* n);
+        void attach_lit(sat::literal lit, euf::enode* n);
         euf::enode* mk_true();
         euf::enode* mk_false();
 
@@ -118,7 +121,7 @@ namespace euf {
         // solving
         void propagate();
         void get_antecedents(literal l, constraint& j, literal_vector& r);
-		void force_push();
+        void force_push();
 
         constraint& mk_constraint(constraint*& c, constraint::kind_t k);
         constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
@@ -131,6 +134,7 @@ namespace euf {
             m_expr2var(expr2var),
             si(si),
             m_egraph(m),
+            m_unhandled_functions(m),
             m_solver(nullptr),
             m_lookahead(nullptr),
             m_to_m(&m),
@@ -197,6 +201,8 @@ namespace euf {
         bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
         sat::literal internalize(expr* e, bool sign, bool root) override;
         void update_model(model_ref& mdl);
+
+        func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
        
     };
 };
diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h
index 37e447ab4..2762d9664 100644
--- a/src/sat/smt/sat_smt.h
+++ b/src/sat/smt/sat_smt.h
@@ -88,7 +88,11 @@ namespace sat {
 
         static void* ptr2mem(void* ptr) {
             return reinterpret_cast<void*>(((unsigned char*) ptr) + ext_size());
-        }    
+        }   
+
+        static void* idx2mem(size_t idx) {
+            return ptr2mem(from_index(idx));
+        }
             
     };
 }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 26fdc3485..004919386 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -66,7 +66,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
     expr_ref_vector             m_trail;
-    func_decl_ref_vector        m_interpreted_funs;
+    func_decl_ref_vector        m_unhandled_funs;
     bool                        m_default_external;
     bool                        m_xor_solver;
     bool                        m_euf;
@@ -80,7 +80,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_map(map),
         m_dep2asm(dep2asm),
         m_trail(m),
-        m_interpreted_funs(m),
+        m_unhandled_funs(m),
         m_default_external(default_external) {
         updt_params(p);
         m_true = sat::null_literal;
@@ -174,7 +174,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                         return;
                     }
                     else
-                        m_interpreted_funs.push_back(to_app(t)->get_decl());
+                        m_unhandled_funs.push_back(to_app(t)->get_decl());
                 }
             }
         }
@@ -398,8 +398,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
-        sat::literal  l1 = m_result_stack[sz - 1];
-        sat::literal  l2 = m_result_stack[sz - 2];
+        sat::literal  l2 = m_result_stack[sz - 1];
+        sat::literal  l1 = m_result_stack[sz - 2];
         if (root) {
             SASSERT(sz == 2);
             if (sign) {
@@ -469,6 +469,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
             convert_iff2(t, root, sign);
     }
 
+    func_decl_ref_vector const& interpreted_funs() {
+        auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+        if (ext)
+            return ext->unhandled_functions();
+        return m_unhandled_funs;
+    }
+
     void convert_euf(expr* e, bool root, bool sign) {
         sat::extension* ext = m_solver.get_extension();
         euf::solver* euf = nullptr;
@@ -693,6 +700,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void operator()(goal const & g) {
+        g.display(std::cout);
         struct scoped_reset {
             imp& i;
             scoped_reset(imp& i) :i(i) {}
@@ -741,6 +749,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
+    void update_model(model_ref& mdl) {
+        auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
+        if (ext)
+            ext->update_model(mdl);
+    }
+
 };
 
 struct unsupported_bool_proc {
@@ -792,7 +806,7 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
         
     (*m_imp)(g);
     
-    if (!t.get_extension() && m_imp->m_interpreted_funs.empty()) {
+    if (!t.get_extension() && m_imp->interpreted_funs().empty()) {
         dealloc(m_imp);
         m_imp = nullptr;
     }
@@ -801,12 +815,17 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
 
 void goal2sat::get_interpreted_funs(func_decl_ref_vector& atoms) {
     if (m_imp) {
-        atoms.append(m_imp->m_interpreted_funs);
+        atoms.append(m_imp->interpreted_funs());
     }
 }
 
 bool goal2sat::has_interpreted_funs() const {
-    return m_imp && !m_imp->m_interpreted_funs.empty(); 
+    return m_imp && !m_imp->interpreted_funs().empty(); 
+}
+
+void goal2sat::update_model(model_ref& mdl) {
+    if (m_imp) 
+        m_imp->update_model(mdl);
 }
 
 
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index 1576b10a9..298e9dc36 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -61,12 +61,14 @@ public:
     */
     void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
-    void get_interpreted_funs(func_decl_ref_vector& atoms);
+    void get_interpreted_funs(func_decl_ref_vector& funs);
 
     bool has_interpreted_funs() const;
 
     sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
 
+    void update_model(model_ref& mdl);
+
 };
 
 
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 455df100e..8249bd865 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -50,11 +50,12 @@ class sat_tactic : public tactic {
             obj_map<expr, sat::literal> dep2asm;
             sat::literal_vector assumptions;
             m_goal2sat(*g, m_params, *m_solver, map, dep2asm);
-            TRACE("sat", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
-                  for (auto const& kv : map) {
-                      if (!is_uninterp_const(kv.m_key))
-                          tout << mk_ismt2_pp(kv.m_key, m) << "\n";
-                  });
+            TRACE("sat", tout << "interpreted_atoms: " << m_goal2sat.has_interpreted_funs() << "\n";
+                  func_decl_ref_vector funs(m);
+                  m_goal2sat.get_interpreted_funs(funs);
+                  for (func_decl* f : funs) 
+                      tout << mk_ismt2_pp(f, m) << "\n";
+                  );
             g->reset();
             g->m().compact_memory();
 
@@ -78,7 +79,7 @@ class sat_tactic : public tactic {
                 }
                 g->assert_expr(m.mk_false(), nullptr, lcore);
             }
-            else if (r == l_true && !map.interpreted_atoms()) {
+            else if (r == l_true && !m_goal2sat.has_interpreted_funs()) {
                 // register model
                 if (produce_models) {
                     model_ref md = alloc(model, m);
@@ -99,6 +100,7 @@ class sat_tactic : public tactic {
                             break;
                         }
                     }
+                    m_goal2sat.update_model(md);
                     TRACE("sat_tactic", model_v2_pp(tout, *md););
                     g->add(model2model_converter(md.get()));
                 }