diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp
index a38b19c7d..f0e960644 100644
--- a/src/ackermannization/ackermannize_bv_tactic.cpp
+++ b/src/ackermannization/ackermannize_bv_tactic.cpp
@@ -29,9 +29,7 @@ public:
 
     virtual ~ackermannize_bv_tactic() { }
 
-    virtual void operator()(goal_ref const & g,
-        goal_ref_buffer & result,
-        expr_dependency_ref & core) {
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
         tactic_report report("ackermannize", *g);
         fail_if_unsat_core_generation("ackermannize", g);
         fail_if_proof_generation("ackermannize", g);
@@ -49,7 +47,6 @@ public:
             TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;);
             result.reset();
             result.push_back(g.get());
-            core = 0;
             return;
         }
         result.push_back(resg.get());
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 2d9a47863..e9b3bb47d 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -25,7 +25,7 @@ Revision History:
 #include "util/cancel_eh.h"
 #include "util/scoped_timer.h"
 
-Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c), m_core(m) {
+Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c) {
 }
 
 extern "C" {
@@ -418,7 +418,7 @@ extern "C" {
             scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             try {
-                exec(*to_tactic_ref(t), new_goal, ref->m_subgoals, ref->m_core);
+                exec(*to_tactic_ref(t), new_goal, ref->m_subgoals);
                 ref->m_pc = new_goal->pc();
                 ref->m_mc = new_goal->mc();
                 return of_apply_result(ref);
diff --git a/src/api/api_tactic.h b/src/api/api_tactic.h
index fd2f05185..909785748 100644
--- a/src/api/api_tactic.h
+++ b/src/api/api_tactic.h
@@ -50,7 +50,6 @@ struct Z3_apply_result_ref : public api::object {
     goal_ref_buffer      m_subgoals;
     model_converter_ref  m_mc;
     proof_converter_ref  m_pc;
-    expr_dependency_ref  m_core;
     Z3_apply_result_ref(api::context& c, ast_manager & m);
     virtual ~Z3_apply_result_ref() {}
 };
diff --git a/src/cmd_context/echo_tactic.cpp b/src/cmd_context/echo_tactic.cpp
index 37dcc0a29..131962716 100644
--- a/src/cmd_context/echo_tactic.cpp
+++ b/src/cmd_context/echo_tactic.cpp
@@ -28,15 +28,14 @@ public:
     echo_tactic(cmd_context & ctx, char const * msg, bool newline):m_ctx(ctx), m_msg(msg), m_newline(newline) {}
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         #pragma omp critical (echo_tactic)
         {
             m_ctx.regular_stream() << m_msg;
             if (m_newline)
                 m_ctx.regular_stream() << std::endl;
         }
-        skip_tactic::operator()(in, result, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
@@ -60,8 +59,7 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         double val = (*m_p)(*(in.get())).get_value();
         #pragma omp critical (probe_value_tactic)
         {
@@ -71,7 +69,7 @@ public:
             if (m_newline)
                 m_ctx.diagnostic_stream() << std::endl;
         }
-        skip_tactic::operator()(in, result, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 20f6fc632..efbb81e28 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -326,7 +326,6 @@ public:
             unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
 
             goal_ref_buffer     result_goals;
-            expr_dependency_ref core(m);
 
             std::string reason_unknown;
             bool failed = false;
@@ -337,7 +336,7 @@ public:
                 scoped_timer timer(timeout, &eh);
                 cmd_context::scoped_watch sw(ctx);
                 try {
-                    exec(t, g, result_goals, core);
+                    exec(t, g, result_goals);
                 }
                 catch (tactic_exception & ex) {
                     ctx.regular_stream() << "(error \"tactic failed: " << ex.msg() << "\")" << std::endl;
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 5940dcbfc..184d7f54a 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -242,14 +242,12 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
             m_imp->process(*in);
             m_imp->collect_statistics(m_stats);
             result.reset();
             result.push_back(in.get());
-            core = 0;
         }
         catch (z3_exception & ex) {
             // convert all Z3 exceptions into tactic exceptions
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index 4802bbb33..881ae9aec 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -177,10 +177,8 @@ class horn_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("horn", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -386,9 +384,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void collect_statistics(statistics & st) const {
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 452be8914..effb9f613 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -202,9 +202,8 @@ namespace pdr {
     void pred_transformer::simplify_formulas(tactic& tac, expr_ref_vector& v) {
         goal_ref g(alloc(goal, m, false, false, false));
         for (unsigned j = 0; j < v.size(); ++j) g->assert_expr(v[j].get());
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
-        tac(g, result, core);
+        tac(g, result);
         SASSERT(result.size() == 1);
         goal* r = result[0];
         v.reset();
diff --git a/src/muz/pdr/pdr_farkas_learner.cpp b/src/muz/pdr/pdr_farkas_learner.cpp
index 68a9db2ef..59cc7de0b 100644
--- a/src/muz/pdr/pdr_farkas_learner.cpp
+++ b/src/muz/pdr/pdr_farkas_learner.cpp
@@ -520,10 +520,9 @@ namespace pdr {
             g->assert_expr(lemmas[i].get()); 
         }
         expr_ref tmp(m);
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
         tactic_ref simplifier = mk_arith_bounds_tactic(m);
-        (*simplifier)(g, result, core);
+        (*simplifier)(g, result);
         lemmas.reset();
         SASSERT(result.size() == 1);
         goal* r = result[0];
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index d1350d29a..3a032fdb3 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1367,7 +1367,6 @@ void pred_transformer::frames::simplify_formulas ()
         // normalize level
         unsigned level = i < m_size ? i : infty_level ();
 
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
 
         // simplify lemmas of the current level
@@ -1393,7 +1392,7 @@ void pred_transformer::frames::simplify_formulas ()
         }
 
         // more than one lemma at current level. simplify.
-        (*simplifier)(g, result, core);
+        (*simplifier)(g, result);
         SASSERT(result.size () == 1);
         goal *r = result[0];
 
diff --git a/src/muz/spacer/spacer_legacy_frames.cpp b/src/muz/spacer/spacer_legacy_frames.cpp
index 176e0101b..49157a085 100644
--- a/src/muz/spacer/spacer_legacy_frames.cpp
+++ b/src/muz/spacer/spacer_legacy_frames.cpp
@@ -46,9 +46,8 @@ void pred_transformer::legacy_frames::simplify_formulas(tactic& tac,
     ast_manager &m = m_pt.get_ast_manager();
     goal_ref g(alloc(goal, m, false, false, false));
     for (unsigned j = 0; j < v.size(); ++j) { g->assert_expr(v[j].get()); }
-    expr_dependency_ref core(m);
     goal_ref_buffer result;
-    tac(g, result, core);
+    tac(g, result);
     SASSERT(result.size() == 1);
     goal* r = result[0];
     v.reset();
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 726ff86c8..1eddedb68 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -929,10 +929,9 @@ void simplify_bounds_old(expr_ref_vector& cube) {
     }
 
     expr_ref tmp(m);
-    expr_dependency_ref core(m);
     goal_ref_buffer result;
     tactic_ref simplifier = mk_arith_bounds_tactic(m);
-    (*simplifier)(g, result, core);
+    (*simplifier)(g, result);
     SASSERT(result.size() == 1);
     goal* r = result[0];
 
@@ -953,13 +952,12 @@ void simplify_bounds_new (expr_ref_vector &cube) {
         g->assert_expr(cube.get(i));
     }
 
-    expr_dependency_ref dep(m);
     goal_ref_buffer goals;
     tactic_ref prop_values = mk_propagate_values_tactic(m);
     tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m);
     tactic_ref t = and_then(prop_values.get(), prop_bounds.get());
 
-    (*t)(g, goals, dep);
+    (*t)(g, goals);
     SASSERT(goals.size() == 1);
 
     g = goals[0];
diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp
index bedd7c655..25e5b12cc 100644
--- a/src/nlsat/tactic/nlsat_tactic.cpp
+++ b/src/nlsat/tactic/nlsat_tactic.cpp
@@ -129,10 +129,8 @@ class nlsat_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("nlsat", *g);
             
             if (g->is_decided()) {
@@ -233,12 +231,11 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
             imp local_imp(in->m(), m_params);
             scoped_set_imp setter(*this, local_imp);
-            local_imp(in, result, core);
+            local_imp(in, result);
         }
         catch (z3_error & ex) {
             throw ex;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index edcdb64e0..dd90963df 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -745,9 +745,8 @@ namespace opt {
         else {
             set_simplify(tac0.get());
         }
-        expr_dependency_ref core(m);
         goal_ref_buffer result;
-        (*m_simplify)(g, result, core); 
+        (*m_simplify)(g, result); 
         SASSERT(result.size() == 1);
         goal* r = result[0];
         m_model_converter = r->mc();
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index 87e713efc..ec27e168a 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -660,7 +660,7 @@ namespace qe {
             g->assert_expr(fml);
             expr_dependency_ref core(m);
             goal_ref_buffer result;
-            (*m_nftactic)(g, result, core);
+            (*m_nftactic)(g, result);
             SASSERT(result.size() == 1);
             TRACE("qe", result[0]->display(tout););
             g2s(*result[0], m_params, m_solver, m_a2b, m_t2x);
@@ -810,14 +810,12 @@ namespace qe {
 
         
         void operator()(/* in */  goal_ref const & in, 
-                        /* out */ goal_ref_buffer & result, 
-                        /* out */ expr_dependency_ref & core) {
+                        /* out */ goal_ref_buffer & result) {
 
             tactic_report report("nlqsat-tactic", *in);
 
             ptr_vector<expr> fmls;
             expr_ref fml(m);
-            core = 0;
             in->get_formulas(fmls);
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             if (m_mode == elim_t) {
diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 51e5c1b78..5c0e3b7d8 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -2532,10 +2532,8 @@ class qe_lite_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("qe-lite", *g);
             proof_ref new_pr(m);
             expr_ref new_f(m);
@@ -2601,9 +2599,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
 
diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp
index 28bc78f84..43029204e 100644
--- a/src/qe/qe_sat_tactic.cpp
+++ b/src/qe/qe_sat_tactic.cpp
@@ -233,8 +233,7 @@ namespace qe {
 
         virtual void operator()(
             goal_ref const& goal,  
-            goal_ref_buffer& result, 
-            expr_dependency_ref& core) 
+            goal_ref_buffer& result) 
         {
             try {
                 checkpoint();
diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp
index 131d0d3fb..80f52020c 100644
--- a/src/qe/qe_tactic.cpp
+++ b/src/qe/qe_tactic.cpp
@@ -50,10 +50,8 @@ class qe_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("qe", *g);
             m_fparams.m_model = g->models_enabled();
             proof_ref new_pr(m);
@@ -119,9 +117,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
         m_st.reset();
         m_imp->collect_statistics(m_st);
         
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index ca8a36844..2e78574ec 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1211,16 +1211,12 @@ namespace qe {
 
         
         void operator()(/* in */  goal_ref const & in, 
-                        /* out */ goal_ref_buffer & result, 
-                        /* out */ expr_dependency_ref & core) {
+                        /* out */ goal_ref_buffer & result) {
             tactic_report report("qsat-tactic", *in);
             ptr_vector<expr> fmls;
             expr_ref_vector defs(m);
             expr_ref fml(m);
-            core = 0;
             in->get_formulas(fmls);
-
-
             fml = mk_and(m, fmls.size(), fmls.c_ptr());
             
             // for now:
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index d391eddd0..3f5744556 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -61,7 +61,6 @@ class inc_sat_solver : public solver {
     model_converter_ref m_mc;
     model_converter_ref m_mc0;
     model_converter_ref m_sat_mc;
-    expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
     std::string         m_unknown;
     // access formulas after they have been pre-processed and handled by the sat solver.
@@ -82,7 +81,6 @@ public:
         m_core(m),
         m_map(m),
         m_num_scopes(0),
-        m_dep_core(m),
         m_unknown("no reason given"),
         m_internalized(false), 
         m_internalized_converted(false), 
@@ -495,7 +493,6 @@ private:
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_mc.reset();
         m_pc.reset();
-        m_dep_core.reset();
         m_subgoals.reset();
         init_preprocess();
         SASSERT(g->models_enabled());
@@ -505,7 +502,7 @@ private:
         SASSERT(!g->proofs_enabled());
         TRACE("sat", g->display(tout););
         try {
-            (*m_preprocess)(g, m_subgoals, m_dep_core);
+            (*m_preprocess)(g, m_subgoals);
         }
         catch (tactic_exception & ex) {
             IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 413dfa9bf..a708f99bf 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -39,9 +39,7 @@ class sat_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+                        goal_ref_buffer & result) { 
             fail_if_proof_generation("sat", g);
             bool produce_models = g->models_enabled();
             bool produce_core = g->unsat_core_enabled();
@@ -175,12 +173,11 @@ public:
     }
     
     void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) {
+                    goal_ref_buffer & result) {
         imp proc(g->m(), m_params);
         scoped_set_imp set(this, &proc);
         try {
-            proc(g, result, core);
+            proc(g, result);
             proc.m_solver.collect_statistics(m_stats);
         }
         catch (sat::solver_exception & ex) {
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index d504a63b2..b2385b971 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -70,10 +70,8 @@ public:
     virtual void reset_statistics() { m_num_steps = 0; }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         
-        core = 0;
         reduce(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 2bb68d590..dc927e9f3 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -145,11 +145,9 @@ public:
 
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
             IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";);
-            core = 0;
             SASSERT(in->is_well_sorted());
             ast_manager & m = in->m();
             TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp
index 0b900426b..5258f8711 100644
--- a/src/smt/tactic/unit_subsumption_tactic.cpp
+++ b/src/smt/tactic/unit_subsumption_tactic.cpp
@@ -40,8 +40,7 @@ struct unit_subsumption_tactic : public tactic {
     void cleanup() {}
 
     virtual void operator()(/* in */  goal_ref const & in, 
-                            /* out */ goal_ref_buffer & result, 
-                            /* out */ expr_dependency_ref & core) {        
+                            /* out */ goal_ref_buffer & result) {        
         reduce_core(in, result);
     }
 
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 60a7404b6..6863c935e 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -102,9 +102,7 @@ public:
     }
 
     virtual void operator()(/* in */  goal_ref const & in, 
-                            /* out */ goal_ref_buffer & result, 
-                            /* out */ expr_dependency_ref & core) {
-        core = 0;
+                            /* out */ goal_ref_buffer & result) {
         expr_ref_vector clauses(m);
         expr2expr_map               bool2dep;
         ptr_vector<expr>            assumptions;
@@ -130,7 +128,7 @@ public:
         case l_false: {
             in->reset();
             proof* pr = 0;
-            expr_dependency* lcore = 0;
+            expr_dependency_ref lcore(m);
             if (in->proofs_enabled()) {
                 pr = local_solver->get_proof();
                 in->set(proof2proof_converter(m, pr));
@@ -138,13 +136,13 @@ public:
             if (in->unsat_core_enabled()) {
                 ptr_vector<expr> core;
                 local_solver->get_unsat_core(core);
-                for (unsigned i = 0; i < core.size(); ++i) {
-                    lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(core[i])));
+                for (expr* c : core) {
+                    lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(c)));
                 }
             }
             in->assert_expr(m.mk_false(), pr, lcore);
             result.push_back(in.get());
-            core = lcore;
+            in->set(dependency_converter::unit(lcore));
             break;
         }
         case l_undef:
diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt
index 8e1ae8cd5..c9554b76a 100644
--- a/src/tactic/CMakeLists.txt
+++ b/src/tactic/CMakeLists.txt
@@ -1,5 +1,6 @@
 z3_add_component(tactic
   SOURCES
+    dependency_converter.cpp
     equiv_proof_converter.cpp
     generic_model_converter.cpp
     goal.cpp
diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp
index 6de44c654..606ed7d82 100644
--- a/src/tactic/aig/aig_tactic.cpp
+++ b/src/tactic/aig/aig_tactic.cpp
@@ -90,11 +90,8 @@ public:
         SASSERT(g->is_well_sorted());
     }
     
-    virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
         fail_if_proof_generation("aig", g);
-        core = 0;
         operator()(g);
         g->inc_depth();
         result.push_back(g.get());
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 852eb9cc0..1449ae645 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -111,9 +111,7 @@ class add_bounds_tactic : public tactic {
         };
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+                        goal_ref_buffer & result) {
             tactic_report report("add-bounds", *g);
             bound_manager bm(m);
             expr_fast_mark1 visited;
@@ -159,9 +157,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(g, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp
index d86d8dd8f..afac5b4e6 100644
--- a/src/tactic/arith/arith_bounds_tactic.cpp
+++ b/src/tactic/arith/arith_bounds_tactic.cpp
@@ -24,8 +24,7 @@ struct arith_bounds_tactic : public tactic {
 
 
     virtual void operator()(/* in */  goal_ref const & in, 
-                            /* out */ goal_ref_buffer & result, 
-                            /* out */ expr_dependency_ref & core) {        
+                            /* out */ goal_ref_buffer & result) {        
         bounds_arith_subsumption(in, result);
     }
     
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index ec9f92a35..6349c40b2 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -53,11 +53,10 @@ public:
 
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         TRACE("card2bv-before", g->display(tout););
         SASSERT(g->is_well_sorted());
-        core = 0; result.reset();
+        result.reset();
         tactic_report report("card2bv", *g);
         th_rewriter rw1(m, m_params);
         pb2bv_rewriter rw2(m, m_params);
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index 62b030706..704d48eac 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -223,10 +223,8 @@ class degree_shift_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             m_produce_proofs = g->proofs_enabled();
             m_produce_models = g->models_enabled();
             tactic_report report("degree_shift", *g);
@@ -291,9 +289,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index 06966178f..bf45e1afe 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -313,11 +313,10 @@ class diff_neq_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
             m_produce_models = g->models_enabled();
-            core = 0; result.reset();
+            result.reset();
             tactic_report report("diff-neq", *g);
             fail_if_proof_generation("diff-neq", g);
             fail_if_unsat_core_generation("diff-neq", g);
@@ -383,9 +382,8 @@ public:
        If s is not really in the difference logic fragment, then this is a NOOP.
     */
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/arith/elim01_tactic.cpp b/src/tactic/arith/elim01_tactic.cpp
index 731ca4b5d..a287e7a83 100644
--- a/src/tactic/arith/elim01_tactic.cpp
+++ b/src/tactic/arith/elim01_tactic.cpp
@@ -152,10 +152,8 @@ public:
 
     
     virtual void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) {
+                    goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
-        core = 0;
         
         tactic_report report("elim01", *g);
         
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 74bc9a5ef..50dd142e6 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -149,12 +149,8 @@ public:
     void updt_params(params_ref const & p) {
     }
     
-    virtual void operator()(
-        goal_ref const & g, 
-        goal_ref_buffer & result, 
-        expr_dependency_ref & core) {
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
-        core = 0;
         m_trail.reset();
         m_fd.reset();
         m_max.reset();
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 1233ddf9d..3ddc8b7bf 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -257,10 +257,8 @@ class factor_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("factor", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -311,10 +309,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (z3_error & ex) {
             throw ex;
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index 16288f7ad..fe1b64e90 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -249,10 +249,8 @@ class fix_dl_var_tactic : public tactic {
         }
                 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("fix-dl-var", *g);
             bool produce_proofs = g->proofs_enabled();
             m_produce_models    = g->models_enabled();
@@ -319,10 +317,9 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 92e6ee530..fac826811 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1550,10 +1550,8 @@ class fm_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("fm", *g);
             fail_if_proof_generation("fm", g);
             m_produce_models = g->models_enabled();
@@ -1673,9 +1671,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 };
 
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index dfff44526..4bcf24534 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -159,10 +159,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) {
+                    goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
-        core = 0;
         m_01s->reset();
         
         tactic_report report("cardinality-intro", *g);
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index cc339f74a..274c6dd40 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -188,13 +188,12 @@ class lia2pb_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("lia2pb", g);
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
-            core = 0; result.reset();
+            result.reset();
             tactic_report report("lia2pb", *g);
             m_bm.reset(); m_rw.reset(); m_new_deps.reset();
 
@@ -328,10 +327,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp
index 2b4783c6f..f7c985129 100644
--- a/src/tactic/arith/nla2bv_tactic.cpp
+++ b/src/tactic/arith/nla2bv_tactic.cpp
@@ -440,12 +440,11 @@ public:
        \return false if transformation is not possible.
     */
     virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
         fail_if_proof_generation("nla2bv", g);
         fail_if_unsat_core_generation("nla2bv", g);
-        core = 0; result.reset();
+        result.reset();
         
         imp proc(g->m(), m_params);
         scoped_set_imp setter(*this, proc);
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index 955e92f1a..130b5cfe6 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -79,10 +79,7 @@ class normalize_bounds_tactic : public tactic {
             return false;
         }
         
-        void operator()(goal_ref const & in, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+        void operator()(goal_ref const & in, goal_ref_buffer & result) {
             bool produce_models = in->models_enabled();
             bool produce_proofs = in->proofs_enabled();
             tactic_report report("normalize-bounds", *in);
@@ -166,10 +163,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index e06c44110..de4fa8221 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -886,14 +886,13 @@ private:
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             TRACE("pb2bv", g->display(tout););
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("pb2bv", g);
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
-            core = 0; result.reset();
+            result.reset();
             tactic_report report("pb2bv", *g);
             m_bm.reset(); m_rw.reset(); m_new_deps.reset();
 
@@ -999,9 +998,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 58fdf14ca..926fea829 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -52,7 +52,7 @@ public:
     virtual void updt_params(params_ref const & p);
     virtual void collect_param_descrs(param_descrs & r) {}
 
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core);
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result);
     
     virtual void cleanup();
 };
@@ -527,12 +527,11 @@ void propagate_ineqs_tactic::updt_params(params_ref const & p) {
 }
 
 void propagate_ineqs_tactic::operator()(goal_ref const & g, 
-                                        goal_ref_buffer & result, 
-                                        expr_dependency_ref & core) {
+                                        goal_ref_buffer & result) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("propagate-ineqs", g);
     fail_if_unsat_core_generation("propagate-ineqs", g);
-    core = 0; result.reset();
+    result.reset();
     goal_ref r;
     (*m_imp)(g.get(), r);
     result.push_back(r.get());
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index 0caa0194d..692d6ab6d 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -821,11 +821,9 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("purify-arith", *g);
             TRACE("purify_arith", g->display(tout););
             bool produce_proofs = g->proofs_enabled();
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 2fde96caf..7645f34cd 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -292,13 +292,12 @@ class recover_01_tactic : public tactic {
         }
     
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("recover-01", g);
             fail_if_unsat_core_generation("recover-01", g);
             m_produce_models      = g->models_enabled();
-            core = 0; result.reset();
+            result.reset();
             tactic_report report("recover-01", *g);
             
             bool saved = false;
@@ -401,10 +400,9 @@ public:
     }
 
     void operator()(goal_ref const & g, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) {
+                    goal_ref_buffer & result) {
         try {
-            (*m_imp)(g, result, core);
+            (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 7928185b3..989427ee7 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -51,9 +51,7 @@ class bit_blaster_tactic : public tactic {
         
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+                        goal_ref_buffer & result) {
             bool proofs_enabled = g->proofs_enabled();
 
             if (proofs_enabled && m_blast_quant)
@@ -131,10 +129,9 @@ public:
     }
      
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(g, result, core);
+            (*m_imp)(g, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 9e31330fd..d23d7a308 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -379,9 +379,7 @@ class bv1_blaster_tactic : public tactic {
         
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+                        goal_ref_buffer & result) {
             
             if (!is_target(*g))
                 throw tactic_exception("bv1 blaster cannot be applied to goal");
@@ -453,9 +451,8 @@ public:
        Return a model_converter that converts any model for the updated set into a model for the old set.
     */
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(g, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp
index 151b00f50..beacc52ad 100644
--- a/src/tactic/bv/bv_bound_chk_tactic.cpp
+++ b/src/tactic/bv/bv_bound_chk_tactic.cpp
@@ -136,9 +136,7 @@ class bv_bound_chk_tactic : public tactic {
 public:
     bv_bound_chk_tactic(ast_manager & m, params_ref const & p);
     virtual ~bv_bound_chk_tactic();
-    void operator()(goal_ref const & g,
-        goal_ref_buffer & result,
-        expr_dependency_ref & core);
+    void operator()(goal_ref const & g, goal_ref_buffer & result) override;
     virtual tactic * translate(ast_manager & m);
     virtual void updt_params(params_ref const & p);
     void cleanup();
@@ -195,14 +193,12 @@ bv_bound_chk_tactic::~bv_bound_chk_tactic() {
     dealloc(m_imp);
 }
 
-void bv_bound_chk_tactic::operator()(goal_ref const & g,
-        goal_ref_buffer & result,
-        expr_dependency_ref & core) {
+void bv_bound_chk_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("bv-bound-chk", g);
     fail_if_unsat_core_generation("bv-bound-chk", g);
     TRACE("bv-bound-chk", g->display(tout << "before:"); tout << std::endl;);
-    core = 0; result.reset();
+    result.reset();
     m_imp->operator()(g);
     g->inc_depth();
     result.push_back(g.get());
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index e7cda8a2f..8c4ea22ad 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -39,7 +39,7 @@ public:
 
     virtual ~bv_size_reduction_tactic();
 
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core);
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result);
 
     virtual void cleanup();
 };
@@ -382,12 +382,11 @@ bv_size_reduction_tactic::~bv_size_reduction_tactic() {
 }
 
 void bv_size_reduction_tactic::operator()(goal_ref const & g, 
-                                          goal_ref_buffer & result, 
-                                          expr_dependency_ref & core) {
+                                          goal_ref_buffer & result) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("bv-size-reduction", g);
     fail_if_unsat_core_generation("bv-size-reduction", g);
-    core = 0; result.reset();
+    result.reset();
     model_converter_ref mc;
     m_imp->operator()(*(g.get()), mc);
     g->inc_depth();
diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp
index 421b3e1e7..7718a9679 100644
--- a/src/tactic/bv/bvarray2uf_tactic.cpp
+++ b/src/tactic/bv/bvarray2uf_tactic.cpp
@@ -53,12 +53,11 @@ class bvarray2uf_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core)
+                        goal_ref_buffer & result)
         {
             SASSERT(g->is_well_sorted());
             tactic_report report("bvarray2uf", *g);
-            core = 0; result.reset();
+            result.reset();
             fail_if_unsat_core_generation("bvarray2uf", g);
 
             TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
@@ -129,9 +128,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
     virtual void cleanup() {
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index a50658b5a..bbfbe02fd 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -116,10 +116,7 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {
     }
 
-    virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        core = 0;
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
         bool produce_proofs = g->proofs_enabled();
         tactic_report report("dt2bv", *g);
         unsigned   size = g->size();
diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp
index 2d8224f42..7da9aa1ae 100644
--- a/src/tactic/bv/elim_small_bv_tactic.cpp
+++ b/src/tactic/bv/elim_small_bv_tactic.cpp
@@ -224,11 +224,8 @@ class elim_small_bv_tactic : public tactic {
             m_rw.cfg().updt_params(p);
         }
 
-        void operator()(goal_ref const & g,
-            goal_ref_buffer & result,
-            expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("elim-small-bv", *g);
             bool produce_proofs = g->proofs_enabled();
             fail_if_proof_generation("elim-small-bv", g);
@@ -286,9 +283,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-        goal_ref_buffer & result,
-        expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+        goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
     virtual void cleanup() {
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index e9452dbbc..e9922b7e1 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -237,10 +237,8 @@ class max_bv_sharing_tactic : public tactic {
         ast_manager & m() const { return m_rw.m(); }
                 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("max-bv-sharing", *g);
             bool produce_proofs = g->proofs_enabled();
             
@@ -297,9 +295,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index e24ae0eb2..f8c5d33c0 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -113,11 +113,8 @@ class blast_term_ite_tactic : public tactic {
             m_rw.cfg().updt_params(p);
         }
         
-        void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("blast-term-ite", *g);
             bool produce_proofs = g->proofs_enabled();
 
@@ -170,9 +167,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp
index e43d0c1ef..f04dd6313 100644
--- a/src/tactic/core/cofactor_term_ite_tactic.cpp
+++ b/src/tactic/core/cofactor_term_ite_tactic.cpp
@@ -54,14 +54,11 @@ public:
     virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
     virtual void collect_param_descrs(param_descrs & r) { m_elim_ite.collect_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void  operator()(goal_ref const & g, goal_ref_buffer& result) override {
         SASSERT(g->is_well_sorted());
         fail_if_proof_generation("cofactor-term-ite", g);
         fail_if_unsat_core_generation("cofactor-term-ite", g);
         tactic_report report("cofactor-term-ite", *g);
-        core = 0;
         process(*(g.get()));
         g->inc_depth();
         result.push_back(g.get());
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index faba93dc5..85e2d6199 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/src/tactic/core/collect_statistics_tactic.cpp
@@ -63,8 +63,7 @@ public:
 
     virtual void collect_param_descrs(param_descrs & r) {}
 
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result) {
         tactic_report report("collect-statistics", *g);
 
         collect_proc cp(m, m_stats);
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 1216a7556..eece6a889 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -621,9 +621,7 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
 }
 
 void ctx_simplify_tactic::operator()(goal_ref const & in,
-                                     goal_ref_buffer & result,
-                                     expr_dependency_ref & core) {
-    core = 0;
+                                     goal_ref_buffer & result) {
     (*m_imp)(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());
diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h
index 21468d6da..bde74508e 100644
--- a/src/tactic/core/ctx_simplify_tactic.h
+++ b/src/tactic/core/ctx_simplify_tactic.h
@@ -55,8 +55,7 @@ public:
     virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core);
+                            goal_ref_buffer & result);
 
     virtual void cleanup();
 };
diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index 1b51c92e6..aa6838d0b 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -74,9 +74,7 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        core = 0;
+                            goal_ref_buffer & result) {
         (*m_imp)(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());
diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp
index dd887a0e1..3c5f8057a 100644
--- a/src/tactic/core/distribute_forall_tactic.cpp
+++ b/src/tactic/core/distribute_forall_tactic.cpp
@@ -100,14 +100,13 @@ public:
     }
 
     virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
         ast_manager & m = g->m();
         bool produce_proofs = g->proofs_enabled();
         rw r(m, produce_proofs);
         m_rw = &r;
-        core = 0; result.reset();
+        result.reset();
         tactic_report report("distribute-forall", *g);
 
         expr_ref   new_curr(m);
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index c18f6cd29..caeb4c245 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -183,17 +183,11 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) {
     return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
 }
 
-void dom_simplify_tactic::operator()(
-    goal_ref const & in,
-    goal_ref_buffer & result,
-    expr_dependency_ref & core) {
-    core = 0;
-
+void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) {
     tactic_report report("dom-simplify", *in.get());
     simplify_goal(*(in.get()));
     in->inc_depth();
     result.push_back(in.get());
-
 }
 
 void dom_simplify_tactic::cleanup() {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 10a56a979..e2fbe81fa 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -137,9 +137,7 @@ public:
     static  void get_param_descrs(param_descrs & r) {}
     virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core);
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
 
     virtual void cleanup();
 };
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 3035a8582..e4e337e00 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -100,10 +100,8 @@ class elim_term_ite_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("elim-term-ite", *g);
             bool produce_proofs = g->proofs_enabled();
             m_rw.cfg().m_produce_models = g->models_enabled();
@@ -160,9 +158,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index a3bb482f1..cc5402e41 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -816,9 +816,7 @@ class elim_uncnstr_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
-            core = 0;
+                        goal_ref_buffer & result) {
             bool produce_models = g->models_enabled();
             bool produce_proofs = g->proofs_enabled();
 
@@ -929,9 +927,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(g, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(g, result);
         report_tactic_progress(":num-elim-apps", get_num_elim_apps());
     }
     
diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp
index 9c233ac1c..0f7cec782 100644
--- a/src/tactic/core/injectivity_tactic.cpp
+++ b/src/tactic/core/injectivity_tactic.cpp
@@ -144,10 +144,8 @@ class injectivity_tactic : public tactic {
         }
 
         void operator()(goal_ref const & goal,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(goal->is_well_sorted());
-            core = 0;
             tactic_report report("injectivity", *goal);
             fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores
             fail_if_proof_generation("injectivity", goal);
@@ -269,9 +267,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_finder)(g, result, core);
+                            goal_ref_buffer & result) {
+        (*m_finder)(g, result);
 
         for (unsigned i = 0; i < g->size(); ++i) {
             expr*     curr = g->form(i);
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index 37251b8e9..c13f49b52 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -54,11 +54,9 @@ public:
     virtual void collect_param_descrs(param_descrs & r) { nnf::get_param_descrs(r); }
 
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout););
         SASSERT(g->is_well_sorted());
-        core = 0;
         tactic_report report("nnf", *g);
         bool produce_proofs = g->proofs_enabled();
 
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index a1cf0931a..e875a0472 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -128,10 +128,8 @@ class occf_tactic : public tactic {
         }
         
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             
             fail_if_proof_generation("occf", g);
 
@@ -209,9 +207,8 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {}
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp
index e622eb9a3..4ed55b0d2 100644
--- a/src/tactic/core/pb_preprocess_tactic.cpp
+++ b/src/tactic/core/pb_preprocess_tactic.cpp
@@ -147,12 +147,10 @@ public:
         return alloc(pb_preprocess_tactic, m);
     }
     
-    virtual void operator()(
+    void operator()(
         goal_ref const & g, 
-        goal_ref_buffer & result, 
-        expr_dependency_ref & core) {
+        goal_ref_buffer & result) override {
         SASSERT(g->is_well_sorted());
-        core = 0;
 
         if (g->proofs_enabled()) {
             throw tactic_exception("pb-preprocess does not support proofs");
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 12a14f5a6..45ff6250a 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -136,10 +136,8 @@ class propagate_values_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("propagate-values", *g);
             m_goal = g.get();
 
@@ -238,11 +236,9 @@ public:
         r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds.");
     }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 25f0a8f36..1e7baa14f 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -73,8 +73,8 @@ public:
 
     virtual ~reduce_args_tactic();
     
-    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, expr_dependency_ref & core);
-    virtual void cleanup();
+    void operator()(goal_ref const & g, goal_ref_buffer & result) override;
+    void cleanup() override;
 };
 
 tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
@@ -483,12 +483,11 @@ reduce_args_tactic::~reduce_args_tactic() {
 }
 
 void reduce_args_tactic::operator()(goal_ref const & g, 
-                                    goal_ref_buffer & result, 
-                                    expr_dependency_ref & core) {
+                                    goal_ref_buffer & result) {
     SASSERT(g->is_well_sorted());
     fail_if_proof_generation("reduce-args", g);
     fail_if_unsat_core_generation("reduce-args", g);
-    core = 0; result.reset();
+    result.reset();
     m_imp->operator()(*(g.get()));
     g->inc_depth();
     result.push_back(g.get());
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index a8278c383..93495922b 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -93,13 +93,11 @@ void simplify_tactic::get_param_descrs(param_descrs & r) {
 }
 
 void simplify_tactic::operator()(goal_ref const & in, 
-                                 goal_ref_buffer & result, 
-                                 expr_dependency_ref & core) {
+                                 goal_ref_buffer & result) {
     try {
         (*m_imp)(*(in.get()));
         in->inc_depth();
         result.push_back(in.get());
-        core = 0;
     }
     catch (rewriter_exception & ex) {
         throw tactic_exception(ex.msg());
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index 282feda0f..872eb6bab 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -30,19 +30,19 @@ public:
     simplify_tactic(ast_manager & m, params_ref const & ref = params_ref());
     virtual ~simplify_tactic();
 
-    virtual void updt_params(params_ref const & p);
+    void updt_params(params_ref const & p) override;
+
     static void get_param_descrs(param_descrs & r);
-    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core);
+    void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); }
     
-    virtual void cleanup();
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override;
+    
+    void cleanup() override;
 
     unsigned get_num_steps() const;
 
-    virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+    tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); }
 
 };
 
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index fec0edd81..22b87d60e 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -666,11 +666,8 @@ class solve_eqs_tactic : public tactic {
             return m_num_eliminated_vars;
         }
         
-        void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             model_converter_ref mc;
             tactic_report report("solve_eqs", *g);
             m_produce_models = g->models_enabled();
@@ -732,10 +729,9 @@ public:
         r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
     }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+    void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result) override {
+        (*m_imp)(in, result);
         report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
     }
     
diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp
index 60dbdd568..4f0edf797 100644
--- a/src/tactic/core/split_clause_tactic.cpp
+++ b/src/tactic/core/split_clause_tactic.cpp
@@ -101,12 +101,10 @@ public:
     }
     
     void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) override {
+                    goal_ref_buffer & result) override {
         SASSERT(in->is_well_sorted());
         tactic_report report("split-clause", *in);
         TRACE("before_split_clause", in->display(tout););
-        core = 0; 
         ast_manager & m = in->m();
         unsigned cls_pos = select_clause(m, in);
         if (cls_pos == UINT_MAX) {
@@ -129,6 +127,7 @@ public:
             result.push_back(subgoal_i);
         }
         in->set(concat(in->pc(), result.size(), result.c_ptr()));
+        in->add(dependency_converter::concat(result.size(), result.c_ptr()));
     }
     
     virtual void cleanup() {
diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 920521e0c..cf48a8a09 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -39,8 +39,7 @@ public:
     virtual ~symmetry_reduce_tactic();
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core);
+                            goal_ref_buffer & result);
     virtual void cleanup();
 };
 
@@ -633,11 +632,10 @@ symmetry_reduce_tactic::~symmetry_reduce_tactic() {
 }
     
 void symmetry_reduce_tactic::operator()(goal_ref const & g, 
-                                        goal_ref_buffer & result, 
-                                        expr_dependency_ref & core) {
+                                        goal_ref_buffer & result) {
     fail_if_proof_generation("symmetry_reduce", g);
     fail_if_unsat_core_generation("symmetry_reduce", g);
-    core = 0; result.reset();
+    result.reset();
     (*m_imp)(*(g.get()));
     g->inc_depth();
     result.push_back(g.get());
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index 11b7ceb8c..91f974eb9 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -799,10 +799,8 @@ class tseitin_cnf_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("tseitin-cnf", *g);
             fail_if_proof_generation("tseitin-cnf", g);
             m_produce_models      = g->models_enabled();
@@ -880,9 +878,8 @@ public:
     }
     
     virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
         report_tactic_progress(":cnf-aux-vars", m_imp->m_num_aux_vars);
     }
     
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 3ed9f9cb0..9a0579346 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -47,14 +47,13 @@ class fpa2bv_tactic : public tactic {
         }
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
             m_proofs_enabled      = g->proofs_enabled();
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
 
-            core = 0; result.reset();
+            result.reset();
             tactic_report report("fpa2bv", *g);
             m_rw.reset();
 
@@ -138,10 +137,9 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         try {
-            (*m_imp)(in, result, core);
+            (*m_imp)(in, result);
         }
         catch (rewriter_exception & ex) {
             throw tactic_exception(ex.msg());
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index 778c3804b..c7b730099 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -107,6 +107,7 @@ void goal::copy_to(goal & target) const {
     target.m_precision            = mk_union(prec(), target.prec());
     target.m_mc                   = m_mc.get(); 
     target.m_pc                   = m_pc.get(); 
+    target.m_dc                   = m_dc.get();
 }
 
 void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
@@ -655,6 +656,7 @@ goal * goal::translate(ast_translation & translator) const {
     res->m_precision    = m_precision;
     res->m_pc           = m_pc ? m_pc->translate(translator) : nullptr;
     res->m_mc           = m_mc ? m_mc->translate(translator) : nullptr;
+    res->m_dc           = m_dc ? m_dc->translate(translator) : nullptr;
 
     return res;
 }
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index 73fbb6f17..06c51b4b6 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -37,6 +37,7 @@ Revision History:
 #include "util/ref_buffer.h"
 #include "tactic/model_converter.h"
 #include "tactic/proof_converter.h"
+#include "tactic/dependency_converter.h"
 
 class goal {
 public:
@@ -53,6 +54,7 @@ protected:
     ast_manager &         m_manager;
     model_converter_ref   m_mc;
     proof_converter_ref   m_pc;
+    dependency_converter_ref m_dc;
     unsigned              m_ref_count;
     expr_array            m_forms;
     expr_array            m_proofs;
@@ -147,10 +149,13 @@ public:
     bool is_decided() const;
     bool is_well_sorted() const;
 
+    dependency_converter* dc() { return m_dc.get(); }
     model_converter* mc() { return m_mc.get(); }
     proof_converter* pc() { return inconsistent() ? proof2proof_converter(m(), pr(0)) : m_pc.get(); }
+    void add(dependency_converter* d) { m_dc = dependency_converter::concat(m_dc.get(), d); }
     void add(model_converter* m) { m_mc = concat(m_mc.get(), m); }
     void add(proof_converter* p) { m_pc = concat(m_pc.get(), p); }
+    void set(dependency_converter* d) { m_dc = d; }
     void set(model_converter* m) { m_mc = m; }
     void set(proof_converter* p) { m_pc = p; }
 
diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h
index 7069e868e..c768a0cae 100644
--- a/src/tactic/model_converter.h
+++ b/src/tactic/model_converter.h
@@ -15,6 +15,42 @@ Author:
 
 Notes:
 
+    A model converter, mc, can be used to convert a model for one 
+    of a generated subgoal into a model for an initial goal or solver state.
+    For a goal or solver state that is decided, a model converter can be
+    a simple wrapper around a model.
+
+    Logically, given a formula F and subgoal formula F_s a model converter mc
+    for F_s relative to F has the property:
+
+        m |= F_s  iff mc(m) |= F     for every model m
+
+    For the evaluator associated with models, m, we expect
+
+        eval(m)(F_s) <=> eval(mc(m))(F)
+
+    This property holds for both eval, that decides on a fixed value
+    for constants that have no interpretation in m and for 'peval' 
+    (partial eval) that retuns just the constants that are unfixed.
+    (in the model evaluator one can control this behavior using a 
+    configuration flag)
+
+    and more generally over the eval method have:
+
+        G => F_s   iff peval(mc(e))(G) => F   for every formula G
+
+    
+    where e is the empty model (a model that does not evaluate any
+
+    When a model converter supports application to a formula it satisfies
+    the following property:
+
+       mc(G) & F_s is SAT  iff G & F is SAT
+
+    For a model converter that is a sequence of definitions and removals
+    of functions we can obtain mc(G) by adding back or expanding definitinos
+    that are required to interpret G fully in the context of F_s.
+
 --*/
 #ifndef MODEL_CONVERTER_H_
 #define MODEL_CONVERTER_H_
diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp
index abb8df188..8e14d77e2 100644
--- a/src/tactic/portfolio/parallel_tactic.cpp
+++ b/src/tactic/portfolio/parallel_tactic.cpp
@@ -541,7 +541,7 @@ public:
         init();        
     }
 
-    void operator ()(const goal_ref & g,goal_ref_buffer & result, expr_dependency_ref & dep) {
+    void operator ()(const goal_ref & g,goal_ref_buffer & result) {
         ast_manager& m = g->m();
         solver* s = mk_fd_solver(m, m_params);
         solver_state* st = alloc(solver_state, 0, s, m_params, cube_task);
diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp
index 532169d46..7099f0fdf 100644
--- a/src/tactic/sine_filter.cpp
+++ b/src/tactic/sine_filter.cpp
@@ -46,11 +46,7 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {
     }
 
-    virtual void operator()(goal_ref const & g,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        core = 0;
-
+    void operator()(goal_ref const & g, goal_ref_buffer& result) override {
         TRACE("sine", g->display(tout););
         TRACE("sine", tout << g->size(););
         ptr_vector<expr> new_forms;
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 18328f0b8..2fb0d4269 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -60,10 +60,9 @@ public:
     }
     
     virtual void operator()(goal_ref const & g, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+                            goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());        
-        core = 0; result.reset();
+        result.reset();
         
         TRACE("sls", g->display(tout););
         tactic_report report("sls", *g);
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 84d445f45..7e64b9c2c 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -54,8 +54,7 @@ public:
     virtual ~qfufbv_ackr_tactic() { }
 
     virtual void operator()(goal_ref const & g,
-        goal_ref_buffer & result,
-        expr_dependency_ref & core) {
+        goal_ref_buffer & result) {
         ast_manager& m(g->m());
         tactic_report report("qfufbv_ackr", *g);
         fail_if_unsat_core_generation("qfufbv_ackr", g);
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index ed78f229d..c4ae3e106 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -67,12 +67,8 @@ void report_tactic_progress(char const * id, unsigned val) {
     }
 }
 
-void skip_tactic::operator()(goal_ref const & in, 
-                             goal_ref_buffer & result, 
-                             expr_dependency_ref & core) {
-    result.reset();
+void skip_tactic::operator()(goal_ref const & in, goal_ref_buffer& result) {
     result.push_back(in.get());
-    core = 0;
 }
 
 tactic * mk_skip_tactic() {
@@ -81,9 +77,7 @@ tactic * mk_skip_tactic() {
 
 class fail_tactic : public tactic {
 public:
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         throw tactic_exception("fail tactic");
     }
 
@@ -102,11 +96,9 @@ class report_verbose_tactic : public skip_tactic {
 public:
     report_verbose_tactic(char const * msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {}
 
-    void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) override {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";);
-        skip_tactic::operator()(in, result, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
@@ -119,12 +111,10 @@ class trace_tactic : public skip_tactic {
 public:
     trace_tactic(char const * tag): m_tag(tag) {}
     
-    void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) override {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         TRACE(m_tag, in->display(tout););
         (void)m_tag;
-        skip_tactic::operator()(in, result, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
@@ -136,12 +126,10 @@ class fail_if_undecided_tactic : public skip_tactic {
 public:
     fail_if_undecided_tactic() {}
 
-    void operator()(goal_ref const & in, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) override {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (!in->is_decided()) 
             throw tactic_exception("undecided");
-        skip_tactic::operator()(in, result, core);
+        skip_tactic::operator()(in, result);
     }
 };
 
@@ -149,10 +137,10 @@ tactic * mk_fail_if_undecided_tactic() {
     return alloc(fail_if_undecided_tactic);
 }
 
-void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core) {
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) {
     t.reset_statistics();
     try {
-        t(in, result, core);
+        t(in, result);
         t.cleanup();
     }
     catch (tactic_exception & ex) {
@@ -173,7 +161,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
     ast_manager & m = g->m();
     goal_ref_buffer r;
     try {
-        exec(t, g, r, core);
+        exec(t, g, r);
     }
     catch (tactic_exception & ex) {
         reason_unknown = ex.msg();
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 98c57f12c..c9b5a23fd 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -61,9 +61,7 @@ public:
        
        Therefore, in most cases, pc == 0 and core == 0 for non-branching tactics.
     */
-    virtual void operator()(/* in */  goal_ref const & in, 
-                            /* out */ goal_ref_buffer & result, 
-                            /* out */ expr_dependency_ref & core) = 0;
+    virtual void operator()(goal_ref const & in, goal_ref_buffer& result) = 0;
 
     virtual void collect_statistics(statistics & st) const {}
     virtual void reset_statistics() {}
@@ -103,7 +101,7 @@ void report_tactic_progress(char const * id, unsigned val);
 
 class skip_tactic : public tactic {
 public:
-    void operator()(goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core) override;
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override;
     void cleanup() override {}
     tactic * translate(ast_manager & m) override { return this; } 
 };
@@ -136,7 +134,7 @@ public:
 
 #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
 
-void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, expr_dependency_ref & core);
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result);
 lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
 
 // Throws an exception if goal \c in requires proof generation.
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index 5003a4f9d..96979a3ff 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -101,59 +101,45 @@ public:
     and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {}
     virtual ~and_then_tactical() {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
 
         bool models_enabled = in->models_enabled();
         bool proofs_enabled = in->proofs_enabled();
         bool cores_enabled  = in->unsat_core_enabled();
 
-        ast_manager & m = in->m();                                                                          
-        goal_ref_buffer      r1;
-        expr_dependency_ref core1(m);                                                                      
-        result.reset();                                                                                     
-        core = 0;
-        m_t1->operator()(in, r1, core1);                                                            
-        SASSERT(!is_decided(r1) || !core1); // the pc and core of decided goals is 0
+        ast_manager & m = in->m();                                                                         
+        goal_ref_buffer r1;
+        m_t1->operator()(in, r1);
         unsigned r1_size = r1.size();                                                                       
-        SASSERT(r1_size > 0);                                                                               
+        SASSERT(r1_size > 0);  
         if (r1_size == 1) {                                                                                 
             if (r1[0]->is_decided()) {
                 result.push_back(r1[0]);
-                return;                                                                                     
+                return;
             }                                                                                               
             goal_ref r1_0 = r1[0];      
-            m_t2->operator()(r1_0, result, core);
-            if (cores_enabled) core = m.mk_join(core1.get(), core); 
+            m_t2->operator()(r1_0, result);
         }
         else {
-            if (cores_enabled) core = core1;
-            goal_ref_buffer            r2;                                                                  
+            goal_ref_buffer r2;
             for (unsigned i = 0; i < r1_size; i++) {                                                        
-                goal_ref g = r1[i];                                                                         
-                r2.reset();             
-                expr_dependency_ref core2(m);                                                              
-                m_t2->operator()(g, r2, core2);                                              
+                goal_ref g = r1[i];                                                                       
+                r2.reset();
+                m_t2->operator()(g, r2);
                 if (is_decided(r2)) {
                     SASSERT(r2.size() == 1);
                     if (is_decided_sat(r2)) {                                                          
-                        // found solution...                                                                
+                        // found solution...                                                           
+                        result.reset();
                         result.push_back(r2[0]);
-                        SASSERT(!core);
-                        return;                                                                             
+                        return;
                     }                                                                                   
                     else {                                                                                  
                         SASSERT(is_decided_unsat(r2));                                                 
-                        // the proof and unsat core of a decided_unsat goal are stored in the node itself.
-                        // core2 must be 0.
-                        SASSERT(!core2);
-                        if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0));
                     }                                                                         
                 }                                                                                       
                 else {                                                                                      
                     result.append(r2.size(), r2.c_ptr());
-                    if (cores_enabled) core = m.mk_join(core.get(), core2.get());
                 }                                                                                           
             }
                         
@@ -162,17 +148,16 @@ public:
                 // create an decided_unsat goal with the proof
                 in->reset_all();
                 proof_ref pr(m);
+                expr_dependency_ref core(m);
                 if (proofs_enabled) {
                     apply(m, in->pc(), pr);
                 }
-                SASSERT(cores_enabled || core == 0);
+                dependency_converter* dc = in->dc();
+                if (cores_enabled && dc) {
+                    core = (*dc)();
+                }
                 in->assert_expr(m.mk_false(), pr, core);
-                core = 0;
                 result.push_back(in.get());
-                SASSERT(!core);
-            }
-            else {
-                SASSERT(cores_enabled || core == 0);
             }
         }
     }
@@ -300,30 +285,24 @@ public:
 
     virtual ~or_else_tactical() {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    virtual void operator()(goal_ref const & in, goal_ref_buffer& result) {
         goal orig(*(in.get()));
-        proof_converter_ref pc = in->pc();
         unsigned sz = m_ts.size();
         unsigned i;
         for (i = 0; i < sz; i++) {
             tactic * t = m_ts[i];
-            result.reset();
-            pc   = 0;
-            core = 0;
             SASSERT(sz > 0);
             if (i < sz - 1) {
                 try {
-                    t->operator()(in, result, core);
+                    t->operator()(in, result);
                     return;
                 }
                 catch (tactic_exception &) {
-                    in->set(pc.get());
+                    result.reset();
                 }
             }
             else {
-                t->operator()(in, result, core);
+                t->operator()(in, result);
                 return;
             }
             in->reset_all();
@@ -398,9 +377,7 @@ public:
 
     
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
 #ifdef _NO_OMP_
         use_seq = true;
@@ -409,7 +386,7 @@ public:
 #endif
         if (use_seq) {
             // execute tasks sequentially
-            or_else_tactical::operator()(in, result, core);
+            or_else_tactical::operator()(in, result);
             return;
         }
         
@@ -437,13 +414,12 @@ public:
         #pragma omp parallel for
         for (int i = 0; i < static_cast<int>(sz); i++) {
             goal_ref_buffer     _result;
-            expr_dependency_ref _core(*(managers[i]));
             
             goal_ref in_copy = in_copies[i];
             tactic & t = *(ts.get(i));
             
             try {
-                t(in_copy, _result, _core);
+                t(in_copy, _result);
                 bool first = false;
                 #pragma omp critical (par_tactical)
                 {
@@ -462,8 +438,8 @@ public:
                     for (goal* g : _result) {
                         result.push_back(g->translate(translator));
                     }
-                    expr_dependency_translation td(translator);
-                    core = td(_core);
+                    goal_ref in2(in_copy->translate(translator));
+                    in->copy_from(*(in2.get()));
                 }
             }
             catch (tactic_exception & ex) {
@@ -522,9 +498,7 @@ public:
     par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {}
     virtual ~par_and_then_tactical() {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         bool use_seq;
 #ifdef _NO_OMP_
         use_seq = true;
@@ -533,7 +507,7 @@ public:
 #endif
         if (use_seq) {
             // execute tasks sequentially
-            and_then_tactical::operator()(in, result, core);
+            and_then_tactical::operator()(in, result);
             return;
         }
 
@@ -544,27 +518,20 @@ public:
         bool cores_enabled  = in->unsat_core_enabled();
 
         ast_manager & m = in->m();                                                                          
-        goal_ref_buffer      r1;
-        expr_dependency_ref core1(m);                                                                      
-        result.reset();                                                                                     
-        core = 0;
-        m_t1->operator()(in, r1, core1);                                                            
-        SASSERT(!is_decided(r1) || !core1); // the core of decided goals is 0
-        unsigned r1_size = r1.size();                                                                       
+        goal_ref_buffer r1;
+        m_t1->operator()(in, r1);                
+        unsigned r1_size = r1.size();                                                                               
         SASSERT(r1_size > 0);                                                                               
         if (r1_size == 1) {                                                                                 
             // Only one subgoal created... no need for parallelism
             if (r1[0]->is_decided()) {
-                result.push_back(r1[0]);                                                                    
-                SASSERT(!core);
-                return;                                                                                     
+                result.push_back(r1[0]);
+                return;
             }                                                                                               
             goal_ref r1_0 = r1[0];                                                                          
-            m_t2->operator()(r1_0, result, core);  
-            if (cores_enabled) core = m.mk_join(core1.get(), core); 
+            m_t2->operator()(r1_0, result);
         }                                                                                     
         else {                                                                                              
-            if (cores_enabled) core = core1;  
 
             scoped_ptr_vector<ast_manager> managers;
             tactic_ref_vector              ts2;
@@ -596,12 +563,11 @@ public:
                 goal_ref new_g = g_copies[i];
 
                 goal_ref_buffer r2;
-                expr_dependency_ref core2(new_m);                                                              
                 
                 bool curr_failed = false;
 
                 try {
-                    ts2[i]->operator()(new_g, r2, core2);                                              
+                    ts2[i]->operator()(new_g, r2);                  
                 }
                 catch (tactic_exception & ex) {
                     #pragma omp critical (par_and_then_tactical)
@@ -667,14 +633,10 @@ public:
                                 ast_translation translator(new_m, m, false);
                                 SASSERT(r2.size() == 1);
                                 result.push_back(r2[0]->translate(translator));                                
-                                SASSERT(!core);
                             }       
                         }                                                     
                         else {                                                                                  
                             SASSERT(is_decided_unsat(r2));                                                 
-                            // the proof and unsat core of a decided_unsat goal are stored in the node itself.
-                            // core2 must be 0.
-                            SASSERT(!core2);
                             
                             if (cores_enabled && r2[0]->dep(0) != 0) {
                                 expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m);
@@ -687,9 +649,10 @@ public:
                         goal_ref_buffer * new_r2 = alloc(goal_ref_buffer);
                         goals_vect.set(i, new_r2);
                         new_r2->append(r2.size(), r2.c_ptr());
-                        if (cores_enabled && core2 != 0) {
+                        dependency_converter* dc = r1[i]->dc();                           
+                        if (cores_enabled && dc) {
                             expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m);
-                            *new_dep = core2;
+                            *new_dep = (*dc)();
                             core_buffer.set(i, new_dep);
                         }
                     }                                                                                           
@@ -707,8 +670,8 @@ public:
 
             if (found_solution)
                 return;
-
-            core = 0;
+            
+            expr_dependency_ref core(m);
             for (unsigned i = 0; i < r1_size; i++) {
                 ast_translation translator(*(managers[i]), m, false);
                 goal_ref_buffer * r = goals_vect[i];
@@ -730,7 +693,9 @@ public:
                     core = m.mk_join(curr_core, core);
                 }
             }
-
+            if (core) {
+                in->add(dependency_converter::unit(core));
+            }
 
             if (result.empty()) {
                 // all subgoals were shown to be unsat.                                                     
@@ -740,14 +705,12 @@ public:
                 if (proofs_enabled) {
                     apply(m, in->pc(), pr);
                 }
-                SASSERT(cores_enabled || core == 0);
+                dependency_converter* dc = in->dc();
+                if (cores_enabled && dc) {
+                    core = (*dc)();
+                }
                 in->assert_expr(m.mk_false(), pr, core);
-                core = 0;
                 result.push_back(in.get());
-                SASSERT(!core);
-            }
-            else {
-                SASSERT(cores_enabled || core == 0);
             }
         }
     }
@@ -786,10 +749,8 @@ public:
 
     virtual ~unary_tactical() { }
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        m_t->operator()(in, result, core);
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override { 
+        m_t->operator()(in, result);
     }
    
     virtual void cleanup(void) { m_t->cleanup(); }
@@ -814,12 +775,10 @@ class repeat_tactical : public unary_tactical {
     
     void operator()(unsigned depth,
                     goal_ref const & in, 
-                    goal_ref_buffer & result, 
-                    expr_dependency_ref & core) {
+                    goal_ref_buffer& result) {
         // TODO: implement a non-recursive version.
         if (depth > m_max_depth) {
             result.push_back(in.get());
-            core = 0;
             return;
         }
 
@@ -828,17 +787,14 @@ class repeat_tactical : public unary_tactical {
         bool cores_enabled  = in->unsat_core_enabled();
 
         ast_manager & m = in->m();                                                                          
-        goal_ref_buffer      r1;                                                                           
-        expr_dependency_ref core1(m);                                                                      
-        result.reset();                                                                                     
-        core = 0;
+        goal_ref_buffer      r1;  
+        result.reset();          
         {
             goal orig_in(in->m(), proofs_enabled, models_enabled, cores_enabled);
             orig_in.copy_from(*(in.get()));
-            m_t->operator()(in, r1, core1);                                                            
+            m_t->operator()(in, r1);                                                            
             if (r1.size() == 1 && is_equal(orig_in, *(r1[0]))) {
                 result.push_back(r1[0]);
-                if (cores_enabled) core = core1; 
                 return;                                                                                     
             }
         }
@@ -847,38 +803,30 @@ class repeat_tactical : public unary_tactical {
         if (r1_size == 1) {                                                                                 
             if (r1[0]->is_decided()) {
                 result.push_back(r1[0]);  
-                SASSERT(!core);
                 return;                                                                                     
             }                                                                                               
             goal_ref r1_0 = r1[0];                                                                          
-            operator()(depth+1, r1_0, result, core); 
-            if (cores_enabled) core = m.mk_join(core1.get(), core); 
+            operator()(depth+1, r1_0, result); 
         }                                                                                                   
         else {
-            if (cores_enabled) core = core1;
             goal_ref_buffer            r2;                                                                  
             for (unsigned i = 0; i < r1_size; i++) {                                                        
                 goal_ref g = r1[i];                                                                         
                 r2.reset();                   
-                expr_dependency_ref  core2(m);                                                              
-                operator()(depth+1, g, r2, core2);                                              
+                operator()(depth+1, g, r2);                                              
                 if (is_decided(r2)) {
                     SASSERT(r2.size() == 1);
                     if (is_decided_sat(r2)) {                                                          
                         // found solution...                                                                
                         result.push_back(r2[0]);
-                        SASSERT(!core);
                         return;                                                                             
                     }                                                                                       
                     else {                                                                                  
                         SASSERT(is_decided_unsat(r2));
-                        SASSERT(!core2);
-                        if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0));
                     }                                                                                       
                 }                                                                                           
                 else {                                                                                      
                     result.append(r2.size(), r2.c_ptr());                                                           
-                    if (cores_enabled) core = m.mk_join(core.get(), core2.get());                                              
                 }                                                                                           
             }    
                                                                                            
@@ -887,17 +835,15 @@ class repeat_tactical : public unary_tactical {
                 // create an decided_unsat goal with the proof
                 in->reset_all();
                 proof_ref pr(m);
+                expr_dependency_ref core(m);
                 if (proofs_enabled) {
                     apply(m, in->pc(), pr);                    
                 }
-                SASSERT(cores_enabled || core == 0);
+                if (cores_enabled && in->dc()) {
+                    core = (*in->dc())();
+                }
                 in->assert_expr(m.mk_false(), pr, core);
-                core = 0;
                 result.push_back(in.get());
-                SASSERT(!core);
-            }
-            else {
-                SASSERT(cores_enabled || core == 0);
             }
         }
     }
@@ -908,10 +854,8 @@ public:
         m_max_depth(max_depth) {
     }
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        operator()(0, in, result, core);
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        operator()(0, in, result);
     }
 
     virtual tactic * translate(ast_manager & m) { 
@@ -929,13 +873,10 @@ class fail_if_branching_tactical : public unary_tactical {
 public:
     fail_if_branching_tactical(tactic * t, unsigned threshold):unary_tactical(t), m_threshold(threshold) {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        m_t->operator()(in, result, core);
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        m_t->operator()(in, result);
         if (result.size() > m_threshold) {
-            result.reset();
-            core = 0;
+            result.reset(); // assumes in is not strenthened to one of the branches
             throw tactic_exception("failed-if-branching tactical");
         }
     };    
@@ -954,10 +895,8 @@ class cleanup_tactical : public unary_tactical {
 public:
     cleanup_tactical(tactic * t):unary_tactical(t) {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        m_t->operator()(in, result, core);
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
+        m_t->operator()(in, result);
         m_t->cleanup();
     }    
 
@@ -976,14 +915,12 @@ class try_for_tactical : public unary_tactical {
 public:
     try_for_tactical(tactic * t, unsigned ts):unary_tactical(t), m_timeout(ts) {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         cancel_eh<reslimit> eh(in->m().limit());
         { 
             // Warning: scoped_timer is not thread safe in Linux.
             scoped_timer timer(m_timeout, &eh);
-            m_t->operator()(in, result, core);
+            m_t->operator()(in, result);
         }
     }
 
@@ -1044,11 +981,9 @@ public:
     annotate_tactical(char const* name, tactic* t):
         unary_tactical(t), m_name(name) {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {        
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         scope _scope(m_name);
-        m_t->operator()(in, result, core);
+        m_t->operator()(in, result);
     }
 
     virtual tactic * translate(ast_manager & m) { 
@@ -1073,13 +1008,11 @@ public:
 
     virtual ~cond_tactical() {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         if (m_p->operator()(*(in.get())).is_true()) 
-            m_t1->operator()(in, result, core);
+            m_t1->operator()(in, result);
         else
-            m_t2->operator()(in, result, core);
+            m_t2->operator()(in, result);
     }
 
     virtual tactic * translate(ast_manager & m) { 
@@ -1109,10 +1042,7 @@ public:
 
     void cleanup() {}
 
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
-        core = 0;
+    void  operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (m_p->operator()(*(in.get())).is_true()) {
             throw tactic_exception("fail-if tactic");
         }
@@ -1136,16 +1066,12 @@ class if_no_proofs_tactical : public unary_tactical {
 public:
     if_no_proofs_tactical(tactic * t):unary_tactical(t) {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer & result) override {
         if (in->proofs_enabled()) {
-            core = 0;
-            result.reset();
             result.push_back(in.get());
         }
         else {
-            m_t->operator()(in, result, core);
+            m_t->operator()(in, result);
         }
     }
 
@@ -1156,16 +1082,12 @@ class if_no_unsat_cores_tactical : public unary_tactical {
 public:
     if_no_unsat_cores_tactical(tactic * t):unary_tactical(t) {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (in->unsat_core_enabled()) {
-            core = 0;
-            result.reset();
             result.push_back(in.get());
         }
         else {
-            m_t->operator()(in, result, core);
+            m_t->operator()(in, result);
         }
     }
 
@@ -1176,16 +1098,12 @@ class if_no_models_tactical : public unary_tactical {
 public:
     if_no_models_tactical(tactic * t):unary_tactical(t) {}
     
-    virtual void operator()(goal_ref const & in, 
-                            goal_ref_buffer & result, 
-                            expr_dependency_ref & core) {
+    void operator()(goal_ref const & in, goal_ref_buffer& result) override {
         if (in->models_enabled()) {
-            core = 0;
-            result.reset();
             result.push_back(in.get());
         }
         else {
-            m_t->operator()(in, result, core);
+            m_t->operator()(in, result);
         }
     }
 
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index fb5c7d458..efed67486 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -38,10 +38,8 @@ class macro_finder_tactic : public tactic {
 
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("macro-finder", *g);
 
             bool produce_proofs = g->proofs_enabled();
@@ -115,9 +113,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
     virtual void cleanup() {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 61dbcaf01..05c5bdd73 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -36,10 +36,8 @@ class quasi_macros_tactic : public tactic {
 
 
         void operator()(goal_ref const & g,
-                        goal_ref_buffer & result,
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("quasi-macros", *g);
 
             bool produce_proofs = g->proofs_enabled();
@@ -126,9 +124,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
     virtual void cleanup() {
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 6b9882e29..914c874ee 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -32,10 +32,8 @@ class ufbv_rewriter_tactic : public tactic {
         ast_manager & m() const { return m_manager; }
                 
         void operator()(goal_ref const & g, 
-                        goal_ref_buffer & result, 
-                        expr_dependency_ref & core) {
+                        goal_ref_buffer & result) {
             SASSERT(g->is_well_sorted());
-            core = 0;
             tactic_report report("ufbv-rewriter", *g);
             fail_if_unsat_core_generation("ufbv-rewriter", g);
 
@@ -100,9 +98,8 @@ public:
     }
 
     virtual void operator()(goal_ref const & in,
-                            goal_ref_buffer & result,
-                            expr_dependency_ref & core) {
-        (*m_imp)(in, result, core);
+                            goal_ref_buffer & result) {
+        (*m_imp)(in, result);
     }
 
     virtual void cleanup() {