diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
index be730a5c7..74ab001b4 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp
@@ -371,18 +371,21 @@ namespace datalog {
     bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
         unsigned u_len = r->get_uninterpreted_tail_size();
         unsigned len = r->get_tail_size();
-        if (u_len==len) {
+        if (u_len == len) {
             return false;
         }
 
         ptr_vector<expr> todo;
-        for (unsigned i=u_len; i<len; i++) {
+        for (unsigned i = u_len; i < len; i++) {
             todo.push_back(r->get_tail(i));
             SASSERT(!r->is_neg_tail(i));
         }
 
         m_rule_subst.reset(r);
 
+        obj_hashtable<expr> leqs;
+        expr_ref_vector trail(m);
+        expr_ref tmp1(m), tmp2(m);
         bool found_something = false;
 
 #define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; }
@@ -424,6 +427,17 @@ namespace datalog {
                     TRY_UNIFY(arg1, m.mk_true());
                 }
             }
+            else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) {
+                tmp1 = a.mk_sub(arg1, arg2);
+                tmp2 = a.mk_sub(arg2, arg1);
+                if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
+                    TRY_UNIFY(arg1, arg2);
+                }
+                else {
+                    trail.push_back(tmp1);
+                    leqs.insert(tmp1);
+                }
+            }
         }
 
         if (!found_something) {
diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h
index 99bda325f..5e4fd8fbc 100644
--- a/src/muz_qe/dl_mk_interp_tail_simplifier.h
+++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h
@@ -24,6 +24,7 @@ Revision History:
 #include "dl_rule_transformer.h"
 #include "unifier.h"
 #include "substitution.h"
+#include "arith_decl_plugin.h"
 
 namespace datalog {
 
@@ -60,11 +61,10 @@ namespace datalog {
             }
         };
 
-
-        ast_manager & m;
-        context & m_context;
-        th_rewriter & m_simp;
-
+        ast_manager &     m;
+        context &         m_context;
+        th_rewriter &     m_simp;
+        arith_util        a;
         rule_substitution m_rule_subst;
 
         class normalizer_cfg;
@@ -82,6 +82,7 @@ namespace datalog {
             m(ctx.get_manager()),
             m_context(ctx),
             m_simp(ctx.get_rewriter()),
+            a(m),
             m_rule_subst(ctx) {}
 
         /**If rule should be retained, assign transformed version to res and return true;
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 0b9115e57..1f1d12340 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -732,7 +732,7 @@ namespace datalog {
 
 
     void mk_slice::update_rule(rule& r, rule_set& dst) {
-        rule* new_rule;
+        rule_ref new_rule(rm);
         if (rule_updated(r)) {
             init_vars(r);
             app_ref_vector tail(m);
@@ -794,16 +794,20 @@ namespace datalog {
                 
             }
             
+            
             new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);        
+
+            rm.fix_unbound_vars(new_rule, false);
+
             TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
         }
         else {
             new_rule = &r;
         }
-        dst.add_rule(new_rule);
+        dst.add_rule(new_rule.get());
 
         if (m_pc) {
-            m_pc->insert(&r, new_rule, 0, 0);
+            m_pc->insert(&r, new_rule.get(), 0, 0);
         }
     }
 
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 34868c7e5..b5e6b9305 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -41,6 +41,7 @@ Revision History:
 #include"quant_hoist.h"
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
+#include"qe_lite.h"
 
 namespace datalog {
 
@@ -613,14 +614,65 @@ namespace datalog {
         return r;
     }
 
+    void rule_manager::reduce_unbound_vars(rule_ref& r) {
+        unsigned ut_len = r->get_uninterpreted_tail_size();
+        unsigned t_len = r->get_tail_size();
+        ptr_vector<sort> vars;
+        uint_set index_set;
+        qe_lite qe(m);
+        expr_ref_vector conjs(m);
+
+        if (ut_len == t_len) {
+            return;
+        }
+
+        get_free_vars(r->get_head(), vars);
+        for (unsigned i = 0; i < ut_len; ++i) {
+            get_free_vars(r->get_tail(i), vars);
+        }
+        for (unsigned i = ut_len; i < t_len; ++i) {
+            conjs.push_back(r->get_tail(i));
+        }
+
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            if (vars[i]) {
+                index_set.insert(i);
+            }
+        }
+        qe(index_set, false, conjs);
+        bool change = conjs.size() != t_len - ut_len;
+        for (unsigned i = 0; !change && i < conjs.size(); ++i) {
+            change = r->get_tail(ut_len+i) != conjs[i].get();
+        }
+        if (change) {
+            app_ref_vector tail(m);
+            svector<bool> tail_neg;
+            for (unsigned i = 0; i < ut_len; ++i) {
+                tail.push_back(r->get_tail(i));
+                tail_neg.push_back(r->is_neg_tail(i));
+            }
+            for (unsigned i = 0; i < conjs.size(); ++i) {
+                tail.push_back(ensure_app(conjs[i].get()));
+            }
+            tail_neg.resize(tail.size(), false);
+            r = mk(r->get_head(), tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+            TRACE("dl", r->display(m_ctx, tout << "reduced rule\n"););
+        }
+    }
+
     void rule_manager::fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination) {
 
+        reduce_unbound_vars(r);
+
         if (!m_ctx.fix_unbound_vars()) {
             return;
         }
 
-        if (r->get_uninterpreted_tail_size() == r->get_tail_size()) {
-            //no interpreted tail to fix
+        unsigned ut_len = r->get_uninterpreted_tail_size();
+        unsigned t_len = r->get_tail_size();
+
+        if (ut_len == t_len) {
+            // no interpreted tail to fix
             return;
         }
 
@@ -633,7 +685,7 @@ namespace datalog {
         get_free_vars(r, free_rule_vars);
         vctr.count_vars(m, head);
 
-        unsigned ut_len = r->get_uninterpreted_tail_size();
+
         for (unsigned i = 0; i < ut_len; i++) {
             app * t = r->get_tail(i);
             vctr.count_vars(m, t);
@@ -642,11 +694,9 @@ namespace datalog {
         }
 
         ptr_vector<sort> interp_vars;
-        //var_idx_set interp_vars;
         var_idx_set unbound_vars;
         expr_ref_vector tails_with_unbound(m);
 
-        unsigned t_len = r->get_tail_size();
         for (unsigned i = ut_len; i < t_len; i++) {
             app * t = r->get_tail(i);
             interp_vars.reset();
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 0117f1e07..0882a52f3 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -83,6 +83,11 @@ namespace datalog {
 
         unsigned hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
 
+        /**
+           \brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
+         */
+        void reduce_unbound_vars(rule_ref& r);
+
     public:
 
         ast_manager& get_manager() const { return m; }
@@ -127,6 +132,7 @@ namespace datalog {
         void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
 
 
+
         /**
            \brief apply substitution to variables of rule.
         */
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 1280810e3..0f426b6fd 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -472,10 +472,7 @@ namespace pdr {
         th_rewriter rw(m);
         rw(m_transition);
         rw(m_initial_state);
-        if (ctx.is_dl()) {
-            hoist_non_bool_if(m_transition);
-            hoist_non_bool_if(m_initial_state);
-        }
+        
         m_solver.add_formula(m_transition);
         m_solver.add_level_formula(m_initial_state, 0);
         TRACE("pdr", 
@@ -578,6 +575,9 @@ namespace pdr {
         expr_ref fml = pm.mk_and(conj);
         th_rewriter rw(m);
         rw(fml);
+        if (ctx.is_dl()) {
+            hoist_non_bool_if(fml);
+        }
         TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
         SASSERT(is_ground(fml));
         if (m.is_false(fml)) {
@@ -1825,6 +1825,7 @@ namespace pdr {
             ++m_stats.m_num_nodes;
             m_search.add_leaf(*child); 
             IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+            m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
         }
         check_pre_closed(n);
         TRACE("pdr", m_search.display(tout););
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 1a6a3f9c6..19b1a6570 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -175,21 +175,25 @@ namespace pdr {
         expr_ref               m_state;
         model_ref              m_model;
         ptr_vector<model_node> m_children;
-        unsigned               m_level;
+        unsigned               m_level;       
         unsigned               m_orig_level;
+        unsigned               m_depth;
         bool                   m_closed;
     public:
         model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
-            m_parent(parent), m_pt(pt), m_state(state), m_model(0), m_level(level), m_orig_level(level), m_closed(false) {
+            m_parent(parent), m_pt(pt), m_state(state), m_model(0), 
+                m_level(level), m_orig_level(level), m_depth(0), m_closed(false) {
             if (m_parent) {
                 m_parent->m_children.push_back(this);
                 SASSERT(m_parent->m_level == level+1);
                 SASSERT(m_parent->m_level > 0);
+                m_depth = m_parent->m_depth+1;
             }
         }
         void set_model(model_ref& m) { m_model = m; }
         unsigned level() const { return m_level; }
         unsigned orig_level() const { return m_orig_level; }
+        unsigned depth() const { return m_depth; }
         void     increase_level() { ++m_level; }
         expr*    state() const { return m_state; }
         ptr_vector<model_node> const& children() { return m_children; }
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 045411fb1..1e7ba27c7 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -201,8 +201,10 @@ void dl_interface::collect_params(param_descrs& p) {
     p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
     p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
     p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
-    p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); 
-    p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
+    p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "
+             "Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); 
+    p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples "
+             "by extending candidate trace within search area");
     p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
     p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
     p.insert(":validate-result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
@@ -219,5 +221,5 @@ void dl_interface::collect_params(param_descrs& p) {
     PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"););
     PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"););
     p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
-    p.insert(":coalesce-rules", CPK_BOOL, "PDR: (default false) coalesce rules");
+    p.insert(":coalesce-rules", CPK_BOOL, "BMC: (default false) coalesce rules");
 }
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index a543593b3..33298c515 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -468,7 +468,10 @@ void model_evaluator::eval_arith(app* e) {
 void model_evaluator::inherit_value(expr* e, expr* v) {
     SASSERT(!is_unknown(v));
     SASSERT(m.get_sort(e) == m.get_sort(v));
-    if (m.is_bool(e)) {
+    if (is_x(v)) {
+        set_x(e);
+    }
+    else if (m.is_bool(e)) {
         SASSERT(m.is_bool(v));
         if (is_true(v)) set_true(e);
         else if (is_false(v)) set_false(e);
@@ -862,12 +865,19 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         fml = m.mk_and(conjs.size(), conjs.c_ptr());        
     }
 
+    // 
+    // (f (if c1 (if c2 e1 e2) e3) b c) -> 
+    // (if c1 (if c2 (f e1 b c)
+
     class ite_hoister {
         ast_manager& m;
     public:
         ite_hoister(ast_manager& m): m(m) {}
 
         br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
+            if (m.is_ite(f)) {
+                return BR_FAILED;
+            }
             for (unsigned i = 0; i < num_args; ++i) {
                 expr* c, *t, *e;
                 if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
@@ -875,8 +885,13 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
                     ptr_vector<expr> args1(num_args, args);
                     args1[i] = t;
                     e1 = m.mk_app(f, num_args, args1.c_ptr());
+                    if (t == e) {
+                        result = e1;
+                        return BR_REWRITE1;
+                    }
                     args1[i] = e;
                     e2 = m.mk_app(f, num_args, args1.c_ptr());
+                    result = m.mk_app(f, num_args, args);
                     result = m.mk_ite(c, e1, e2);
                     return BR_REWRITE3;
                 }
@@ -910,7 +925,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         ite_hoister_star ite_rw(m, p);
         expr_ref tmp(m);
         ite_rw(fml, tmp);
-        fml = tmp;
+        fml = tmp;        
     }
 
     class test_diff_logic {
@@ -934,13 +949,23 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
         }
 
-        bool is_var_or_numeric(expr* e) const {
+        bool is_offset(expr* e) const {
             if (a.is_numeral(e)) {
                 return true;
             }
-            expr* cond, *th, *el;
+            expr* cond, *th, *el, *e1, *e2;
             if (m.is_ite(e, cond, th, el)) {
-                return is_var_or_numeric(th) && is_var_or_numeric(el);
+                return is_offset(th) && is_offset(el);
+            }
+            // recognize offsets.
+            if (a.is_add(e, e1, e2)) {
+                if (is_numeric(e1)) {
+                    return is_offset(e2);
+                }
+                if (is_numeric(e2)) {
+                    return is_offset(e1);
+                }
+                return false;
             }
             return !is_arith_expr(e);
         }
@@ -954,14 +979,14 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             SASSERT(to_app(e)->get_num_args() == 2);
             expr * lhs = to_app(e)->get_arg(0);
             expr * rhs = to_app(e)->get_arg(1);
-            if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs)) 
+            if (is_offset(lhs) && is_offset(rhs)) 
                 return true;    
             if (!is_numeric(rhs)) 
                 std::swap(lhs, rhs);
             if (!is_numeric(rhs)) 
                 return false;    
             // lhs can be 'x' or '(+ x (* -1 y))'
-            if (is_var_or_numeric(lhs))
+            if (is_offset(lhs))
                 return true;
             expr* arg1, *arg2;
             if (!a.is_add(lhs, arg1, arg2)) 
@@ -975,7 +1000,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             expr* m1, *m2;
             if (!a.is_mul(arg2, m1, m2))
                 return false;
-            return is_minus_one(m1) && is_var_or_numeric(m2);
+            return is_minus_one(m1) && is_offset(m2);
         }
 
         bool test_eq(expr* e) const {
@@ -997,7 +1022,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             if (a.is_numeral(e)) {
                 return true;
             }
-            if (is_var_or_numeric(e)) {
+            if (is_offset(e)) {
                 return true;
             }
             expr* lhs, *rhs;
@@ -1005,7 +1030,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
                 if (!a.is_numeral(lhs)) {
                     std::swap(lhs, rhs);
                 }
-                return a.is_numeral(lhs) && is_var_or_numeric(rhs);
+                return a.is_numeral(lhs) && is_offset(rhs);
             }
             if (a.is_mul(e, lhs, rhs)) {
                 return is_minus_one(lhs) || is_minus_one(rhs);
diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp
index 77750ced6..a01500fe3 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/muz_qe/qe.cpp
@@ -1712,7 +1712,8 @@ namespace qe {
                         m_solver.get_model(model);
                         SASSERT(is_sat == l_true);
                         model_evaluator model_eval2(*model);
-                        model_eval2(x,val);
+                        model_eval2.set_model_completion(true);
+                        model_eval2(x, val);
                     }
                     TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";);
                     m_current->add_def(x, val);
diff --git a/src/muz_qe/qe_datatype_plugin.cpp b/src/muz_qe/qe_datatype_plugin.cpp
index c280df964..3978a9ba4 100644
--- a/src/muz_qe/qe_datatype_plugin.cpp
+++ b/src/muz_qe/qe_datatype_plugin.cpp
@@ -133,7 +133,7 @@ namespace qe {
             func_decl* f = a->get_decl();
             if (m_util.is_recognizer(f) && a->get_arg(0) == x) {
                 m_recognizers.push_back(a);
-                TRACE("quant_elim", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
+                TRACE("qe", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
                 return true;
             }
             if (!m.is_eq(a)) {
@@ -161,6 +161,10 @@ namespace qe {
         unsigned num_neqs() { return m_neq_atoms.size(); }
         app*  neq_atom(unsigned i) { return m_neq_atoms[i].get(); }
 
+        unsigned num_neq_terms() const { return m_neqs.size(); }
+        expr* neq_term(unsigned i) const { return m_neqs[i]; }
+        expr* const* neq_terms() const { return m_neqs.c_ptr(); }
+
         unsigned num_recognizers() { return m_recognizers.size(); }
         app*   recognizer(unsigned i) { return m_recognizers[i].get(); }
 
@@ -212,7 +216,7 @@ namespace qe {
         }
 
         void add_atom(app* a, bool is_pos) {
-            TRACE("quant_elim", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
+            TRACE("qe", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
             if (is_pos) {
                 m_eq_atoms.push_back(a);
             }
@@ -326,7 +330,7 @@ namespace qe {
             for_each_expr(*this, fml.get());
             if (m_change) {
                 fml = get_expr(fml.get());  
-                TRACE("quant_elim", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
+                TRACE("qe", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
             }
             return m_change;
         }
@@ -380,7 +384,7 @@ namespace qe {
             }
             expr* e = m.mk_and(conj.size(), conj.c_ptr());
             m_map.insert(a, e, 0);            
-            TRACE("quant_elim", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
+            TRACE("qe", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
             return true;
         }
 
@@ -456,7 +460,7 @@ namespace qe {
         virtual void assign(contains_app& x, expr* fml, rational const& vl) {
             sort* s = x.x()->get_decl()->get_range();
             SASSERT(m_datatype_util.is_datatype(s));
-            TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
+            TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
             if (m_datatype_util.is_recursive(s)) {
                 assign_rec(x, fml, vl);
             }
@@ -468,16 +472,13 @@ namespace qe {
         virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
             sort* s = x.x()->get_decl()->get_range();
             SASSERT(m_datatype_util.is_datatype(s));
-            TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
+            TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
             if (m_datatype_util.is_recursive(s)) {
                 subst_rec(x, vl, fml, def);
             }
             else {
                 subst_nonrec(x, vl, fml, def);
             }
-            if (def) {
-                *def = 0; // TBD
-            }
         }
         
         virtual unsigned get_weight( contains_app& x, expr* fml) {
@@ -605,7 +606,7 @@ namespace qe {
                 num_branches = rational(eqs.num_eqs() + 1);
                 return true;
             }
-            TRACE("quant_elim", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
+            TRACE("qe", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
             return false;
         }
 
@@ -660,6 +661,7 @@ namespace qe {
             SASSERT(m_datatype_util.is_datatype(s));
             func_decl* c = 0, *r = 0;
 
+            TRACE("qe", tout << mk_pp(x, m) << " " << vl << " " << mk_pp(fml, m) << " " << (def != 0) << "\n";);
             //
             // Add recognizer to formula.
             // Introduce auxiliary variable to eliminate.
@@ -673,13 +675,13 @@ namespace qe {
                 m_ctx.add_var(fresh_x);
                 m_replace->apply_substitution(x, fresh_x, 0, fml);
                 add_def(fresh_x, def);
-                TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
+                TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
                 return;
             }
 
 
             if (has_selector(contains_x, fml, c)) {
-                TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
+                TRACE("qe", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
                 subst_constructor(contains_x, c, fml, def); 
                 return;
             }
@@ -721,14 +723,19 @@ namespace qe {
                 }
 
                 for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
-                    m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
+                    m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
                 }
                 if (def) {
-                    NOT_IMPLEMENTED_YET();
-                    // you need to create a diagonal term
+                    sort* s = m.get_sort(x);
+                    ptr_vector<sort> sorts;
+                    sorts.resize(eqs.num_neq_terms(), s);
+                    func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s);
+                    expr_ref t(m);
+                    t = m.mk_app(diag, eqs.num_neq_terms(), eqs.neq_terms());
+                    add_def(t, def);
                 }
             }
-            TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
+            TRACE("qe", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
         }
 
         bool get_num_branches_nonrec( contains_app& x, expr* fml, rational& num_branches) {
@@ -738,10 +745,10 @@ namespace qe {
             func_decl* c = 0, *r = 0;
 
             if (sz != 1 && has_recognizer(x.x(), fml, r, c)) {
-                TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
+                TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
                 num_branches = rational(1);
             }        
-            TRACE("quant_elim", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
+            TRACE("qe", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
             return true; 
         }
 
@@ -757,7 +764,7 @@ namespace qe {
             }
             func_decl* c = 0, *r = 0;
             if (has_recognizer(x, fml, r, c)) {
-                TRACE("quant_elim", tout << mk_pp(x, m) << " has a recognizer\n";);
+                TRACE("qe", tout << mk_pp(x, m) << " has a recognizer\n";);
                 return;
             }
             
@@ -776,7 +783,7 @@ namespace qe {
             SASSERT(!m_datatype_util.is_recursive(s));
             func_decl* c = 0, *r = 0;
             if (has_recognizer(x.x(), fml, r, c)) {
-                TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
+                TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
             }
             else {
                 unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index ce7b85a87..ec042e33d 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -15,25 +15,68 @@ Author:
 
 Revision History:
 
- - TBD: integrate Fourier Motzkin elimination
-        integrate Gaussean elimination
 
 --*/
 #include "qe_lite.h"
 #include "expr_abstract.h"
 #include "used_vars.h"
-#include"occurs.h"
-#include"for_each_expr.h"
-#include"rewriter_def.h"
-#include"ast_pp.h"
-#include"ast_ll_pp.h"
-#include"ast_smt2_pp.h"
-#include"tactical.h"
-#include"bool_rewriter.h"
-#include"var_subst.h"
+#include "occurs.h"
+#include "for_each_expr.h"
+#include "rewriter_def.h"
+#include "ast_pp.h"
+#include "ast_ll_pp.h"
+#include "ast_smt2_pp.h"
+#include "tactical.h"
+#include "bool_rewriter.h"
+#include "var_subst.h"
+#include "uint_set.h"
+#include "dl_util.h"
+#include "th_rewriter.h"
+#include "dl_util.h"
+
+
+class is_variable_proc {
+public:
+    virtual bool operator()(expr* e) const = 0;
+};
+
+class is_variable_test : public is_variable_proc {
+    enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS };
+    uint_set m_var_set;
+    unsigned m_num_decls;
+    is_var_kind m_var_kind;
+public:
+    is_variable_test(uint_set const& vars, bool index_of_bound) :
+        m_var_set(vars), 
+        m_num_decls(0), 
+        m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {}
+
+    is_variable_test(unsigned num_decls) :
+        m_num_decls(num_decls),
+        m_var_kind(BY_NUM_DECLS) {}
+
+    virtual bool operator()(expr* e) const {
+        if (!is_var(e)) {
+            return false;
+        }
+        unsigned idx = to_var(e)->get_idx();
+        switch(m_var_kind) {
+        case BY_VAR_SET:
+            return m_var_set.contains(idx);
+        case BY_VAR_SET_COMPLEMENT:
+            return !m_var_set.contains(idx);
+        case BY_NUM_DECLS:
+            return idx < m_num_decls;
+        }
+        UNREACHABLE();
+        return false;
+    }
+};
+
 
 class der2 {
     ast_manager &   m;
+    is_variable_proc* m_is_variable;
     var_subst       m_subst;
     expr_ref_buffer m_new_exprs;
     
@@ -43,6 +86,119 @@ class der2 {
     unsigned_vector  m_order;
     expr_ref_vector  m_subst_map;
     expr_ref_buffer  m_new_args;
+    th_rewriter      m_rewriter;
+
+    void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
+        order.reset();
+        
+        // eliminate self loops, and definitions containing quantifiers.
+        bool found = false;
+        for (unsigned i = 0; i < definitions.size(); i++) {
+            var * v  = vars[i];
+            expr * t = definitions[i];
+            if (t == 0 || has_quantifiers(t) || occurs(v, t))
+                definitions[i] = 0;
+            else
+                found = true; // found at least one candidate
+        }
+        
+        if (!found)
+            return;
+        
+        typedef std::pair<expr *, unsigned> frame;
+        svector<frame> todo;
+        
+        expr_fast_mark1 visiting;
+        expr_fast_mark2 done;
+        
+        unsigned vidx, num;
+        
+        for (unsigned i = 0; i < definitions.size(); i++) {
+            if (definitions[i] == 0)
+                continue;
+            var * v = vars[i];
+            SASSERT(v->get_idx() == i);
+            SASSERT(todo.empty());
+            todo.push_back(frame(v, 0));
+            while (!todo.empty()) {
+            start:
+                frame & fr = todo.back();
+                expr * t   = fr.first;
+                if (t->get_ref_count() > 1 && done.is_marked(t)) {
+                    todo.pop_back();
+                    continue;
+                }
+                switch (t->get_kind()) {
+                case AST_VAR:
+                    vidx = to_var(t)->get_idx();
+                    if (fr.second == 0) {
+                        CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
+                        // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
+                        if (definitions.get(vidx, 0) != 0) {
+                            if (visiting.is_marked(t)) {
+                                // cycle detected: remove t
+                                visiting.reset_mark(t);
+                                definitions[vidx] = 0;
+                            }
+                            else {
+                                visiting.mark(t);
+                                fr.second = 1;
+                                todo.push_back(frame(definitions[vidx], 0));
+                                goto start;
+                            }
+                        }
+                    }
+                    else {
+                        SASSERT(fr.second == 1);
+                        if (definitions.get(vidx, 0) != 0) {
+                            visiting.reset_mark(t);
+                            order.push_back(vidx);
+                        }
+                        else {
+                            // var was removed from the list of candidate vars to elim cycle
+                            // do nothing
+                        }
+                    }
+                    if (t->get_ref_count() > 1)
+                        done.mark(t);
+                    todo.pop_back();
+                    break;
+                case AST_QUANTIFIER:
+                    UNREACHABLE();
+                    todo.pop_back();
+                    break;
+                case AST_APP:
+                    num = to_app(t)->get_num_args();
+                    while (fr.second < num) {
+                        expr * arg = to_app(t)->get_arg(fr.second);
+                        fr.second++;
+                        if (arg->get_ref_count() > 1 && done.is_marked(arg))
+                            continue;
+                        todo.push_back(frame(arg, 0));
+                        goto start;
+                    }
+                    if (t->get_ref_count() > 1)
+                        done.mark(t);
+                    todo.pop_back();
+                    break;
+                default:
+                    UNREACHABLE();
+                    todo.pop_back();
+                    break;
+                }
+            }
+        }
+    }
+
+    bool is_variable(expr * e) const {
+        return (*m_is_variable)(e);
+    }
+    
+    bool is_neg_var(ast_manager & m, expr * e) {
+        expr* e1;
+        return m.is_not(e, e1) && is_variable(e1);
+    }
+
 
     /**
        \brief Return true if e can be viewed as a variable disequality. 
@@ -54,424 +210,1668 @@ class der2 {
               (not T) is used because this formula is equivalent to (not (iff (VAR 2) (not T))),
               and can be viewed as a disequality.
     */
-    bool is_var_diseq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
+    bool is_var_diseq(expr * e, var * & v, expr_ref & t) {
+        expr* e1;
+        if (m.is_not(e, e1)) {
+            return is_var_eq(e, v, t);
+        }
+        else if (is_var_eq(e, v, t) && m.is_bool(v)) { 
+            bool_rewriter(m).mk_not(t, t);
+            m_new_exprs.push_back(t);
+            return true;
+        }
+        else {
+            return false;
+        }
+    }
+
+
 
     /**
        \brief Return true if e can be viewed as a variable equality.
     */
-    bool is_var_eq(expr * e, unsigned num_decls, var *& v, expr_ref & t);
 
-    bool is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t);
-
-    void get_elimination_order();
-    void create_substitution(unsigned sz);
-    void apply_substitution(quantifier * q, expr_ref & r);
-    void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr);
-    void elim_unused_vars(expr_ref& r, proof_ref &pr);
-
-public:
-    der2(ast_manager & m):m(m),m_subst(m),m_new_exprs(m),m_subst_map(m),m_new_args(m) {}
-    void operator()(quantifier * q, expr_ref & r, proof_ref & pr);
-    void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr);
-    ast_manager& get_manager() const { return m; }
-};
-
-static bool is_var(expr * e, unsigned num_decls) {
-    return is_var(e) && to_var(e)->get_idx() < num_decls;
-}
-
-static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
-    expr* e1;
-    return m.is_not(e, e1) && is_var(e1, num_decls);
-}
-
-bool der2::is_var_def(bool check_eq, expr* e, unsigned num_decls, var*& v, expr_ref& t) {
-    if (check_eq) {
-        return is_var_eq(e, num_decls, v, t);
-    }
-    else {
-        return is_var_diseq(e, num_decls, v, t);
-    }    
-}
-
-bool der2::is_var_eq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
-    expr* lhs, *rhs;
-    
-    // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases    
-    if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
-        // (iff (not VAR) t) (iff t (not VAR)) cases
-        if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls) && m.is_bool(lhs)) {
-            if (!is_neg_var(m, lhs, num_decls)) {
+    bool is_var_eq(expr * e, var * & v, expr_ref & t) {
+        expr* lhs, *rhs;
+        
+        // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases    
+        if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) {
+            // (iff (not VAR) t) (iff t (not VAR)) cases
+            if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) {
+                if (!is_neg_var(m, lhs)) {
+                    std::swap(lhs, rhs);
+                }
+                if (!is_neg_var(m, lhs)) {
+                    return false;
+                }
+                v = to_var(lhs);
+                t = m.mk_not(rhs);
+                m_new_exprs.push_back(t);
+                TRACE("der", tout << mk_pp(e, m) << "\n";);
+                return true;
+            }
+            if (!is_variable(lhs))
                 std::swap(lhs, rhs);
-            }
-            if (!is_neg_var(m, lhs, num_decls)) {
+            if (!is_variable(lhs))
                 return false;
-            }
             v = to_var(lhs);
-            t = m.mk_not(rhs);
-            m_new_exprs.push_back(t);
+            t = rhs;
             TRACE("der", tout << mk_pp(e, m) << "\n";);
             return true;
         }
-        if (!is_var(lhs, num_decls))
-            std::swap(lhs, rhs);
-        if (!is_var(lhs, num_decls))
+        
+        // (ite cond (= VAR t) (= VAR t2)) case
+        expr* cond, *e2, *e3;
+        if (m.is_ite(e, cond, e2, e3)) {
+            if (is_var_eq(e2, v, t)) {
+                expr_ref t2(m);
+                var* v2;
+                if (is_var_eq(e3, v2, t2) && v2 == v) {
+                    t = m.mk_ite(cond, t, t2);
+                    m_new_exprs.push_back(t);
+                    return true;
+                }
+            }
             return false;
-        v = to_var(lhs);
-        t = rhs;
-        TRACE("der", tout << mk_pp(e, m) << "\n";);
-        return true;
+        }
+        
+        // VAR = true case
+        if (is_variable(e)) {
+            t = m.mk_true();
+            v = to_var(e);
+            TRACE("der", tout << mk_pp(e, m) << "\n";);
+            return true;
+        }
+        
+        // VAR = false case
+        if (is_neg_var(m, e)) {
+            t = m.mk_false();
+            v = to_var(to_app(e)->get_arg(0));
+            TRACE("der", tout << mk_pp(e, m) << "\n";);
+            return true;
+        }
+        
+        return false;
     }
 
-    // (ite cond (= VAR t) (= VAR t2)) case
-    expr* cond, *e2, *e3;
-    if (m.is_ite(e, cond, e2, e3)) {
-        if (is_var_eq(e2, num_decls, v, t)) {
-            expr_ref t2(m);
-            var* v2;
-            if (is_var_eq(e3, num_decls, v2, t2) && v2 == v) {
-                t = m.mk_ite(cond, t, t2);
-                m_new_exprs.push_back(t);
+
+    bool is_var_def(bool check_eq, expr* e, var*& v, expr_ref& t) {
+        if (check_eq) {
+            return is_var_eq(e, v, t);
+        }
+        else {
+            return is_var_diseq(e, v, t);
+        }    
+    }
+
+    void get_elimination_order() {
+        m_order.reset();
+
+        TRACE("top_sort",
+              tout << "DEFINITIONS: " << std::endl;
+              for(unsigned i = 0; i < m_map.size(); i++)
+                  if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl;
+              );
+        
+        der_sort_vars(m_inx2var, m_map, m_order);
+        
+        TRACE("der", 
+              tout << "Elimination m_order:" << std::endl;
+              for(unsigned i=0; i<m_order.size(); i++)
+                  {
+                      if (i != 0) tout << ",";
+                      tout << m_order[i];
+                  }
+              tout << std::endl;            
+              );
+    }    
+
+    void create_substitution(unsigned sz) {
+        m_subst_map.reset();
+        m_subst_map.resize(sz, 0);        
+        for (unsigned i = 0; i < m_order.size(); i++) {
+            expr_ref cur(m_map[m_order[i]], m);            
+            // do all the previous substitutions before inserting
+            expr_ref r(m);
+            m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);            
+            unsigned inx = sz - m_order[i]- 1;
+            SASSERT(m_subst_map[inx]==0);
+            m_subst_map[inx] = r;
+        }
+    }
+
+    void apply_substitution(quantifier * q, expr_ref & r) {
+        expr * e = q->get_expr();
+        unsigned num_args = to_app(e)->get_num_args(); 
+        bool_rewriter rw(m);
+        
+        // get a new expression
+        m_new_args.reset();
+        for(unsigned i = 0; i < num_args; i++) {
+            int x = m_pos2var[i];
+            if (x != -1 && m_map[x] != 0) 
+                continue; // this is a disequality/equality with definition (vanishes)
+            
+            m_new_args.push_back(to_app(e)->get_arg(i));
+        }
+        
+        expr_ref t(m);
+        if (q->is_forall()) {
+            rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t);
+        }
+        else {
+            rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t);
+        }
+        expr_ref new_e(m);    
+        m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
+        
+        // don't forget to update the quantifier patterns
+        expr_ref_buffer  new_patterns(m);
+        expr_ref_buffer  new_no_patterns(m);
+        for (unsigned j = 0; j < q->get_num_patterns(); j++) {
+            expr_ref new_pat(m);
+            m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat);
+            new_patterns.push_back(new_pat);
+        }
+        
+        for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
+            expr_ref new_nopat(m);
+            m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat);
+            new_no_patterns.push_back(new_nopat);
+        }
+        
+        r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), 
+                                new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
+    }
+
+    void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) {
+        expr * e = q->get_expr();
+        is_variable_test is_v(q->get_num_decls());
+        set_is_variable_proc(is_v);
+        unsigned num_args = 1;
+        expr* const* args = &e;
+        if ((q->is_forall() && m.is_or(e)) ||
+            (q->is_exists() && m.is_and(e))) {
+            num_args = to_app(e)->get_num_args();
+            args     = to_app(e)->get_args();
+        }
+        
+        unsigned def_count = 0;
+        unsigned largest_vinx = 0;
+        
+        find_definitions(num_args, args, q->is_exists(), def_count, largest_vinx);
+        
+        if (def_count > 0) {
+            get_elimination_order();
+            SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
+            
+            if (!m_order.empty()) {            
+                create_substitution(largest_vinx + 1);
+                apply_substitution(q, r);
+            }
+            else {
+                r = q;
+            }
+        }
+        else {
+            TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
+            r = q;
+        }
+        
+        if (m.proofs_enabled()) {
+            pr = r == q ? 0 : m.mk_der(q, r);
+        }    
+    }    
+
+    void elim_unused_vars(expr_ref& r, proof_ref &pr) {
+        if (is_quantifier(r)) {
+            quantifier * q = to_quantifier(r);
+            ::elim_unused_vars(m, q, r);
+            if (m.proofs_enabled()) {
+                proof * p1 = m.mk_elim_unused_vars(q, r);
+                pr = m.mk_transitivity(pr, p1);
+            }
+        }
+    }
+
+    void find_definitions(unsigned num_args, expr* const* args, bool is_exists, unsigned& def_count, unsigned& largest_vinx) {
+        var * v = 0;
+        expr_ref t(m);    
+        def_count = 0;
+        largest_vinx = 0;
+        m_map.reset();
+        m_pos2var.reset();
+        m_inx2var.reset();    
+        m_pos2var.reserve(num_args, -1);
+        
+        // Find all definitions
+        for (unsigned i = 0; i < num_args; i++) {
+            if (is_var_def(is_exists, args[i], v, t)) {
+                unsigned idx = v->get_idx();
+                if(m_map.get(idx, 0) == 0) {
+                    m_map.reserve(idx + 1, 0);
+                    m_inx2var.reserve(idx + 1, 0);                
+                    m_map[idx] = t;
+                    m_inx2var[idx] = v;
+                    m_pos2var[i] = idx;
+                    def_count++;
+                    largest_vinx = std::max(idx, largest_vinx); 
+                }
+            }
+        }
+    }
+
+    bool reduce_var_set(expr_ref_vector& conjs) {
+        unsigned def_count = 0;
+        unsigned largest_vinx = 0;
+        
+        find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx);
+        
+        if (def_count > 0) {
+            get_elimination_order();
+            SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
+            
+            if (!m_order.empty()) {            
+                expr_ref r(m), new_r(m);
+                r = m.mk_and(conjs.size(), conjs.c_ptr());
+                create_substitution(largest_vinx + 1);
+                m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r);
+                m_rewriter(new_r);
+                conjs.reset();
+                datalog::flatten_and(new_r, conjs);
                 return true;
             }
         }
         return false;
     }
 
-    // VAR = true case
-    if (is_var(e, num_decls)) {
-        t = m.mk_true();
-        v = to_var(e);
-        TRACE("der", tout << mk_pp(e, m) << "\n";);
-        return true;
-    }
 
-    // VAR = false case
-    if (is_neg_var(m, e, num_decls)) {
-        t = m.mk_false();
-        v = to_var(to_app(e)->get_arg(0));
-        TRACE("der", tout << mk_pp(e, m) << "\n";);
-        return true;
-    }
+public:
+    der2(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {}
 
-    return false;
-}
+    void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
 
-/**
-   \brief Return true if \c e is of the form (not (= VAR t)) or (not (iff VAR t)) or 
-                                (iff VAR t) or (iff (not VAR) t) or (VAR IDX) or (not (VAR IDX)).
-   The last case can be viewed 
-*/
-bool der2::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
-    expr* e1;
-    if (m.is_not(e, e1)) {
-        return is_var_eq(e, num_decls, v, t);
-    }
-    else if (is_var_eq(e, num_decls, v, t) && m.is_bool(v)) { 
-        bool_rewriter(m).mk_not(t, t);
-        m_new_exprs.push_back(t);
-        return true;
-    }
-    else {
-        return false;
-    }
-}
-
-void der2::elim_unused_vars(expr_ref& r, proof_ref& pr) {
-    if (is_quantifier(r)) {
-        quantifier * q = to_quantifier(r);
-        ::elim_unused_vars(m, q, r);
-        if (m.proofs_enabled()) {
-            proof * p1 = m.mk_elim_unused_vars(q, r);
-            pr = m.mk_transitivity(pr, p1);
+    void operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
+        TRACE("der", tout << mk_pp(q, m) << "\n";);    
+        pr = 0;
+        r  = q;
+        reduce_quantifier(q, r, pr);    
+        if (r != q) {
+            elim_unused_vars(r, pr);
         }
     }
-}
 
-/**
-   Reduce the set of definitions in quantifier.
-   Then eliminate variables that have become unused
-*/
-void der2::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
-    TRACE("der", tout << mk_pp(q, m) << "\n";);    
-    pr = 0;
-    r  = q;
-    reduce_quantifier(q, r, pr);    
-    if (r != q) {
-        elim_unused_vars(r, pr);
-    }
-}
-
-void der2::reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) {   
-    r = q;
-    // Keep applying reduce_quantifier1 until r doesn't change anymore
-    do {
-        proof_ref curr_pr(m);
-        q  = to_quantifier(r);
-        reduce_quantifier1(q, r, curr_pr);
-        if (m.proofs_enabled()) {
-            pr = m.mk_transitivity(pr, curr_pr);
-        }
-    } while (q != r && is_quantifier(r));
-
-    m_new_exprs.reset();
-}
-
-void der2::reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) {    
-    expr * e = q->get_expr();
-    unsigned num_decls = q->get_num_decls();
-    var * v = 0;
-    expr_ref t(m);    
-    unsigned num_args = 1;
-    expr* const* args = &e;
-    if ((q->is_forall() && m.is_or(e)) ||
-        (q->is_exists() && m.is_and(e))) {
-        num_args = to_app(e)->get_num_args();
-        args     = to_app(e)->get_args();
-    }
-
-    unsigned def_count = 0;
-    unsigned largest_vinx = 0;
-    
-    m_map.reset();
-    m_pos2var.reset();
-    m_inx2var.reset();    
-    m_pos2var.reserve(num_args, -1);
-    
-    // Find all definitions
-    for (unsigned i = 0; i < num_args; i++) {
-        if (is_var_def(q->is_exists(), args[i], num_decls, v, t)) {
-            unsigned idx = v->get_idx();
-            if(m_map.get(idx, 0) == 0) {
-                m_map.reserve(idx + 1, 0);
-                m_inx2var.reserve(idx + 1, 0);                
-                m_map[idx] = t;
-                m_inx2var[idx] = v;
-                m_pos2var[i] = idx;
-                def_count++;
-                largest_vinx = std::max(idx, largest_vinx); 
-            }
-        }
-    }
-    
-    if (def_count > 0) {
-        get_elimination_order();
-        SASSERT(m_order.size() <= def_count); // some might be missing because of cycles
-        
-        if (!m_order.empty()) {            
-            create_substitution(largest_vinx + 1);
-            apply_substitution(q, r);
-        }
-        else {
-            r = q;
-        }
-    }
-    else {
-        TRACE("der_bug", tout << "Did not find any diseq\n" << mk_pp(q, m) << "\n";);
+    void reduce_quantifier(quantifier * q, expr_ref & r, proof_ref & pr) {   
         r = q;
-    }
- 
-    if (m.proofs_enabled()) {
-        pr = r == q ? 0 : m.mk_der(q, r);
-    }    
-}
-
-static void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsigned_vector & order) {
-    order.reset();
-    
-    // eliminate self loops, and definitions containing quantifiers.
-    bool found = false;
-    for (unsigned i = 0; i < definitions.size(); i++) {
-        var * v  = vars[i];
-        expr * t = definitions[i];
-        if (t == 0 || has_quantifiers(t) || occurs(v, t))
-            definitions[i] = 0;
-        else
-            found = true; // found at least one candidate
-    }
-    
-    if (!found)
-        return;
-
-    typedef std::pair<expr *, unsigned> frame;
-    svector<frame> todo;
-
-    expr_fast_mark1 visiting;
-    expr_fast_mark2 done;
-
-    unsigned vidx, num;
-
-    for (unsigned i = 0; i < definitions.size(); i++) {
-        if (definitions[i] == 0)
-            continue;
-        var * v = vars[i];
-        SASSERT(v->get_idx() == i);
-        SASSERT(todo.empty());
-        todo.push_back(frame(v, 0));
-        while (!todo.empty()) {
-        start:
-            frame & fr = todo.back();
-            expr * t   = fr.first;
-            if (t->get_ref_count() > 1 && done.is_marked(t)) {
-                todo.pop_back();
-                continue;
+        // Keep applying reduce_quantifier1 until r doesn't change anymore
+        do {
+            proof_ref curr_pr(m);
+            q  = to_quantifier(r);
+            reduce_quantifier1(q, r, curr_pr);
+            if (m.proofs_enabled()) {
+                pr = m.mk_transitivity(pr, curr_pr);
             }
-            switch (t->get_kind()) {
-            case AST_VAR:
-                vidx = to_var(t)->get_idx();
-                if (fr.second == 0) {
-                    CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
-                    // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
-                    if (definitions.get(vidx, 0) != 0) {
-                        if (visiting.is_marked(t)) {
-                            // cycle detected: remove t
-                            visiting.reset_mark(t);
-                            definitions[vidx] = 0;
-                        }
-                        else {
-                            visiting.mark(t);
-                            fr.second = 1;
-                            todo.push_back(frame(definitions[vidx], 0));
-                            goto start;
-                        }
+        } while (q != r && is_quantifier(r));
+        
+        m_new_exprs.reset();
+    }
+
+    void operator()(expr_ref_vector& r) {
+        while (reduce_var_set(r)) ;
+        m_new_exprs.reset();
+    }
+
+    ast_manager& get_manager() const { return m; }
+};
+
+// ------------------------------------------------------------
+// fm_tactic adapted to eliminate designated de-Brujin indices.
+
+namespace fm {
+    typedef ptr_vector<app> clauses;
+    typedef unsigned        var;
+    typedef int             bvar;
+    typedef int             literal;
+    typedef svector<var>    var_vector;
+
+    // Encode the constraint
+    // lits \/ ( as[0]*xs[0] + ... + as[num_vars-1]*xs[num_vars-1] <= c
+    // if strict is true, then <= is <.
+    struct constraint {
+        static unsigned get_obj_size(unsigned num_lits, unsigned num_vars) {
+            return sizeof(constraint) + num_lits*sizeof(literal) + num_vars*(sizeof(var) + sizeof(rational));
+        }
+        unsigned           m_id;
+        unsigned           m_num_lits:29;
+        unsigned           m_strict:1;
+        unsigned           m_dead:1;
+        unsigned           m_mark:1;
+        unsigned           m_num_vars;
+        literal *          m_lits;
+        var *              m_xs;
+        rational  *        m_as;
+        rational           m_c;
+        expr_dependency *  m_dep;
+        ~constraint() {
+            rational * it  = m_as;
+            rational * end = it + m_num_vars;
+            for (; it != end; ++it)
+                it->~rational();
+        }
+        
+        unsigned hash() const { return hash_u(m_id); }
+    };
+    
+    typedef ptr_vector<constraint> constraints;
+    
+    class constraint_set {
+        unsigned_vector m_id2pos; 
+        constraints     m_set;
+    public:
+        typedef constraints::const_iterator iterator;
+        
+        bool contains(constraint const & c) const { 
+            if (c.m_id >= m_id2pos.size()) 
+                return false; 
+            return m_id2pos[c.m_id] != UINT_MAX; 
+        }
+        
+        bool empty() const { return m_set.empty(); }
+        unsigned size() const { return m_set.size(); }
+        
+        void insert(constraint & c) {
+            unsigned id  = c.m_id;
+            m_id2pos.reserve(id+1, UINT_MAX);
+            if (m_id2pos[id] != UINT_MAX)
+                return; // already in the set
+            unsigned pos = m_set.size();
+            m_id2pos[id] = pos;
+            m_set.push_back(&c);
+        }
+        
+        void erase(constraint & c) {
+            unsigned id = c.m_id;
+            if (id >= m_id2pos.size())
+                return;
+            unsigned pos = m_id2pos[id];
+            if (pos == UINT_MAX)
+                return;
+            m_id2pos[id] = UINT_MAX;
+            unsigned last_pos = m_set.size() - 1;
+            if (pos != last_pos) {
+                constraint * last_c = m_set[last_pos];
+                m_set[pos] = last_c; 
+                m_id2pos[last_c->m_id] = pos;
+            }
+            m_set.pop_back();
+        }
+        
+        constraint & erase() {
+            SASSERT(!empty());
+            constraint & c = *m_set.back(); 
+            m_id2pos[c.m_id] = UINT_MAX;
+            m_set.pop_back();
+            return c;
+        }
+        
+        void reset() { m_id2pos.reset(); m_set.reset(); }
+        void finalize() { m_id2pos.finalize(); m_set.finalize(); }
+        
+        iterator begin() const { return m_set.begin(); }
+        iterator end() const { return m_set.end(); }
+    };
+    
+    class fm {
+        ast_manager &            m;
+        is_variable_proc*        m_is_variable;
+        small_object_allocator   m_allocator;
+        arith_util               m_util;
+        constraints              m_constraints;
+        expr_ref_vector          m_bvar2expr;
+        char_vector              m_bvar2sign;
+        obj_map<expr, bvar>      m_expr2bvar;
+        char_vector              m_is_int;
+        char_vector              m_forbidden;
+        expr_ref_vector          m_var2expr;
+        obj_map<expr, var>       m_expr2var;
+        unsigned_vector          m_var2pos;
+        vector<constraints>      m_lowers;
+        vector<constraints>      m_uppers;
+        uint_set                 m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part
+        expr_ref_vector          m_new_fmls;
+        volatile bool            m_cancel;
+        id_gen                   m_id_gen;
+        bool                     m_fm_real_only;
+        unsigned                 m_fm_limit;
+        unsigned                 m_fm_cutoff1;
+        unsigned                 m_fm_cutoff2;
+        unsigned                 m_fm_extra;
+        bool                     m_fm_occ;
+        unsigned long long       m_max_memory;
+        unsigned                 m_counter;
+        bool                     m_inconsistent;
+        expr_dependency_ref      m_inconsistent_core;
+        constraint_set           m_sub_todo;
+        
+        // ---------------------------
+        //
+        // OCC clause recognizer
+        //
+        // ---------------------------
+        
+        bool is_literal(expr * t) const {
+            expr * atom;
+            return is_uninterp_const(t) || (m.is_not(t, atom) && is_uninterp_const(atom));
+        }
+        
+        bool is_constraint(expr * t) const {
+            return !is_literal(t);
+        }
+        
+        bool is_var(expr * t, expr * & x) const {
+            
+            if ((*m_is_variable)(t)) {
+                x = t;
+                return true;
+            }
+            else if (m_util.is_to_real(t) && (*m_is_variable)(to_app(t)->get_arg(0))) {
+                x = to_app(t)->get_arg(0);
+                return true;
+            }
+            return false;
+        }
+        
+        bool is_var(expr * t) const {
+            expr * x;
+            return is_var(t, x);
+        }
+        
+        bool is_linear_mon_core(expr * t, expr * & x) const {
+            expr * c;
+            if (m_util.is_mul(t, c, x) && m_util.is_numeral(c) && is_var(x, x))
+                return true;
+            return is_var(t, x);
+        }
+        
+        bool is_linear_mon(expr * t) const {
+            expr * x;
+            return is_linear_mon_core(t, x);
+        }
+        
+        bool is_linear_pol(expr * t) const {
+            unsigned       num_mons;
+            expr * const * mons;
+            if (m_util.is_add(t)) {
+                num_mons = to_app(t)->get_num_args();
+                mons     = to_app(t)->get_args();
+            }
+            else {
+                num_mons = 1;
+                mons     = &t;
+            }
+            
+            expr_fast_mark2 visited;
+            bool all_forbidden = true;
+            for (unsigned i = 0; i < num_mons; i++) {
+                expr * x;
+                if (!is_linear_mon_core(mons[i], x))
+                    return false;
+                if (visited.is_marked(x))
+                    return false; // duplicates are not supported... must simplify first
+                visited.mark(x);
+                SASSERT(::is_var(x));
+                if (!m_forbidden_set.contains(::to_var(x)->get_idx()) && (!m_fm_real_only || !m_util.is_int(x)))
+                    all_forbidden = false;
+            }
+            return !all_forbidden;
+        }
+        
+        bool is_linear_ineq(expr * t) const {
+            m.is_not(t, t);
+            expr * lhs, * rhs;
+            TRACE("is_occ_bug", tout << mk_pp(t, m) << "\n";);
+            if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) {
+                if (!m_util.is_numeral(rhs))
+                    return false;
+                return is_linear_pol(lhs);
+            }
+            return false;
+        }
+        
+        bool is_occ(expr * t) {
+            if (m_fm_occ && m.is_or(t)) {
+                unsigned num = to_app(t)->get_num_args();
+                bool found = false;
+                for (unsigned i = 0; i < num; i++) {
+                    expr * l = to_app(t)->get_arg(i);
+                    if (is_literal(l)) {
+                        continue;
                     }
-                }
-                else {
-                    SASSERT(fr.second == 1);
-                    if (definitions.get(vidx, 0) != 0) {
-                        visiting.reset_mark(t);
-                        order.push_back(vidx);
+                    else if (is_linear_ineq(l)) {
+                        if (found)
+                            return false;
+                        found = true;
                     }
                     else {
-                        // var was removed from the list of candidate vars to elim cycle
-                        // do nothing
+                        return false;
                     }
                 }
-                if (t->get_ref_count() > 1)
-                    done.mark(t);
-                todo.pop_back();
-                break;
-            case AST_QUANTIFIER:
-                UNREACHABLE();
-                todo.pop_back();
-                break;
-            case AST_APP:
-                num = to_app(t)->get_num_args();
-                while (fr.second < num) {
-                    expr * arg = to_app(t)->get_arg(fr.second);
-                    fr.second++;
-                    if (arg->get_ref_count() > 1 && done.is_marked(arg))
-                        continue;
-                    todo.push_back(frame(arg, 0));
-                    goto start;
+                return found;
+            }
+            return is_linear_ineq(t);
+        }
+        
+        // ---------------------------
+        //
+        // Memory mng
+        //
+        // ---------------------------
+        void del_constraint(constraint * c) {
+            m.dec_ref(c->m_dep);
+            m_sub_todo.erase(*c);
+            m_id_gen.recycle(c->m_id);
+            c->~constraint();
+            unsigned sz = constraint::get_obj_size(c->m_num_lits, c->m_num_vars);
+            m_allocator.deallocate(sz, c);
+        }
+
+        void del_constraints(unsigned sz, constraint * const * cs) {
+            for (unsigned i = 0; i < sz; i++)
+                del_constraint(cs[i]);
+        }
+        
+        void reset_constraints() {
+            del_constraints(m_constraints.size(), m_constraints.c_ptr());
+            m_constraints.reset();
+        }
+        
+        constraint * mk_constraint(unsigned num_lits, literal * lits, unsigned num_vars, var * xs, rational * as, rational & c, bool strict,
+                                   expr_dependency * dep) {
+            unsigned sz         = constraint::get_obj_size(num_lits, num_vars);
+            char * mem          = static_cast<char*>(m_allocator.allocate(sz));
+            char * mem_as       = mem + sizeof(constraint);
+            char * mem_lits     = mem_as + sizeof(rational)*num_vars;
+            char * mem_xs       = mem_lits + sizeof(literal)*num_lits;
+            constraint * cnstr  = new (mem) constraint();
+            cnstr->m_id         = m_id_gen.mk();
+            cnstr->m_num_lits   = num_lits;
+            cnstr->m_dead       = false;
+            cnstr->m_mark       = false;
+            cnstr->m_strict     = strict;
+            cnstr->m_num_vars   = num_vars;
+            cnstr->m_lits       = reinterpret_cast<literal*>(mem_lits);
+            for (unsigned i = 0; i < num_lits; i++)
+                cnstr->m_lits[i] = lits[i];
+            cnstr->m_xs         = reinterpret_cast<var*>(mem_xs);
+            cnstr->m_as         = reinterpret_cast<rational*>(mem_as);
+            for (unsigned i = 0; i < num_vars; i++) {
+                TRACE("mk_constraint_bug", tout << "xs[" << i << "]: " << xs[i] << "\n";);
+                cnstr->m_xs[i] = xs[i];
+                new (cnstr->m_as + i) rational(as[i]);
+            }
+            cnstr->m_c = c;
+            DEBUG_CODE({
+                for (unsigned i = 0; i < num_vars; i++) {
+                    SASSERT(cnstr->m_xs[i] == xs[i]);
+                    SASSERT(cnstr->m_as[i] == as[i]);
                 }
-                if (t->get_ref_count() > 1)
-                    done.mark(t);
-                todo.pop_back();
-                break;
-            default:
-                UNREACHABLE();
-                todo.pop_back();
-                break;
+            });
+            cnstr->m_dep = dep;
+            m.inc_ref(dep);
+            return cnstr;
+        }
+        
+        // ---------------------------
+        //
+        // Util
+        //
+        // ---------------------------
+        
+        unsigned num_vars() const { return m_is_int.size(); }
+        
+        // multiply as and c, by the lcm of their denominators
+        void mk_int(unsigned num, rational * as, rational & c) {
+            rational l = denominator(c);
+            for (unsigned i = 0; i < num; i++)
+                l = lcm(l, denominator(as[i]));
+            if (l.is_one())
+                return;
+            c *= l;
+            SASSERT(c.is_int());
+            for (unsigned i = 0; i < num; i++) {
+                as[i] *= l;
+                SASSERT(as[i].is_int());
             }
         }
-    }
-}
-
-void der2::get_elimination_order() {
-    m_order.reset();
-
-    TRACE("top_sort",
-        tout << "DEFINITIONS: " << std::endl;
-        for(unsigned i = 0; i < m_map.size(); i++)
-            if(m_map[i]) tout << "VAR " << i << " = " << mk_pp(m_map[i], m) << std::endl;
-      );
-
-    // der2::top_sort ts(m);
-    der_sort_vars(m_inx2var, m_map, m_order);
-
-    TRACE("der", 
-            tout << "Elimination m_order:" << std::endl;
-            for(unsigned i=0; i<m_order.size(); i++)
-            {
-                if (i != 0) tout << ",";
-                tout << m_order[i];
+        
+        void normalize_coeffs(constraint & c) {
+            if (c.m_num_vars == 0)
+                return;
+            // compute gcd of all coefficients
+            rational g = c.m_c;
+            if (g.is_neg())
+                g.neg();
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                if (g.is_one())
+                    break;
+                if (c.m_as[i].is_pos())
+                    g = gcd(c.m_as[i], g);
+                else
+                    g = gcd(-c.m_as[i], g);
             }
-            tout << std::endl;            
-          );
-}
+            if (g.is_one())
+                return;
+            c.m_c /= g;
+            for (unsigned i = 0; i < c.m_num_vars; i++)
+                c.m_as[i] /= g;
+        }
+        
+        void display(std::ostream & out, constraint const & c) const {
+            for (unsigned i = 0; i < c.m_num_lits; i++) {
+                literal l = c.m_lits[i];
+                if (sign(l))
+                    out << "~";
+                bvar p    = lit2bvar(l);
+                out << mk_ismt2_pp(m_bvar2expr[p], m);
+                out << " ";
+            }
+            out << "(";
+            if (c.m_num_vars == 0)
+                out << "0";
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                if (i > 0)
+                    out << " + ";
+                if (!c.m_as[i].is_one())
+                    out << c.m_as[i] << "*";
+                out << mk_ismt2_pp(m_var2expr.get(c.m_xs[i]), m);
+            }
+            if (c.m_strict)
+                out << " < ";
+            else
+                out << " <= ";
+            out << c.m_c;
+            out << ")";
+        }
+        
+        /**
+           \brief Return true if c1 subsumes c2
+       
+           c1 subsumes c2 If
+           1) All literals of c1 are literals of c2
+           2) polynomial of c1 == polynomial of c2
+           3) c1.m_c <= c2.m_c
+        */
+        bool subsumes(constraint const & c1, constraint const & c2) {
+            if (&c1 == &c2)
+                return false;
+            // quick checks first
+            if (c1.m_num_lits > c2.m_num_lits)
+                return false;
+            if (c1.m_num_vars != c2.m_num_vars)
+                return false;
+            if (c1.m_c > c2.m_c)
+                return false;
+            if (!c1.m_strict && c2.m_strict && c1.m_c == c2.m_c)
+                return false;
+            
+            m_counter += c1.m_num_lits + c2.m_num_lits;
+            
+            for (unsigned i = 0; i < c1.m_num_vars; i++) {
+                m_var2pos[c1.m_xs[i]] = i;
+            }
+            
+            bool failed = false;
+            for (unsigned i = 0; i < c2.m_num_vars; i++) {
+                unsigned pos1 = m_var2pos[c2.m_xs[i]];
+                if (pos1 == UINT_MAX || c1.m_as[pos1] != c2.m_as[i]) {
+                    failed = true;
+                    break;
+                }
+            }
+            
+            for (unsigned i = 0; i < c1.m_num_vars; i++) {
+                m_var2pos[c1.m_xs[i]] = UINT_MAX;
+            }
+            
+            if (failed)
+                return false;
+            
+            for (unsigned i = 0; i < c2.m_num_lits; i++) {
+                literal l = c2.m_lits[i];
+                bvar b    = lit2bvar(l);
+                SASSERT(m_bvar2sign[b] == 0);
+                m_bvar2sign[b] = sign(l) ? -1 : 1;
+            }
+            
+            for (unsigned i = 0; i < c1.m_num_lits; i++) {
+                literal l = c1.m_lits[i];
+                bvar b    = lit2bvar(l);
+                char s    = sign(l) ? -1 : 1;
+                if (m_bvar2sign[b] != s) {
+                    failed = true;
+                    break;
+                }
+            }
+            
+            for (unsigned i = 0; i < c2.m_num_lits; i++) {
+                literal l = c2.m_lits[i];
+                bvar b    = lit2bvar(l);
+                m_bvar2sign[b] = 0;
+            }
+            
+            if (failed)
+                return false;
+            
+            return true;
+        }
+        
+        void backward_subsumption(constraint const & c) {
+            if (c.m_num_vars == 0)
+                return;
+            var      best       = UINT_MAX;
+            unsigned best_sz    = UINT_MAX;
+            bool     best_lower = false;
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                var xi     = c.m_xs[i];
+                if (is_forbidden(xi))
+                    continue; // variable is not in the index
+                bool neg_a = c.m_as[i].is_neg();
+                constraints & cs = neg_a ? m_lowers[xi] : m_uppers[xi];
+                if (cs.size() < best_sz) {
+                    best       = xi;
+                    best_sz    = cs.size();
+                    best_lower = neg_a;
+                }
+            }
+            if (best_sz == 0)
+                return;
+            if (best == UINT_MAX)
+                return; // none of the c variables are in the index.
+            constraints & cs = best_lower ? m_lowers[best] : m_uppers[best];
+            m_counter += cs.size();
+            constraints::iterator it  = cs.begin();
+            constraints::iterator it2 = it;
+            constraints::iterator end = cs.end();
+            for (; it != end; ++it) {
+                constraint * c2 = *it;
+                if (c2->m_dead)
+                    continue;
+                if (subsumes(c, *c2)) {
+                    TRACE("fm_subsumption", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
+                    c2->m_dead = true;
+                    continue;
+                }
+                *it2 = *it;
+                ++it2;
+            }
+            cs.set_end(it2);
+        }
+        
+        void subsume() {
+            while (!m_sub_todo.empty()) {
+                constraint & c = m_sub_todo.erase();
+                if (c.m_dead)
+                    continue;
+                backward_subsumption(c);
+            }
+        }
 
-void der2::create_substitution(unsigned sz) {
-    m_subst_map.reset();
-    m_subst_map.resize(sz, 0);
+    public:
+        
+        // ---------------------------
+        //
+        // Initialization
+        //
+        // ---------------------------
+        
+        fm(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_allocator("fm-elim"),
+            m_util(m),
+            m_bvar2expr(m),
+            m_var2expr(m),
+            m_new_fmls(m),
+            m_inconsistent_core(m) {
+            updt_params(p);
+            m_cancel = false;
+        }
+        
+        ~fm() {
+            reset_constraints();
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+            m_fm_real_only   = p.get_bool(":fm-real-only", true);
+            m_fm_limit       = p.get_uint(":fm-limit", 5000000);
+            m_fm_cutoff1     = p.get_uint(":fm-cutoff1", 8);
+            m_fm_cutoff2     = p.get_uint(":fm-cutoff2", 256);
+            m_fm_extra       = p.get_uint(":fm-extra", 0);
+            m_fm_occ         = p.get_bool(":fm-occ", false);
+        }
+        
+        void set_cancel(bool f) {
+            m_cancel = f;
+        }
+    private:
+        
+        struct forbidden_proc {
+            fm & m_owner;
+            forbidden_proc(fm & o):m_owner(o) {}
+            void operator()(::var * n) {
+                if (m_owner.is_var(n) && m_owner.m.get_sort(n)->get_family_id() == m_owner.m_util.get_family_id()) {
+                    m_owner.m_forbidden_set.insert(n->get_idx());
+                }
+            }
+            void operator()(app * n) { }
+            void operator()(quantifier * n) {}
+        };
+        
+        void init_forbidden_set(expr_ref_vector const & g) {
+            m_forbidden_set.reset();
+            expr_fast_mark1 visited;
+            forbidden_proc  proc(*this);
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++) {
+                expr * f = g[i];
+                if (is_occ(f))
+                    continue;
+                TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
+                quick_for_each_expr(proc, visited, f);
+            }
+        }
+        
+        void init(expr_ref_vector const & g) {
+            m_sub_todo.reset();
+            m_id_gen.reset();
+            reset_constraints();
+            m_bvar2expr.reset();
+            m_bvar2sign.reset();
+            m_bvar2expr.push_back(0); // bvar 0 is not used
+            m_bvar2sign.push_back(0);
+            m_expr2var.reset();
+            m_is_int.reset();
+            m_var2pos.reset();
+            m_forbidden.reset();
+            m_var2expr.reset();
+            m_expr2var.reset();
+            m_lowers.reset();
+            m_uppers.reset();
+            m_new_fmls.reset();
+            m_counter = 0;
+            m_inconsistent = false;
+            m_inconsistent_core = 0;
+            init_forbidden_set(g);
+        }
+        
+        // ---------------------------
+        //
+        // Internal data-structures
+        //
+        // ---------------------------
+        
+        static bool sign(literal l) { return l < 0; }
+        static bvar lit2bvar(literal l) { return l < 0 ? -l : l; }
+        
+        bool is_int(var x) const { 
+            return m_is_int[x] != 0;
+        }
+        
+        bool is_forbidden(var x) const {
+            return m_forbidden[x] != 0;
+        }
+        
+        bool all_int(constraint const & c) const {
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                if (!is_int(c.m_xs[i]))
+                    return false;
+            }
+            return true;
+        }
+        
+        app * to_expr(constraint const & c) {
+            expr * ineq;
+            if (c.m_num_vars == 0) {
+                // 0 <  k (for k > 0)  --> true
+                // 0 <= 0 -- > true
+                if (c.m_c.is_pos() || (!c.m_strict && c.m_c.is_zero()))
+                    return m.mk_true();
+                ineq = 0;
+            }
+            else {
+                bool int_cnstr = all_int(c);
+                ptr_buffer<expr> ms;
+                for (unsigned i = 0; i < c.m_num_vars; i++) {
+                    expr * x = m_var2expr.get(c.m_xs[i]);
+                    if (!int_cnstr && is_int(c.m_xs[i]))
+                        x = m_util.mk_to_real(x);
+                    if (c.m_as[i].is_one())
+                        ms.push_back(x);
+                    else
+                        ms.push_back(m_util.mk_mul(m_util.mk_numeral(c.m_as[i], int_cnstr), x));
+                }
+                expr * lhs;
+                if (c.m_num_vars == 1)
+                    lhs = ms[0];
+                else
+                    lhs = m_util.mk_add(ms.size(), ms.c_ptr());
+                expr * rhs = m_util.mk_numeral(c.m_c, int_cnstr);
+                if (c.m_strict) {
+                    ineq = m.mk_not(m_util.mk_ge(lhs, rhs));
+                }
+                else {
+                    ineq = m_util.mk_le(lhs, rhs);
+                }
+            }
+            
+            if (c.m_num_lits == 0) {
+                if (ineq)
+                    return to_app(ineq);
+                else
+                    return m.mk_false();
+            }
+            
+            ptr_buffer<expr> lits;
+            for (unsigned i = 0; i < c.m_num_lits; i++) {
+                literal l = c.m_lits[i];
+                if (sign(l))
+                    lits.push_back(m.mk_not(m_bvar2expr.get(lit2bvar(l))));
+                else 
+                    lits.push_back(m_bvar2expr.get(lit2bvar(l)));
+            }
+            if (ineq)
+                lits.push_back(ineq);
+            if (lits.size() == 1)
+                return to_app(lits[0]);
+            else
+                return m.mk_or(lits.size(), lits.c_ptr());
+        }
+        
+        var mk_var(expr * t) {
+            SASSERT(::is_var(t));
+            SASSERT(m_util.is_int(t) || m_util.is_real(t));
+            var x = m_var2expr.size();
+            m_var2expr.push_back(t);
+            bool is_int = m_util.is_int(t);
+            m_is_int.push_back(is_int);
+            m_var2pos.push_back(UINT_MAX);
+            m_expr2var.insert(t, x);
+            m_lowers.push_back(constraints());
+            m_uppers.push_back(constraints());
+            bool forbidden = m_forbidden_set.contains(::to_var(t)->get_idx()) || (m_fm_real_only && is_int);
+            m_forbidden.push_back(forbidden);
+            SASSERT(m_var2expr.size()  == m_is_int.size());
+            SASSERT(m_lowers.size()    == m_is_int.size());
+            SASSERT(m_uppers.size()    == m_is_int.size());
+            SASSERT(m_forbidden.size() == m_is_int.size()); 
+            SASSERT(m_var2pos.size()   == m_is_int.size());
+            return x;
+        }
+        
+        bvar mk_bvar(expr * t) {
+            SASSERT(is_uninterp_const(t));
+            SASSERT(m.is_bool(t));
+            bvar p = m_bvar2expr.size();
+            m_bvar2expr.push_back(t);
+            m_bvar2sign.push_back(0);
+            SASSERT(m_bvar2expr.size() == m_bvar2sign.size());
+            m_expr2bvar.insert(t, p);
+            SASSERT(p > 0);
+            return p;
+        }
+        
+        var to_var(expr * t) {
+            var x;
+            if (!m_expr2var.find(t, x))
+                x = mk_var(t);
+            SASSERT(m_expr2var.contains(t));
+            SASSERT(m_var2expr.get(x) == t);
+            TRACE("to_var_bug", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
+            return x;
+        }
+        
+        bvar to_bvar(expr * t) {
+            bvar p;
+            if (m_expr2bvar.find(t, p))
+                return p;
+            return mk_bvar(t);
+        }
+        
+        literal to_literal(expr * t) {
+            if (m.is_not(t, t))
+                return -to_bvar(t); 
+            else
+                return to_bvar(t);
+        }
+        
+        
+        void add_constraint(expr * f, expr_dependency * dep) {
+            SASSERT(!m.is_or(f) || m_fm_occ);
+            sbuffer<literal> lits;
+            sbuffer<var>     xs;
+            buffer<rational> as;
+            rational         c;
+            bool             strict;
+            unsigned         num;
+            expr * const *   args;
+            if (m.is_or(f)) {
+                num  = to_app(f)->get_num_args();
+                args = to_app(f)->get_args();
+            }
+            else {
+                num  = 1;
+                args = &f;
+            }
 
-    for(unsigned i = 0; i < m_order.size(); i++) {
-        expr_ref cur(m_map[m_order[i]], m);
+#if Z3DEBUG
+            bool found_ineq = false;
+#endif
+            for (unsigned i = 0; i < num; i++) {
+                expr * l = args[i];
+                if (is_literal(l)) {
+                    lits.push_back(to_literal(l));
+                }
+                else {
+                    // found inequality
+                    SASSERT(!found_ineq);
+                    DEBUG_CODE(found_ineq = true;);
+                    bool neg    = m.is_not(l, l);
+                    SASSERT(m_util.is_le(l) || m_util.is_ge(l));
+                    strict      = neg;
+                    if (m_util.is_ge(l))
+                        neg = !neg;
+                    expr * lhs = to_app(l)->get_arg(0);
+                    expr * rhs = to_app(l)->get_arg(1);
+                    m_util.is_numeral(rhs, c);
+                    if (neg)
+                        c.neg();
+                    unsigned num_mons;
+                    expr * const * mons;
+                    if (m_util.is_add(lhs)) {
+                        num_mons = to_app(lhs)->get_num_args();
+                        mons     = to_app(lhs)->get_args();
+                    }
+                    else {
+                        num_mons = 1;
+                        mons     = &lhs;
+                    }
+                    
+                    bool all_int = true;
+                    for (unsigned j = 0; j < num_mons; j++) {
+                        expr * monomial = mons[j];
+                        expr * a;
+                        rational a_val;
+                        expr * x;
+                        if (m_util.is_mul(monomial, a, x)) {
+                            VERIFY(m_util.is_numeral(a, a_val));
+                        }
+                        else {
+                            x     = monomial;
+                            a_val = rational(1);
+                        }
+                        if (neg)
+                            a_val.neg();
+                        VERIFY(is_var(x, x));
+                        xs.push_back(to_var(x));
+                        as.push_back(a_val);
+                        if (!is_int(xs.back()))
+                            all_int = false;
+                    }
+                    mk_int(as.size(), as.c_ptr(), c);
+                    if (all_int && strict) {
+                        strict = false;
+                        c--;
+                    }
+                }
+            }
+            
+            TRACE("to_var_bug", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
+            
+            constraint * new_c = mk_constraint(lits.size(),
+                                               lits.c_ptr(),
+                                               xs.size(),
+                                               xs.c_ptr(),
+                                               as.c_ptr(),
+                                               c,
+                                               strict,
+                                               dep);
+            
+            TRACE("to_var_bug", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
+            VERIFY(register_constraint(new_c));
+        }
+        
+        bool is_false(constraint const & c) const {
+            return c.m_num_lits == 0 && c.m_num_vars == 0 && (c.m_c.is_neg() || (c.m_strict && c.m_c.is_zero()));
+        }
+        
+        bool register_constraint(constraint * c) {
+            normalize_coeffs(*c);
+            if (is_false(*c)) {
+                del_constraint(c);
+                m_inconsistent = true;
+                TRACE("add_constraint_bug", tout << "is false "; display(tout, *c); tout << "\n";);
+                return false;
+            }
+            
+            bool r = false;
+            
+            for (unsigned i = 0; i < c->m_num_vars; i++) {
+                var x = c->m_xs[i];
+                if (!is_forbidden(x)) {
+                    r = true;
+                    if (c->m_as[i].is_neg()) 
+                        m_lowers[x].push_back(c);
+                    else
+                        m_uppers[x].push_back(c);
+                }
+            }
+            
+            if (r) {
+                m_sub_todo.insert(*c);
+                m_constraints.push_back(c);
+                return true;
+            }
+            else {
+                TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
+                m_new_fmls.push_back(to_expr(*c));
+                del_constraint(c);
+                return false;
+            }
+        }
+        
+        void init_use_list(expr_ref_vector const & g) {
+            unsigned sz = g.size();
+            for (unsigned i = 0; !m_inconsistent && i < sz; i++) {
+                expr * f = g[i];
+                if (is_occ(f))
+                    add_constraint(f, 0);
+                else
+                    m_new_fmls.push_back(f);
+            }
+        }
 
-        // do all the previous substitutions before inserting
-        expr_ref r(m);
-        m_subst(cur, m_subst_map.size(), m_subst_map.c_ptr(), r);
-
-        unsigned inx = sz - m_order[i]- 1;
-        SASSERT(m_subst_map[inx]==0);
-        m_subst_map[inx] = r;
-    }
-}
-
-void der2::apply_substitution(quantifier * q, expr_ref & r) {
-    expr * e = q->get_expr();
-    unsigned num_args=to_app(e)->get_num_args(); 
-    bool_rewriter rw(m);
+        unsigned get_cost(var x) const {
+            unsigned long long r = static_cast<unsigned long long>(m_lowers[x].size()) * static_cast<unsigned long long>(m_uppers[x].size());
+            if (r > UINT_MAX)
+                return UINT_MAX;
+            return static_cast<unsigned>(r);
+        }
+        
+        typedef std::pair<var, unsigned> x_cost;
     
-    // get a new expression
-    m_new_args.reset();
-    for(unsigned i = 0; i < num_args; i++) {
-        int x = m_pos2var[i];
-        if (x != -1 && m_map[x] != 0) 
-            continue; // this is a disequality with definition (vanishes)
+        struct x_cost_lt {
+            char_vector const m_is_int;
+            x_cost_lt(char_vector & is_int):m_is_int(is_int) {}
+            bool operator()(x_cost const & p1, x_cost const & p2) const { 
+                // Integer variables with cost 0 can be eliminated even if they depend on real variables.
+                // Cost 0 == no lower or no upper bound.
+                if (p1.second == 0) {
+                    if (p2.second > 0) return true;
+                    return p1.first < p2.first;
+                }
+                if (p2.second == 0) return false;
+                bool int1 = m_is_int[p1.first] != 0;
+                bool int2 = m_is_int[p2.first] != 0;
+                return (!int1 && int2) || (int1 == int2 && p1.second < p2.second); 
+            }
+        };
+
+        void sort_candidates(var_vector & xs) {
+            svector<x_cost> x_cost_vector;
+            unsigned num = num_vars();
+            for (var x = 0; x < num; x++) {
+                if (!is_forbidden(x)) {
+                    x_cost_vector.push_back(x_cost(x, get_cost(x)));
+                }
+            }
+            // x_cost_lt is not a total order on variables
+            std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
+            TRACE("fm", 
+                  svector<x_cost>::iterator it2  = x_cost_vector.begin();
+                  svector<x_cost>::iterator end2 = x_cost_vector.end();
+                  for (; it2 != end2; ++it2) {
+                      tout << "(" << mk_ismt2_pp(m_var2expr.get(it2->first), m) << " " << it2->second << ") ";
+                  }
+                  tout << "\n";);
+            svector<x_cost>::iterator it2  = x_cost_vector.begin();
+            svector<x_cost>::iterator end2 = x_cost_vector.end();
+            for (; it2 != end2; ++it2) {
+                xs.push_back(it2->first);
+            }
+        }
+        
+        void cleanup_constraints(constraints & cs) {
+            unsigned j = 0;
+            unsigned sz = cs.size();
+            for (unsigned i = 0; i < sz; i++) {
+                constraint * c = cs[i];
+                if (c->m_dead)
+                    continue;
+                cs[j] = c;
+                j++;
+            }
+            cs.shrink(j);
+        }
+    
+        // Set all_int = true if all variables in c are int.
+        // Set unit_coeff = true if the coefficient of x in c is 1 or -1.
+        // If all_int = false, then unit_coeff may not be set.
+        void analyze(constraint const & c, var x, bool & all_int, bool & unit_coeff) const {
+            all_int    = true;
+            unit_coeff = true;
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                if (!is_int(c.m_xs[i])) {
+                    all_int = false;
+                    return;
+                }
+                if (c.m_xs[i] == x) {
+                    unit_coeff = (c.m_as[i].is_one() || c.m_as[i].is_minus_one());
+                }
+            }
+        }
+
+        void analyze(constraints const & cs, var x, bool & all_int, bool & unit_coeff) const {
+            all_int    = true;
+            unit_coeff = true;
+            constraints::const_iterator it  = cs.begin();
+            constraints::const_iterator end = cs.end();
+            for (; it != end; ++it) {
+                bool curr_unit_coeff;
+                analyze(*(*it), x, all_int, curr_unit_coeff);
+                if (!all_int)
+                    return;
+                if (!curr_unit_coeff)
+                    unit_coeff = false;
+            }
+        }
+        
+        // An integer variable x may be eliminated, if 
+        //   1- All variables in the contraints it occur are integer.
+        //   2- The coefficient of x in all lower bounds (or all upper bounds) is unit.
+        bool can_eliminate(var x) const {
+            if (!is_int(x))
+                return true;
+            bool all_int;
+            bool l_unit, u_unit;
+            analyze(m_lowers[x], x, all_int, l_unit);
+            if (!all_int)
+                return false;
+            analyze(m_uppers[x], x, all_int, u_unit);
+            return all_int && (l_unit || u_unit);
+        }
+        
+        void copy_constraints(constraints const & s, clauses & t) {
+            constraints::const_iterator it  = s.begin();
+            constraints::const_iterator end = s.end();
+            for (; it != end; ++it) {
+                app * c = to_expr(*(*it));
+                t.push_back(c);
+            }
+        }
+        
+        clauses tmp_clauses;
+        void save_constraints(var x) {  }
+        
+        void mark_constraints_dead(constraints const & cs) {
+            constraints::const_iterator it  = cs.begin();
+            constraints::const_iterator end = cs.end();
+            for (; it != end; ++it)
+                (*it)->m_dead = true;
+        }
+        
+        void mark_constraints_dead(var x) {
+            save_constraints(x);
+            mark_constraints_dead(m_lowers[x]);
+            mark_constraints_dead(m_uppers[x]);
+        }
+        
+        void get_coeff(constraint const & c, var x, rational & a) {
+            for (unsigned i = 0; i < c.m_num_vars; i++) {
+                if (c.m_xs[i] == x) {
+                    a = c.m_as[i];
+                    return;
+                }
+            }
+            UNREACHABLE();
+        }
+        
+        var_vector       new_xs;
+        vector<rational> new_as;
+        svector<literal> new_lits;
+        
+        constraint * resolve(constraint const & l, constraint const & u, var x) {
+            m_counter += l.m_num_vars + u.m_num_vars + l.m_num_lits + u.m_num_lits;
+            rational a, b;
+            get_coeff(l, x, a);
+            get_coeff(u, x, b);
+            SASSERT(a.is_neg());
+            SASSERT(b.is_pos());
+            a.neg();
+            
+            SASSERT(!is_int(x) || a.is_one() || b.is_one());
+            
+            new_xs.reset();
+            new_as.reset();
+            rational         new_c = l.m_c*b + u.m_c*a;
+            bool             new_strict = l.m_strict || u.m_strict;
+            
+            for (unsigned i = 0; i < l.m_num_vars; i++) {
+                var xi = l.m_xs[i];
+                if (xi == x)
+                    continue;
+                unsigned pos = new_xs.size();
+                new_xs.push_back(xi);
+                SASSERT(m_var2pos[xi] == UINT_MAX);
+                m_var2pos[xi] = pos;
+                new_as.push_back(l.m_as[i] * b);
+                SASSERT(new_xs[m_var2pos[xi]] == xi);
+                SASSERT(new_xs.size() == new_as.size());
+            }
+            
+            for (unsigned i = 0; i < u.m_num_vars; i++) {
+                var xi = u.m_xs[i];
+                if (xi == x)
+                    continue;
+                unsigned pos = m_var2pos[xi];
+                if (pos == UINT_MAX) {
+                    new_xs.push_back(xi);
+                    new_as.push_back(u.m_as[i] * a);
+                }
+                else {
+                    new_as[pos] += u.m_as[i] * a;
+                }
+            }
+            
+            // remove zeros and check whether all variables are int
+            bool all_int = true;
+            unsigned sz = new_xs.size();
+            unsigned j  = 0;
+            for (unsigned i = 0; i < sz; i++) {
+                if (new_as[i].is_zero())
+                    continue;
+                if (!is_int(new_xs[i]))
+                    all_int = false;
+                if (i != j) {
+                    new_xs[j] = new_xs[i];
+                    new_as[j] = new_as[i];
+                }
+                j++;
+            }
+            new_xs.shrink(j);
+            new_as.shrink(j);
+            
+            if (all_int && new_strict) {
+                new_strict = false;
+                new_c --;
+            }
+            
+            // reset m_var2pos
+            for (unsigned i = 0; i < l.m_num_vars; i++) {
+                m_var2pos[l.m_xs[i]] = UINT_MAX;
+            }
+            
+            if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) {
+                // literal is true
+                TRACE("fm", tout << "resolution " << x << " consequent literal is always true: \n";
+                      display(tout, l);
+                      tout << "\n";
+                      display(tout, u); tout << "\n";);
+                return 0; // no constraint needs to be created.
+            }
+            
+            new_lits.reset();
+            for (unsigned i = 0; i < l.m_num_lits; i++) {
+                literal lit = l.m_lits[i];
+                bvar    p   = lit2bvar(lit);
+                m_bvar2sign[p] = sign(lit) ? -1 : 1;
+                new_lits.push_back(lit);
+            }
+            
+            bool tautology = false;
+            for (unsigned i = 0; i < u.m_num_lits && !tautology; i++) {
+                literal lit = u.m_lits[i];
+                bvar    p   = lit2bvar(lit);
+                switch (m_bvar2sign[p]) {
+                case 0:
+                    new_lits.push_back(lit);
+                break;
+                case -1:
+                    if (!sign(lit))
+                        tautology = true;
+                    break;
+                case 1:
+                    if (sign(lit))
+                        tautology = true;
+                    break;
+                default:
+                    UNREACHABLE();
+                }
+            }
+            
+            // reset m_bvar2sign
+            for (unsigned i = 0; i < l.m_num_lits; i++) {
+                literal lit = l.m_lits[i];
+                bvar    p   = lit2bvar(lit);
+                m_bvar2sign[p] = 0;
+            }
+            
+            if (tautology) {
+                TRACE("fm", tout << "resolution " << x << " tautology: \n";
+                      display(tout, l);
+                      tout << "\n";
+                      display(tout, u); tout << "\n";);
+                return 0;
+            }
+
+            expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep);
+            
+            if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) {
+                TRACE("fm", tout << "resolution " << x << " inconsistent: \n";
+                      display(tout, l);
+                      tout << "\n";
+                      display(tout, u); tout << "\n";);
+                m_inconsistent      = true;
+                m_inconsistent_core = new_dep;
+                return 0;
+            }
+            
+            constraint * new_cnstr = mk_constraint(new_lits.size(),
+                                                   new_lits.c_ptr(),
+                                                   new_xs.size(),
+                                                   new_xs.c_ptr(),
+                                                   new_as.c_ptr(),
+                                                   new_c,
+                                                   new_strict,
+                                                   new_dep);
+
+            TRACE("fm", tout << "resolution " << x << "\n";
+                  display(tout, l);
+                  tout << "\n";
+                  display(tout, u);
+                  tout << "\n---->\n";
+                  display(tout, *new_cnstr); 
+                  tout << "\n";
+                  tout << "new_dep: " << new_dep << "\n";);
+            
+            return new_cnstr;
+        }
+        
+        ptr_vector<constraint> new_constraints;
+        
+        bool try_eliminate(var x) {
+            constraints & l = m_lowers[x];
+            constraints & u = m_uppers[x];
+            cleanup_constraints(l);
+            cleanup_constraints(u);
+            
+            if (l.empty() || u.empty()) {
+                // easy case
+                mark_constraints_dead(x);
+                TRACE("fm", tout << "variable was eliminated (trivial case)\n";);
+                return true;
+            }
+            
+            unsigned num_lowers = l.size();
+            unsigned num_uppers = u.size();
+            
+            if (num_lowers > m_fm_cutoff1 && num_uppers > m_fm_cutoff1)
+                return false;
+            
+            if (num_lowers * num_uppers > m_fm_cutoff2)
+                return false;
+            
+            if (!can_eliminate(x))
+                return false;
+            
+            m_counter += num_lowers * num_uppers;
+            
+            TRACE("fm_bug", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
+                  display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u););
+            
+            unsigned num_old_cnstrs = num_uppers + num_lowers;
+            unsigned limit          = num_old_cnstrs + m_fm_extra;
+            unsigned num_new_cnstrs = 0;
+            new_constraints.reset();
+            for (unsigned i = 0; i < num_lowers; i++) {
+                for (unsigned j = 0; j < num_uppers; j++) {
+                    if (m_inconsistent || num_new_cnstrs > limit) {
+                        TRACE("fm", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
+                        del_constraints(new_constraints.size(), new_constraints.c_ptr());
+                        return false;
+                    }
+                    constraint const & l_c = *(l[i]);
+                    constraint const & u_c = *(u[j]);
+                    constraint * new_c = resolve(l_c, u_c, x);
+                    if (new_c != 0) {
+                        num_new_cnstrs++;
+                        new_constraints.push_back(new_c);
+                    }
+                }
+            }
+            
+            mark_constraints_dead(x);
+            
+            unsigned sz = new_constraints.size();
+            
+            m_counter += sz;
+            
+            for (unsigned i = 0; i < sz; i++) {
+                constraint * c = new_constraints[i];
+                backward_subsumption(*c);
+                register_constraint(c);
+            }
+            TRACE("fm", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
+            return true;
+        }
+        
+        void copy_remaining(vector<constraints> & v2cs) {
+            vector<constraints>::iterator it  = v2cs.begin();
+            vector<constraints>::iterator end = v2cs.end();
+            for (; it != end; ++it) {
+                constraints & cs = *it;
+                constraints::iterator it2  = cs.begin();
+                constraints::iterator end2 = cs.end();
+                for (; it2 != end2; ++it2) {
+                    constraint * c = *it2;
+                    if (!c->m_dead) {
+                        c->m_dead = true;
+                        expr * new_f = to_expr(*c);
+                        TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
+                        m_new_fmls.push_back(new_f);
+                    }
+                }
+            }
+            v2cs.finalize();
+        }
+        
+        // Copy remaining clauses to m_new_fmls
+        void copy_remaining() {
+            copy_remaining(m_uppers);
+            copy_remaining(m_lowers);
+        }
+        
+        void checkpoint() {
+            // cooperate("fm");
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+        }
+    public:
+
+        void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;}
+
+
+        void operator()(expr_ref_vector& fmls) {
+            init(fmls);
+            init_use_list(fmls);
+            if (m_inconsistent) {
+                m_new_fmls.reset();
+                m_new_fmls.push_back(m.mk_false());
+            }
+            else {
+                TRACE("fm", display(tout););
                 
-        m_new_args.push_back(to_app(e)->get_arg(i));
-    }
-
-    expr_ref t(m);
-    if (q->is_forall()) {
-        rw.mk_or(m_new_args.size(), m_new_args.c_ptr(), t);
-    }
-    else {
-        rw.mk_and(m_new_args.size(), m_new_args.c_ptr(), t);
-    }
-    expr_ref new_e(m);    
-    m_subst(t, m_subst_map.size(), m_subst_map.c_ptr(), new_e);
-    
-    // don't forget to update the quantifier patterns
-    expr_ref_buffer  new_patterns(m);
-    expr_ref_buffer  new_no_patterns(m);
-    for (unsigned j = 0; j < q->get_num_patterns(); j++) {
-        expr_ref new_pat(m);
-        m_subst(q->get_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_pat);
-        new_patterns.push_back(new_pat);
-    }
-
-    for (unsigned j = 0; j < q->get_num_no_patterns(); j++) {
-        expr_ref new_nopat(m);
-        m_subst(q->get_no_pattern(j), m_subst_map.size(), m_subst_map.c_ptr(), new_nopat);
-        new_no_patterns.push_back(new_nopat);
-    }
-
-    r = m.update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), 
-                            new_no_patterns.size(), new_no_patterns.c_ptr(), new_e);
-}
-
-
-
+                subsume();
+                var_vector candidates;
+                sort_candidates(candidates);                
+                unsigned eliminated = 0;                
+                
+                unsigned num = candidates.size();
+                for (unsigned i = 0; i < num; i++) {
+                    checkpoint();
+                    if (m_counter > m_fm_limit)
+                        break;
+                    m_counter++;
+                    if (try_eliminate(candidates[i]))
+                        eliminated++;
+                    if (m_inconsistent) {
+                        m_new_fmls.reset();
+                        m_new_fmls.push_back(m.mk_false());
+                        break;
+                    }
+                }
+                if (!m_inconsistent) {
+                    copy_remaining();
+                }
+            }
+            reset_constraints();
+            fmls.reset();
+            fmls.append(m_new_fmls);
+        }        
+        
+        void display_constraints(std::ostream & out, constraints const & cs) const {
+            constraints::const_iterator it  = cs.begin();
+            constraints::const_iterator end = cs.end();
+            for (; it != end; ++it) {
+                out << "  ";
+                display(out, *(*it));
+                out << "\n";
+            }
+        }
+        
+        void display(std::ostream & out) const {
+            unsigned num = num_vars();
+            for (var x = 0; x < num; x++) {
+                if (is_forbidden(x))
+                    continue;
+                out << mk_ismt2_pp(m_var2expr.get(x), m) << "\n";
+                display_constraints(out, m_lowers[x]);
+                display_constraints(out, m_uppers[x]);
+            }
+        }
+    };
 
+} // namespace fm
 
 class qe_lite::impl {
     ast_manager& m;
     der2         m_der;
+    params_ref   m_params;
+    fm::fm       m_fm;
 
 public:
-    impl(ast_manager& m): m(m), m_der(m) {}
+    impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params) {}
     
     void operator()(app_ref_vector& vars, expr_ref& fml) {
         if (vars.empty()) {
@@ -520,6 +1920,26 @@ public:
         }
     }
 
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
+        expr_ref_vector conjs(m);
+        conjs.push_back(fml);
+        (*this)(index_set, index_of_bound, conjs);
+        bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), fml);
+    }
+
+
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
+        datalog::flatten_and(fmls);
+        is_variable_test is_var(index_set, index_of_bound);
+        TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
+        IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) verbose_stream() << mk_pp(fmls[i].get(), m) << "\n";);
+        m_der.set_is_variable_proc(is_var);
+        m_der(fmls);
+        m_fm.set_is_variable_proc(is_var);
+        m_fm(fmls);
+        TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";);
+    }
+
 };
 
 qe_lite::qe_lite(ast_manager& m) {
@@ -537,3 +1957,11 @@ void qe_lite::operator()(app_ref_vector& vars, expr_ref& fml) {
 void qe_lite::operator()(expr_ref& fml, proof_ref& pr) {
     (*m_impl)(fml, pr);
 }
+
+void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) {
+    (*m_impl)(index_set, index_of_bound, fml);
+}
+
+void qe_lite::operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) {
+    (*m_impl)(index_set, index_of_bound, fmls);
+}
diff --git a/src/muz_qe/qe_lite.h b/src/muz_qe/qe_lite.h
index 96166d7c3..3a23c7188 100644
--- a/src/muz_qe/qe_lite.h
+++ b/src/muz_qe/qe_lite.h
@@ -22,6 +22,7 @@ Revision History:
 #define __QE_LITE_H__
 
 #include "ast.h"
+#include "uint_set.h"
 
 class qe_lite {
     class impl;
@@ -40,6 +41,17 @@ public:
     */
     void operator()(app_ref_vector& vars, expr_ref& fml);
 
+    /**
+       \brief
+       Apply light-weight quantifier elimination to variables present/absent in the index set.
+       If 'index_of_bound' is true, then the index_set is treated as the set of
+       bound variables. if 'index_of_bound' is false, then index_set is treated as the
+       set of variables that are not bound (variables that are not in the index set are bound).
+     */
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);
+
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
+
     /**
         \brief full rewriting based light-weight quantifier elimination round.
     */
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index af6861af0..bae63f129 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -77,7 +77,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
 #endif
 
 
-static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) {
+static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml, bool validate) {
     front_end_params params;
     qe::expr_quant_elim qe(m, params);
     qe::guarded_defs defs(m);
@@ -86,7 +86,8 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr*
     std::cout << mk_pp(fml, m) << "\n";
     if (success) {        
         defs.display(std::cout);
-        for (unsigned i = 0; i < defs.size(); ++i) {     
+        
+        for (unsigned i = 0; validate && i < defs.size(); ++i) {     
             validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
         }
     }
@@ -106,6 +107,10 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
            << "(declare-const z Int)\n"
            << "(declare-const a Int)\n"
            << "(declare-const b Int)\n"
+           << "(declare-const P Bool)\n"
+           << "(declare-const Q Bool)\n"
+           << "(declare-const r1 Real)\n"
+           << "(declare-const r2 Real)\n"
            << "(declare-datatypes () ((IList (nil) (cons (car Int) (cdr IList)))))\n"
            << "(declare-const l1 IList)\n"
            << "(declare-const l2 IList)\n"
@@ -140,21 +145,21 @@ static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) {
     }
 }
 
-static void test_quant_solver(ast_manager& m, app* x, char const* str) {
+static void test_quant_solver(ast_manager& m, app* x, char const* str, bool validate = true) {
     expr_ref fml = parse_fml(m, str);
-    test_quant_solver(m, 1, &x, fml);
+    test_quant_solver(m, 1, &x, fml, validate);
 }
 
-static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) {
+static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str, bool validate = true) {
     expr_ref fml = parse_fml(m, str);
-    test_quant_solver(m, sz, xs, fml);
+    test_quant_solver(m, sz, xs, fml, validate);
 }
 
-static void test_quant_solver(ast_manager& m, char const* str) {
+static void test_quant_solver(ast_manager& m, char const* str, bool validate = true) {
     expr_ref fml(m);
     app_ref_vector vars(m);
     parse_fml(str, vars, fml);
-    test_quant_solver(m, vars.size(), vars.c_ptr(), fml);
+    test_quant_solver(m, vars.size(), vars.c_ptr(), fml, validate);
 }
 
 
@@ -222,9 +227,18 @@ static void test_quant_solve1() {
 
     test_quant_solver(m, "(exists ((c Cell)) (= c null))");
     test_quant_solver(m, "(exists ((c Cell)) (= c (cell null c1)))");
-    //TBD:
-    //test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))");
-    //test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))");
+
+    test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))", false);
+    test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
+    test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
+
+    test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
+    test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
+    test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
+    test_quant_solver(m, "(exists ((t Tuple)) (= r2 (third t)))");
+    test_quant_solver(m, "(exists ((t Tuple)) (not (= a (first t))))");
+    test_quant_solver(m, "(exists ((t Tuple)) (not (= P (second t))))");
+    test_quant_solver(m, "(exists ((t Tuple)) (not (= r2 (third t))))");
 }