diff --git a/lib/dl_util.h b/lib/dl_util.h
index c73f7e762..3e01fb8d2 100644
--- a/lib/dl_util.h
+++ b/lib/dl_util.h
@@ -507,13 +507,13 @@ namespace datalog {
     //
     // -----------------------------------
 
-    template<class Set>
-    void set_intersection(Set & tgt, const Set & src) {
-        svector<typename Set::data> to_remove;
-        typename Set::iterator vit = tgt.begin();
-        typename Set::iterator vend = tgt.end();
+    template<class Set1, class Set2>
+    void set_intersection(Set1 & tgt, const Set2 & src) {
+        svector<typename Set1::data> to_remove;
+        typename Set1::iterator vit = tgt.begin();
+        typename Set1::iterator vend = tgt.end();
         for(;vit!=vend;++vit) {
-            typename Set::data itm=*vit;
+            typename Set1::data itm=*vit;
             if(!src.contains(itm)) {
                 to_remove.push_back(itm);
             }
@@ -534,12 +534,12 @@ namespace datalog {
         }
     }
 
-    template<class Set>
-    void set_union(Set & tgt, const Set & to_add) {
-        typename Set::iterator vit = to_add.begin();
-        typename Set::iterator vend = to_add.end();
+    template<class Set1, class Set2>
+    void set_union(Set1 & tgt, const Set2 & to_add) {
+        typename Set2::iterator vit = to_add.begin();
+        typename Set2::iterator vend = to_add.end();
         for(;vit!=vend;++vit) {
-            typename Set::data itm=*vit;
+            typename Set1::data itm=*vit;
             tgt.insert(itm);
         }
     }
diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp
index 62d32ea63..af5dbe54d 100644
--- a/lib/pdr_context.cpp
+++ b/lib/pdr_context.cpp
@@ -69,6 +69,10 @@ namespace pdr {
         for (; it2 != end2; ++it2) {
             dealloc(it2->m_value);
         }
+        rule2expr::iterator it3 = m_rule2transition.begin(), end3 = m_rule2transition.end();
+        for (; it3 != end3; ++it3) {
+            m.dec_ref(it3->m_value);
+        }
     }
 
     std::ostream& pred_transformer::display(std::ostream& out) const {
@@ -118,7 +122,7 @@ namespace pdr {
         return m_reachable.is_reachable(state);
     }
 
-    datalog::rule const* pred_transformer::find_rule(model_core const& model) const {
+    datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
         obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
         TRACE("pdr",
               for (; it != end; ++it) {
@@ -130,7 +134,7 @@ namespace pdr {
         
         it = m_tag2rule.begin();
         if (m_tag2rule.size() == 1) {
-            return it->m_value;
+            return *it->m_value;
         }
 
         expr_ref vl(m);
@@ -138,11 +142,11 @@ namespace pdr {
             expr* pred = it->m_key;
             TRACE("pdr", tout << mk_pp(pred, m) << "\n";);
             if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) {
-                return it->m_value;
+                return *it->m_value;
             }
         }
         UNREACHABLE();
-        return 0;
+        return *((datalog::rule*)0);
     }
 
     void pred_transformer::find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& preds) const {
@@ -154,10 +158,7 @@ namespace pdr {
     }
 
     void pred_transformer::find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const {
-        datalog::rule const* r = find_rule(model);
-        if (r) {
-            find_predecessors(*r, preds);
-        }
+        find_predecessors(find_rule(model), preds);        
     }
 
     void pred_transformer::remove_predecessors(expr_ref_vector& literals) {
@@ -562,6 +563,8 @@ namespace pdr {
             SASSERT(is_ground(tmp));
         }         
         expr_ref fml = pm.mk_and(conj);
+        th_rewriter rw(m);
+        rw(fml);
         TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
         SASSERT(is_ground(fml));
         if (m.is_false(fml)) {
@@ -574,6 +577,8 @@ namespace pdr {
                 init = m.mk_or(init, fml);
             }
             transitions.push_back(fml);            
+            m.inc_ref(fml);
+            m_rule2transition.insert(&rule, fml.get());
             rules.push_back(&rule);
         }
         if (qi) {
@@ -715,81 +720,6 @@ namespace pdr {
         }   
     }
 
-    void pred_transformer::model2properties(
-        const model_core & mdl, 
-        unsigned index, 
-        model_node const& n, 
-        expr_ref_vector & res) const {
-        expr_ref tr1(transition(), m), tr2(m);
-        expr_ref_vector trs(m), refs(m);
-        expr_substitution sub(m);        
-        unsigned sz = mdl.get_num_constants();
-        obj_map<expr,ptr_vector<app> > equivs;
-
-        for (unsigned i = 0; i < sz; i++) {
-             func_decl * d = mdl.get_constant(i);    
-             expr_ref interp(m);
-             ptr_vector<app> cs;
-             obj_map<expr,ptr_vector<app> >::obj_map_entry* e;
-             get_value_from_model(mdl, d, interp);  
-             app* c = m.mk_const(d);
-             refs.push_back(c);
-             refs.push_back(interp);
-             if (m.is_bool(d->get_range())) {
-                 sub.insert(c, interp);
-             }
-             else {
-                 e = equivs.insert_if_not_there2(interp, cs);
-                 e->get_data().m_value.push_back(c);
-             }
-        }
-        obj_map<expr,ptr_vector<app> >::iterator it = equivs.begin(), end = equivs.end();
-        for (; it != end; ++it) {
-            // 
-            // determine equivalence class representative.
-            // it is either one of the indexed variables, or it
-            // is the constant evaluated by the model.
-            // 
-            ptr_vector<app> const& cs = it->m_value;
-            expr* rep = 0;
-            for (unsigned i = 0; !rep && i < cs.size(); ++i) {
-                if (pm.is_o(cs[i]->get_decl(), index)) {
-                    rep = cs[i];
-                }
-            }
-            if (!rep) {
-                rep = it->m_key;
-            }
-            for (unsigned i = 0; i < cs.size(); ++i) {
-                if (!pm.is_o(cs[i]->get_decl(), index)) {
-                    sub.insert(cs[i], rep);
-                }
-            }            
-        }
-        scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
-        rep->set_substitution(&sub);
-        (*rep)(tr1);
-        th_rewriter rw(m);
-        rw(tr1);
-        TRACE("pdr", tout << "Transition:\n" << mk_pp(tr1, m) << "\n";);
-        pm.formula_o2n(tr1, tr2, index);
-        datalog::flatten_and(tr2, trs);
-        res.append(trs);
-        TRACE("pdr", tout << "Reduced transition:\n" << mk_pp(tr2, m) << "\n";);
-
-        // 
-        // Take state-invariant for indexed formula and select the literals
-        // that are true under the assignment.
-        // 
-        //
-#if 0
-        IF_VERBOSE(2, verbose_stream() << "index: " << index << "\n"
-                   << "level: " << n.level() << "\n"
-                   << mk_pp(n.pt().get_propagation_formula(m_rels, n.level()), m) << "\n"          
-                   << "propagation formula\n"
-                   << mk_pp(n.parent()->pt().get_propagation_formula(m_rels, n.level()+1), m) << "\n";);
-#endif
-    }
 
     // ----------------
     // model_node
@@ -844,8 +774,7 @@ namespace pdr {
                 model.insert(e, m.mk_true());
             }
         }
-        r0 = const_cast<datalog::rule*>(pt().find_rule(*m_model.get()));
-        SASSERT(r0);
+        r0 = const_cast<datalog::rule*>(&pt().find_rule(*m_model.get()));
         app_ref_vector& inst = pt().get_inst(r0);
         TRACE("pdr", tout << mk_pp(state(), m) << "\n";);
         for (unsigned i = 0; i < inst.size(); ++i) {
@@ -886,12 +815,6 @@ namespace pdr {
         return 0;
     }
 
-    void model_node::get_properties(expr_ref_vector& props) const {
-        model_node* p = parent();
-        if (p) {
-            p->pt().model2properties(p->model(), index(), *this, props);
-        }
-    }
 
     // ----------------
     // model_search
@@ -1256,7 +1179,6 @@ namespace pdr {
         for (; it != end; ++it) {
             m_rels.insert(it->m_key, it->m_value);
         }
-        VERIFY(m_rels.find(m_query_pred, m_query));
     }
 
     unsigned context::get_num_levels(func_decl* p) {
@@ -1397,8 +1319,9 @@ namespace pdr {
     void context::init_core_generalizers(datalog::rule_set& rules) {
         reset_core_generalizers();
         classifier_proc classify(m, rules);
-        if (m_params.get_bool(":use-multicore-generalizer", false)) {
-            m_core_generalizers.push_back(alloc(core_multi_generalizer, *this));
+        bool use_mc = m_params.get_bool(":use-multicore-generalizer", false);
+        if (use_mc) {
+            m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
         }
         if (m_params.get_bool(":use-farkas", true) && !classify.is_bool()) {
             if (m_params.get_bool(":inline-proof-mode", true)) {
@@ -1414,10 +1337,7 @@ namespace pdr {
                 m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
             }
         }
-        if (m_params.get_bool(":use-farkas-properties", false)) {
-            m_core_generalizers.push_back(alloc(core_farkas_properties_generalizer, *this));
-        }
-        if (m_params.get_bool(":use-inductive-generalizer", true)) {
+        if (!use_mc && m_params.get_bool(":use-inductive-generalizer", true)) {
             m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
         }
         if (m_params.get_bool(":use-interpolants", false)) {
@@ -1540,6 +1460,9 @@ namespace pdr {
     }
 
     void context::solve_impl() {
+        if (!m_rels.find(m_query_pred, m_query)) {
+            throw inductive_exception();            
+        }
         unsigned lvl = 0;
         bool reachable;
         while (true) {
@@ -1643,15 +1566,28 @@ namespace pdr {
                 }
                 break;
             case l_false: {
-                bool uses_level = true;
-                for (unsigned i = 0; !cube.empty() && i < m_core_generalizers.size(); ++i) {
-                    (*m_core_generalizers[i])(n, cube, uses_level);
+                core_generalizer::cores cores;
+                cores.push_back(std::make_pair(cube, true));
+                
+                for (unsigned i = 0; !cores.empty() && i < m_core_generalizers.size(); ++i) {
+                    core_generalizer::cores new_cores;                    
+                    for (unsigned j = 0; j < cores.size(); ++j) {
+                        (*m_core_generalizers[i])(n, cores[j].first, cores[j].second, new_cores);
+                    }
+                    cores.reset();
+                    cores.append(new_cores);
+                }
+                bool found_invariant = false;
+                for (unsigned i = 0; i < cores.size(); ++i) {
+                    expr_ref_vector const& core = cores[i].first;
+                    bool uses_level = cores[i].second;
+                    found_invariant = !uses_level || found_invariant;
+                    expr_ref ncore(m_pm.mk_not_and(core), m);
+                    TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") <<  mk_pp(ncore, m) << "\n";);
+                    n.pt().add_property(ncore, uses_level?n.level():infty_level);
                 }
-                expr_ref ncube(m_pm.mk_not_and(cube), m);
-                TRACE("pdr", tout << "invariant state: " << (uses_level?"":"(inductive) ") <<  mk_pp(ncube, m) << "\n";);
-                n.pt().add_property(ncube, uses_level?n.level():infty_level);
                 CASSERT("pdr",n.level() == 0 || check_invariant(n.level()-1));
-                m_search.backtrack_level(uses_level && m_params.get_bool(":flexible-trace", false), n);
+                m_search.backtrack_level(!found_invariant && m_params.get_bool(":flexible-trace", false), n);
                 break;
             }
             case l_undef: {
@@ -1707,10 +1643,13 @@ namespace pdr {
         SASSERT(level > 0);
         n.pt().find_predecessors(n.model(), preds);
         n.pt().remove_predecessors(literals);
-        TRACE("pdr", tout << mk_pp(model, m) << "\n";
+        TRACE("pdr", 
               model_v2_pp(tout, n.model());
+              tout << "Model cube\n";
+              tout << mk_pp(model, m) << "\n";
+              tout << "Predecessors\n";
               for (unsigned i = 0; i < preds.size(); ++i) {
-                  tout << mk_pp(preds[i], m) << "\n";
+                  tout << preds[i]->get_name() << "\n";
               }
              );
         for (unsigned i = 0; i < preds.size(); ++i) {            
@@ -1729,6 +1668,58 @@ namespace pdr {
         TRACE("pdr", m_search.display(tout););
     }
 
+    /**
+       \brief create children states from model cube.
+
+       Introduce the shorthands:
+
+       - T(x0,x1,x)   for transition
+       - phi(x)       for n.state()
+       - psi(x0,x1,x) for psi
+       - M(x0,x1,x)   for n.model()
+
+       Assumptions:
+         M => psi
+         psi => phi & T
+         psi & M  agree on which rules are taken.
+
+       In other words, 
+       1. psi is a weakening of M
+       2. phi & T is implied by psi
+       
+       Goal is to find phi0(x0), phi1(x1) such that:
+
+       phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x)
+
+       Strategy: 
+
+       - perform cheap existential quantifier elimination on 
+         exists x . T(x0,x1,x) & phi(x)
+         (e.g., destructive equality resolution) 
+
+       - pull equalities that use 
+       
+       
+    */
+    void context::create_children2(model_node& n, expr* psi) {        
+        SASSERT(n.level() > 0);
+
+        model_core const& M = n.model();
+        datalog::rule const& r = n.pt().find_rule(M);
+        expr* T   = n.pt().get_transition(r);
+        expr* phi = n.state();
+
+        expr_ref_vector Ts(m);
+        datalog::flatten_and(T, Ts);
+
+        ptr_vector<func_decl> preds;
+        n.pt().find_predecessors(r, preds);        
+        n.pt().remove_predecessors(Ts);
+
+        // TBD ...
+        TRACE("pdr", m_search.display(tout););
+    }
+
     void context::collect_statistics(statistics& st) const {
         decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
         for (it = m_rels.begin(); it != end; ++it) {
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index f849fdbcd..b2cd17f84 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -59,6 +59,8 @@ namespace pdr {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
 
+        typedef obj_map<datalog::rule const, expr*> rule2expr;
+
         manager&                     pm;        // pdr-manager
         ast_manager&                 m;         // manager
         
@@ -71,9 +73,10 @@ namespace pdr {
         expr_ref_vector              m_invariants;  // properties that are invariant.
         obj_map<expr, unsigned>      m_prop2level;  // map property to level where it occurs.
         obj_map<expr, datalog::rule const*> m_tag2rule; // map tag predicate to rule. 
-        obj_map<datalog::rule const, expr*> m_rule2tag; // map rule to predicate tag.
+        rule2expr                    m_rule2tag; // map rule to predicate tag.
         qinst_map                    m_rule2qinst;      // map tag to quantifier instantiation.
         rule2inst                    m_rule2inst;       // map rules to instantiations of indices
+        rule2expr                    m_rule2transition; // map rules to transition 
         expr_ref                     m_transition;      // transition relation.
         expr_ref                     m_initial_state;   // initial state.
         reachable_cache              m_reachable; 
@@ -132,7 +135,8 @@ namespace pdr {
         void remove_predecessors(expr_ref_vector& literals);
         void find_predecessors(datalog::rule const& r, ptr_vector<func_decl>& predicates) const;
         void find_predecessors(model_core const& model, ptr_vector<func_decl>& preds) const;
-        datalog::rule const* find_rule(model_core const& model) const;
+        datalog::rule const& find_rule(model_core const& model) const;
+        expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); }
 
         bool propagate_to_next_level(unsigned level);
         void add_property(expr * lemma, unsigned lvl);  // add property 'p' to state at level.
@@ -151,7 +155,6 @@ namespace pdr {
         ast_manager& get_manager() const { return m; }
 
         void model2cube(const model_core & mdl, expr_ref_vector & res) const;
-        void model2properties(const model_core & mdl, unsigned index, model_node const& n, expr_ref_vector & res) const;
 
         void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
 
@@ -193,7 +196,6 @@ namespace pdr {
         model_node* parent() const { return m_parent; }
         model_core const& model() const { return *m_model; }
         unsigned index() const;
-        void get_properties(expr_ref_vector& props) const;
 
         bool is_closed() const { return m_closed; }
         bool is_open() const { return !is_closed(); }
@@ -278,9 +280,16 @@ namespace pdr {
     protected:
         context& m_ctx;
     public:
+        typedef vector<std::pair<expr_ref_vector,bool> > cores;
         core_generalizer(context& ctx): m_ctx(ctx) {}
         virtual ~core_generalizer() {}
         virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level) = 0;
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
+            new_cores.push_back(std::make_pair(core, uses_level));
+            if (!core.empty()) {
+                (*this)(n, new_cores.back().first, new_cores.back().second);
+            }
+        }
         virtual void collect_statistics(statistics& st) {}
     };
 
@@ -324,6 +333,7 @@ namespace pdr {
         void expand_node(model_node& n);
         lbool expand_state(model_node& n, expr_ref_vector& cube);
         void create_children(model_node& n, expr* cube);
+        void create_children2(model_node& n, expr* cube);
         expr_ref mk_sat_answer() const;
         expr_ref mk_unsat_answer() const;
         
diff --git a/lib/pdr_dl_interface.cpp b/lib/pdr_dl_interface.cpp
index 52481bd13..d7952fec3 100644
--- a/lib/pdr_dl_interface.cpp
+++ b/lib/pdr_dl_interface.cpp
@@ -122,8 +122,8 @@ lbool dl_interface::query(expr * query) {
     if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) {
         unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0);
         datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
-        transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
-        m_ctx.transform_rules(transformer1, mc, pc);
+        //transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+        //m_ctx.transform_rules(transformer1, mc, pc);
         transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
         while (num_unfolds > 0) {
             m_ctx.transform_rules(transformer2, mc, pc);        
@@ -205,7 +205,6 @@ void dl_interface::collect_params(param_descrs& p) {
     PRIVATE_PARAMS(p.insert(":use-farkas-model", CPK_BOOL, "PDR: (default false) enable using Farkas generalization through model propagation"););
     PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions"););
     PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
-    PRIVATE_PARAMS(p.insert(":use-farkas-properties", CPK_BOOL, "PDR: (default false) experimental Farkas lemma generation method"););
     PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
     PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););
     PRIVATE_PARAMS(p.insert(":dump-interpolants", CPK_BOOL, "PDR: (default false) display interpolants"););
diff --git a/lib/pdr_generalizers.cpp b/lib/pdr_generalizers.cpp
index c15e8193f..d3db59d39 100644
--- a/lib/pdr_generalizers.cpp
+++ b/lib/pdr_generalizers.cpp
@@ -124,52 +124,42 @@ namespace pdr {
     //
     // extract multiple cores from unreachable state.
     //
+
+
     void core_multi_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
+        UNREACHABLE();
+    }
+
+    /**
+       \brief Find minimal cores.
+       Apply a simple heuristic: find a minimal core, then find minimal cores that exclude at least one
+       literal from each of the literals in the minimal cores.
+    */
+    void core_multi_generalizer::operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores) {
         ast_manager& m = core.get_manager();
-        manager& pm = n.pt().get_pdr_manager();
-        expr_ref_vector states(m), cores(m);
-        datalog::flatten_and(n.state(), states);
-        obj_hashtable<expr> core_exprs;
-        for (unsigned i = 0; i < core.size(); ++i) {
-            core_exprs.insert(core[i].get());
-        }
-        TRACE("pdr", 
-            tout << "Old core:\n"; for (unsigned i = 0; i < core.size(); ++i) tout << mk_pp(core[i].get(), m) << "\n";
-            tout << "State:\n"; for (unsigned i = 0; i < states.size(); ++i) tout << mk_pp(states[i].get(), m) << "\n";
-        );
-        cores.push_back(pm.mk_and(core));
-        bool change = false;
-        for (unsigned i = 0; i < states.size(); ++i) {
-            expr_ref tmp(states[i].get(), m), new_state(m);
-            expr_ref_vector new_core(m);
-            if (core_exprs.contains(tmp.get())) {
-                states[i] = m.mk_true();
-                new_state = m.mk_not(pm.mk_and(states));
-                bool assumes_level;
-                if (n.pt().is_invariant(n.level(), new_state, false, assumes_level, &new_core)) {
-#if 0
-                    for (unsigned j = 0; j < new_core.size(); ++j) {
-                        core_exprs.insert(new_core[j].get());
-                    }
-#endif
-                    if (assumes_level) {
-                        uses_level = true;
-                    }
-                    tmp = pm.mk_and(new_core);
-                    TRACE("pdr", tout << "New core:\n" << mk_pp(tmp, m) << "\n";);
-                    cores.push_back(tmp);
-                    change = true;
-                }
-                else {
-                    states[i] = tmp;
+        expr_ref_vector old_core(m), core0(core);
+        bool uses_level1 = uses_level;
+        m_gen(n, core0, uses_level1);
+        new_cores.push_back(std::make_pair(core0, uses_level1));
+        obj_hashtable<expr> core_exprs, core1_exprs;
+        datalog::set_union(core_exprs, core0);
+        for (unsigned i = 0; i < old_core.size(); ++i) {
+            expr* lit = old_core[i].get();             
+            if (core_exprs.contains(lit)) {
+                expr_ref_vector core1(old_core);
+                core1[i] = core1.back();
+                core1.pop_back();
+                uses_level1 = uses_level;
+                m_gen(n, core1, uses_level1);
+                SASSERT(core1.size() <= old_core.size());
+                if (core1.size() < old_core.size()) {
+                    new_cores.push_back(std::make_pair(core1, uses_level1));
+                    core1_exprs.reset();
+                    datalog::set_union(core1_exprs, core1);
+                    datalog::set_intersection(core_exprs, core1_exprs);
                 }
             }
         }
-        if (change) {
-            core.reset();
-            core.push_back(pm.mk_or(cores));
-            TRACE("pdr", tout << "New Cores:\n" << mk_pp(core[0].get(), m) << "\n";);
-        }
     }
 
     // 
@@ -651,35 +641,4 @@ namespace pdr {
         TRACE("pdr", for (unsigned i = 0; i < cube.size(); ++i) tout << mk_pp(cube[i].get(), m) << "\n";);
     }
 
-    //
-    // use properties from predicate transformer to strengthen state.
-    //
-    void core_farkas_properties_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
-        if (core.empty()) return;
-
-        front_end_params& p = m_ctx.get_fparams();
-        ast_manager& m = n.pt().get_manager();
-        manager& pm = n.pt().get_pdr_manager();
-        expr_ref_vector lemmas(m), properties(m);
-        expr_ref A(m), B(m);
-        farkas_learner learner(p, m);
-        n.get_properties(properties);
-        A = n.pt().get_propagation_formula(m_ctx.get_pred_transformers(), n.level());
-        B = m.mk_and(properties.size(), properties.c_ptr());
-        if (learner.get_lemma_guesses(A, B, lemmas)) {
-            TRACE("pdr", 
-                  tout << "Properties:\n";
-                  for (unsigned i = 0; i < properties.size(); ++i) {
-                      tout << mk_pp(properties[i].get(), m) << "\n";
-                  }
-                  tout << mk_pp(B, m) << "\n";
-                  tout << "New core:\n";
-                  for (unsigned i = 0; i < lemmas.size(); ++i) {
-                      tout << mk_pp(lemmas[i].get(), m) << "\n";
-                  });
-            core.append(lemmas); // disjunction?
-            uses_level = true;
-        }
-    }
-
 };
diff --git a/lib/pdr_generalizers.h b/lib/pdr_generalizers.h
index 5f1c01941..22d9784c7 100644
--- a/lib/pdr_generalizers.h
+++ b/lib/pdr_generalizers.h
@@ -64,13 +64,6 @@ namespace pdr {
         virtual void operator()(model_node& n, expr_ref_vector& cube);
     };
 
-    class core_farkas_properties_generalizer : public core_generalizer {
-    public:
-        core_farkas_properties_generalizer(context& ctx): core_generalizer(ctx) {}
-        virtual ~core_farkas_properties_generalizer() {}
-        virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);        
-    };
-
     class model_evaluation_generalizer : public model_generalizer {        
         th_rewriter_model_evaluator m_model_evaluator;
     public:        
@@ -80,10 +73,12 @@ namespace pdr {
     };
 
     class core_multi_generalizer : public core_generalizer {
+        core_bool_inductive_generalizer m_gen;
     public:
-        core_multi_generalizer(context& ctx): core_generalizer(ctx) {}
+        core_multi_generalizer(context& ctx, unsigned max_failures): core_generalizer(ctx), m_gen(ctx, max_failures) {}
         virtual ~core_multi_generalizer() {}
         virtual void operator()(model_node& n, expr_ref_vector& core, bool& uses_level);
+        virtual void operator()(model_node& n, expr_ref_vector const& core, bool uses_level, cores& new_cores);
     };
 
     class core_interpolant_generalizer : public core_generalizer {
diff --git a/lib/pdr_quantifiers.cpp b/lib/pdr_quantifiers.cpp
index 6ba7c2d5e..a4e6a0ac1 100644
--- a/lib/pdr_quantifiers.cpp
+++ b/lib/pdr_quantifiers.cpp
@@ -421,7 +421,7 @@ namespace pdr {
         if (!(&node.model())) {
             return;
         }
-        m_current_rule = pt.find_rule(node.model());   
+        m_current_rule = &pt.find_rule(node.model());   
         m_current_pt = &pt;
         m_current_node = &node;
         if (!m_current_rule) { 
diff --git a/lib/ref_vector.h b/lib/ref_vector.h
index f2ceb769b..3a4f7dd7f 100644
--- a/lib/ref_vector.h
+++ b/lib/ref_vector.h
@@ -113,8 +113,13 @@ public:
 
     T * const * c_ptr() const { return m_nodes.begin(); }
 
+    typedef T* const* iterator;
+
     T ** c_ptr() { return m_nodes.begin(); }
 
+    iterator begin() const { return m_nodes.begin(); }
+    iterator end() const { return begin() + size(); }
+
     void set(unsigned idx, T * n) {
         inc_ref(n);
         dec_ref(m_nodes[idx]);