diff --git a/lib/dl_bmc_engine.cpp b/lib/dl_bmc_engine.cpp
index e15355817..13b3cdeef 100644
--- a/lib/dl_bmc_engine.cpp
+++ b/lib/dl_bmc_engine.cpp
@@ -28,6 +28,7 @@ Revision History:
 #include "bool_rewriter.h"
 #include "model_smt2_pp.h"
 #include "ast_smt_pp.h"
+#include "well_sorted.h"
 
 namespace datalog {
     bmc::bmc(context& ctx): 
@@ -39,11 +40,8 @@ namespace datalog {
         m_rules(ctx),
         m_query_pred(m),
         m_answer(m),
-        m_path_sort(m) {
-        m_fparams.m_model = true;
-        m_fparams.m_model_compact = true;
-        m_fparams.m_mbqi = false;
-        // m_fparams.m_auto_config = false;
+        m_path_sort(m),
+        m_bv(m) {
         }
 
     bmc::~bmc() {}
@@ -95,6 +93,9 @@ namespace datalog {
         }
 
         if (is_linear()) {
+            if (m_ctx.get_engine() == QBMC_ENGINE) {
+                return check_qlinear();
+            }
             return check_linear();
         }
         else {
@@ -113,6 +114,9 @@ namespace datalog {
         return true;
     }
 
+    // --------------------------------------------------------------------------
+    // Basic linear BMC based on incrementally unfolding the transition relation.
+
     void bmc::get_model_linear(unsigned level) {
          rule_manager& rm = m_ctx.get_rule_manager();
          expr_ref level_query = mk_level_predicate(m_query_pred, level);
@@ -124,18 +128,18 @@ namespace datalog {
          SASSERT(m.is_true(md->get_const_interp(to_app(level_query)->get_decl())));
          dl_decl_util util(m);
 
-         TRACE("dl", model_smt2_pp(tout, m, *md, 0););
+         TRACE("bmc", model_smt2_pp(tout, m, *md, 0););
 
          rule_ref r0(rm), r1(rm), r2(rm);
          while (true) {
-             TRACE("dl", tout << "Predicate: " << pred->get_name() << "\n";);
+             TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
              expr_ref_vector sub(m);
              rule_vector const& rls = m_rules.get_predicate_rules(pred);
              rule* r = 0;
              unsigned i = 0;
              for (; i < rls.size(); ++i) {                
                 expr_ref rule_i = mk_level_rule(pred, i, level);
-                TRACE("dl", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
+                TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
                 if (m.is_true(md->get_const_interp(to_app(rule_i)->get_decl()))) {
                     r = rls[i];
                     break;
@@ -210,8 +214,16 @@ namespace datalog {
     }
 
 
-    lbool bmc::check_linear() {
+    void bmc::setup_linear() {
         m_fparams.m_relevancy_lvl = 0;
+        m_fparams.m_model = true;
+        m_fparams.m_model_compact = true;
+        m_fparams.m_mbqi = false;
+        // m_fparams.m_auto_config = false;
+    }
+
+    lbool bmc::check_linear() {
+        setup_linear();
         for (unsigned i = 0; ; ++i) {
             IF_VERBOSE(1, verbose_stream() << "level: " << i << "\n";); 
             checkpoint();
@@ -233,8 +245,8 @@ namespace datalog {
         return m_solver.check(1, &q);
     }
 
-    void bmc::assert_expr(expr* e) {
-        TRACE("dl", tout << mk_pp(e, m) << "\n";);
+    void bmc::assert_expr(expr* e) {        
+        TRACE("bmc", tout << mk_pp(e, m) << "\n";);
         m_solver.assert_expr(e);
     }
 
@@ -258,7 +270,6 @@ namespace datalog {
     }
 
     expr_ref bmc::mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level) {
-        SASSERT(idx < pred->get_arity());
         std::stringstream _name;
         _name << pred->get_name() << "#" << level << "_" << rule_id << "_" << idx;
         symbol nm(_name.str().c_str());        
@@ -328,7 +339,8 @@ namespace datalog {
                 expr_ref rule_i = mk_level_rule(p, i, level);                
                 rules.push_back(rule_i);
                 if (level == 0 && r.get_uninterpreted_tail_size() > 0) {
-                    assert_expr(m.mk_not(rule_i));
+                    tmp = m.mk_not(rule_i);
+                    assert_expr(tmp);
                     continue;
                 }
 
@@ -354,22 +366,333 @@ namespace datalog {
                     conjs.push_back(tmp);
                 }
                 bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
-                
-                assert_expr(m.mk_implies(rule_i, rule_body));
+                rule_body = m.mk_implies(rule_i, rule_body);
+                assert_expr(rule_body);
             }
             bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), tmp);
-            assert_expr(m.mk_implies(level_pred, tmp));
+            tmp = m.mk_implies(level_pred, tmp);
+            assert_expr(tmp);
         }
     }
 
+    // ---------------------------------------------------------------------------
+    // Basic linear BMC based on indexed variables using quantified bit-vector domains.
+
+    lbool bmc::check_qlinear() {
+        setup_qlinear();
+        m_bit_width = 4;
+        lbool res = l_false;
+        while (res == l_false) {
+            m_solver.push();
+            IF_VERBOSE(1, verbose_stream() << "bit_width: " << m_bit_width << "\n";);
+            compile_qlinear();
+            checkpoint();
+            func_decl_ref q = mk_q_func_decl(m_query_pred);
+            expr* T = m.mk_const(symbol("T"), mk_index_sort());
+            expr_ref fml(m.mk_app(q, T), m);
+            assert_expr(fml);
+            res = m_solver.check();
+
+            if (res == l_true) {
+                res = get_model_qlinear();                
+            }
+            m_solver.pop(1);           
+            ++m_bit_width;
+        }
+        return res;
+    }
+
+    sort_ref bmc::mk_index_sort() {
+        return sort_ref(m_bv.mk_sort(m_bit_width), m);
+    }
+
+    var_ref bmc::mk_index_var() {
+        return var_ref(m.mk_var(0, mk_index_sort()), m);
+    }
+
+    void bmc::compile_qlinear() {
+        sort_ref index_sort = mk_index_sort();
+        var_ref var = mk_index_var();
+        sort* index_sorts[1] = { index_sort };
+        symbol tick("T");
+        rule_set::decl2rules::iterator it  = m_rules.begin_grouped_rules();
+        rule_set::decl2rules::iterator end = m_rules.end_grouped_rules();
+        for (; it != end; ++it) {
+            func_decl* p = it->m_key;
+            rule_vector const& rls = *it->m_value;
+            // Assert: forall level . p(T) => body of rule i + equalities for head of rule i
+            func_decl_ref pr = mk_q_func_decl(p);
+            expr_ref pred = expr_ref(m.mk_app(pr, var.get()), m);
+            expr_ref_vector rules(m), sub(m), conjs(m);  
+            expr_ref trm(m), rule_body(m), rule_i(m);
+            for (unsigned i = 0; i < rls.size(); ++i) {       
+                sub.reset(); 
+                conjs.reset();
+                rule& r = *rls[i];                
+                rule_i = m.mk_app(mk_q_rule(p, i), var.get());
+                rules.push_back(rule_i);
+
+                mk_qrule_vars(r, i, sub);
+
+                // apply substitution to body.
+                var_subst vs(m, false);
+                for (unsigned k = 0; k < p->get_arity(); ++k) {
+                    vs(r.get_head()->get_arg(k), sub.size(), sub.c_ptr(), trm);
+                    conjs.push_back(m.mk_eq(trm, mk_q_arg(p, k, true)));
+                }
+                for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
+                    func_decl* q = r.get_decl(j);
+                    for (unsigned k = 0; k < q->get_arity(); ++k) {
+                        vs(r.get_tail(j)->get_arg(k), sub.size(), sub.c_ptr(), trm);
+                        conjs.push_back(m.mk_eq(trm, mk_q_arg(q, k, false)));
+                    }
+                    func_decl_ref qr = mk_q_func_decl(q);
+                    conjs.push_back(m.mk_app(qr, m_bv.mk_bv_sub(var, mk_q_one())));
+                }
+                for (unsigned j = r.get_uninterpreted_tail_size(); j < r.get_tail_size(); ++j) {
+                    vs(r.get_tail(j), sub.size(), sub.c_ptr(), trm);
+                    conjs.push_back(trm);
+                }
+                if (r.get_uninterpreted_tail_size() > 0) {
+                    conjs.push_back(m_bv.mk_ule(mk_q_one(), var));
+                }
+                bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), rule_body);
+                trm = m.mk_implies(rule_i, rule_body);
+                trm = m.mk_forall(1, index_sorts, &tick, trm, 1);
+                assert_expr(trm);
+            }
+            bool_rewriter(m).mk_or(rules.size(), rules.c_ptr(), trm);
+            trm = m.mk_implies(pred, trm);
+            trm = m.mk_forall(1, index_sorts, &tick, trm, 1);
+            SASSERT(is_well_sorted(m, trm));
+            assert_expr(trm);
+        }
+    }
+
+    void bmc::setup_qlinear() {
+        m_fparams.m_relevancy_lvl = 2;
+        m_fparams.m_model = true;
+        m_fparams.m_model_compact = true;
+        m_fparams.m_mbqi = true;
+    }
+
+    void bmc::mk_qrule_vars(datalog::rule const& r, unsigned rule_id, expr_ref_vector& sub) {
+        sort_ref_vector sorts(m);
+        r.get_vars(sorts);
+        // populate substitution of bound variables.
+        sub.reset();
+        sub.resize(sorts.size());
+
+        for (unsigned k = 0; k < r.get_decl()->get_arity(); ++k) {
+            expr* arg = r.get_head()->get_arg(k);
+            if (is_var(arg)) {
+                unsigned idx = to_var(arg)->get_idx();
+                if (!sub[idx].get()) {
+                    sub[idx] = mk_q_arg(r.get_decl(), k, true);
+                }
+            }
+        }
+        for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
+            func_decl* q = r.get_decl(j);
+            for (unsigned k = 0; k < q->get_arity(); ++k) {
+                expr* arg = r.get_tail(j)->get_arg(k);
+                if (is_var(arg)) {
+                    unsigned idx = to_var(arg)->get_idx();
+                    if (!sub[idx].get()) {
+                        sub[idx] = mk_q_arg(q, k, false);
+                    }
+                }
+            }
+        }
+        for (unsigned j = 0, idx = 0; j < sorts.size(); ++j) {
+            if (sorts[j].get() && !sub[j].get()) {
+                sub[j] = mk_q_var(r.get_decl(), sorts[j].get(), rule_id, idx++);
+            }
+        }        
+    }
+
+    expr_ref bmc::mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx) {
+        std::stringstream _name;
+        _name << pred->get_name() << "#" <<  rule_id << "_" << idx;
+        symbol nm(_name.str().c_str());        
+        var_ref var = mk_index_var();
+        return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), s), var), m);
+    }    
+
+    expr_ref bmc::mk_q_arg(func_decl* pred, unsigned idx, bool is_current) {
+        SASSERT(idx < pred->get_arity());
+        std::stringstream _name;
+        _name << pred->get_name() << "#" << idx;
+        symbol nm(_name.str().c_str());        
+        expr_ref var(mk_index_var(), m);
+        if (!is_current) {
+            var = m_bv.mk_bv_sub(var, mk_q_one());
+        }
+        return expr_ref(m.mk_app(m.mk_func_decl(nm, mk_index_sort(), pred->get_domain(idx)), var), m);
+    }
+
+    expr_ref bmc::mk_q_one() {
+        return mk_q_num(1);
+    }
+
+    expr_ref bmc::mk_q_num(unsigned i) {
+        return expr_ref(m_bv.mk_numeral(i, m_bit_width), m);
+    }
+
+    func_decl_ref bmc::mk_q_func_decl(func_decl* f) {
+        std::stringstream _name;
+        _name << f->get_name() << "#";
+        symbol nm(_name.str().c_str());    
+        return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), f->get_range()), m);
+    }
+
+    func_decl_ref bmc::mk_q_rule(func_decl* f, unsigned rule_id) {
+        std::stringstream _name;
+        _name << f->get_name() << "#" << rule_id;
+        symbol nm(_name.str().c_str());    
+        return func_decl_ref(m.mk_func_decl(nm, mk_index_sort(), m.mk_bool_sort()), m);
+    }
+
+
+    expr_ref bmc::eval_q(model_ref& model, func_decl* f, unsigned i) {
+        func_decl_ref fn = mk_q_func_decl(f);
+        expr_ref t(m), result(m);
+        t = m.mk_app(mk_q_func_decl(f), mk_q_num(i));
+        model->eval(t, result);
+        return result;
+    }
+
+    expr_ref bmc::eval_q(model_ref& model, expr* t, unsigned i) {
+        expr_ref tmp(m), result(m), num(m);
+        var_subst vs(m, false);
+        num = mk_q_num(i);
+        expr* nums[1] = { num };
+        vs(t, 1, nums, tmp);
+        model->eval(tmp, result);
+        return result;
+    }    
+
+    lbool bmc::get_model_qlinear() {
+        rule_manager& rm = m_ctx.get_rule_manager();
+        func_decl_ref q = mk_q_func_decl(m_query_pred);
+        expr_ref T(m), rule_i(m), vl(m);
+        model_ref md;
+        proof_ref pr(m);
+        rule_unifier unifier(m_ctx);
+        rational num;
+        unsigned level, bv_size;
+
+        m_solver.get_model(md);
+        func_decl* pred = m_query_pred;
+        dl_decl_util util(m);
+        T = m.mk_const(symbol("T"), mk_index_sort());
+        md->eval(T, vl);
+        VERIFY (m_bv.is_numeral(vl, num, bv_size));
+        SASSERT(num.is_unsigned());
+        level = num.get_unsigned();
+        SASSERT(m.is_true(eval_q(md, m_query_pred, level)));
+        TRACE("bmc", model_smt2_pp(tout, m, *md, 0););
+        
+        rule_ref r0(rm), r1(rm), r2(rm);
+        while (true) {
+            TRACE("bmc", tout << "Predicate: " << pred->get_name() << "\n";);
+            expr_ref_vector sub(m);
+            rule_vector const& rls = m_rules.get_predicate_rules(pred);
+            rule* r = 0;
+            unsigned i = 0;
+            for (; i < rls.size(); ++i) {       
+                rule_i = m.mk_app(mk_q_rule(pred, i), mk_q_num(level));         
+                TRACE("bmc", rls[i]->display(m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " "););
+                if (m.is_true(eval_q(md, rule_i, level))) {
+                    r = rls[i];
+                    break;
+                }
+            }
+            SASSERT(r);
+            mk_qrule_vars(*r, i, sub);
+            // we have rule, we have variable names of rule.
+            
+            // extract values for the variables in the rule.
+            for (unsigned j = 0; j < sub.size(); ++j) {
+                expr_ref vl = eval_q(md, sub[j].get(), i);
+                if (vl) {
+                    // vl can be 0 if the interpretation does not assign a value to it.
+                    sub[j] = vl;   
+                }
+                else {
+                    sub[j] = m.mk_var(j, m.get_sort(sub[j].get()));
+                }
+            }
+            svector<std::pair<unsigned, unsigned> > positions;
+            vector<expr_ref_vector> substs;
+            expr_ref fml(m), concl(m);
+            
+            r->to_formula(fml);
+            r2 = r;
+            rm.substitute(r2, sub.size(), sub.c_ptr());
+            if (r0) {
+                VERIFY(unifier.unify_rules(*r0.get(), 0, *r2.get()));
+                expr_ref_vector sub1 = unifier.get_rule_subst(*r0.get(), true);
+                expr_ref_vector sub2 = unifier.get_rule_subst(*r2.get(), false);
+                apply_subst(sub, sub2);
+                unifier.apply(*r0.get(), 0, *r2.get(), r1);
+                r1->to_formula(concl);
+                scoped_coarse_proof _sp(m);
+                
+                proof* p = m.mk_asserted(fml);
+                proof* premises[2] = { pr, p };
+                
+                positions.push_back(std::make_pair(0, 1));
+                
+                substs.push_back(sub1);
+                substs.push_back(sub);
+                pr = m.mk_hyper_resolve(2, premises, concl, positions, substs);
+                r0 = r1;
+            }
+            else {
+                r2->to_formula(concl);
+                scoped_coarse_proof _sp(m);
+                proof* p = m.mk_asserted(fml);
+                if (sub.empty()) {
+                    pr = p;
+                }
+                else {
+                    substs.push_back(sub);
+                    pr = m.mk_hyper_resolve(1, &p, concl, positions, substs);
+                }
+                r0 = r2;
+            }
+            
+            if (level == 0) {
+                SASSERT(r->get_uninterpreted_tail_size() == 0);
+                break;
+            }
+            --level;
+            SASSERT(r->get_uninterpreted_tail_size() == 1);
+            pred = r->get_decl(0);
+        }
+        scoped_coarse_proof _sp(m);
+        apply(m, m_pc.get(), pr);
+        m_answer = pr;
+        return l_true;
+    }
+
+    // --------------------------------------------------------------------------
+    // Basic non-linear BMC based on compiling into data-types (it is inefficient)
+
 
     lbool bmc::check_nonlinear() {
-        m_fparams.m_relevancy_lvl = 2;
+        setup_nonlinear();
         declare_datatypes();
         compile_nonlinear();        
         return check_query();      
     }
 
+    void bmc::setup_nonlinear() {
+        setup_linear();
+        m_fparams.m_relevancy_lvl = 2;
+    }
+
     func_decl_ref bmc::mk_predicate(func_decl* pred) {
         std::stringstream _name;
         _name << pred->get_name() << "#";
@@ -597,7 +920,7 @@ namespace datalog {
             m_pinned.push_back(new_sorts[i].get());            
         }
         if (new_sorts.size() > 0) {
-            TRACE("dl", dtu.display_datatype(new_sorts[0].get(), tout););
+            TRACE("bmc", dtu.display_datatype(new_sorts[0].get(), tout););
         }
         del_datatype_decls(dts.size(), dts.c_ptr());
 
@@ -700,10 +1023,11 @@ namespace datalog {
     lbool bmc::check_query() {
         sort* trace_sort = m_pred2sort.find(m_query_pred);
         func_decl_ref q = mk_predicate(m_query_pred);
-        expr_ref trace(m), path(m);
+        expr_ref trace(m), path(m), fml(m);
         trace = m.mk_const(symbol("trace"), trace_sort);
         path  = m.mk_const(symbol("path"), m_path_sort);
-        assert_expr(m.mk_app(q, trace.get(), path.get()));
+        fml = m.mk_app(q, trace.get(), path.get());
+        assert_expr(fml);
         while (true) {
             lbool is_sat = m_solver.check();
             model_ref md;
@@ -729,7 +1053,8 @@ namespace datalog {
         m_solver.pop(1);
         if (is_sat == l_false) {
             IF_VERBOSE(1, verbose_stream() << "infeasible trace " << mk_pp(trace_val, m) << "\n";);
-            m_solver.assert_expr(m.mk_not(eq));
+            eq = m.mk_not(eq);
+            m_solver.assert_expr(eq);
         }
         return is_sat != l_false;       
     }
@@ -771,6 +1096,9 @@ namespace datalog {
         m_solver.collect_statistics(st);
     }
 
+    void bmc::collect_params(param_descrs& p) {
+    }
+
     expr_ref bmc::get_answer() {        
         return m_answer;
     }
diff --git a/lib/dl_bmc_engine.h b/lib/dl_bmc_engine.h
index d641643dc..e0e8ff3da 100644
--- a/lib/dl_bmc_engine.h
+++ b/lib/dl_bmc_engine.h
@@ -23,6 +23,7 @@ Revision History:
 #include "params.h"
 #include "statistics.h"
 #include "smt_solver.h"
+#include "bv_decl_plugin.h"
 
 
 namespace datalog {
@@ -44,6 +45,8 @@ namespace datalog {
         volatile bool    m_cancel;
         proof_converter_ref m_pc;
         sort_ref         m_path_sort;
+        bv_util          m_bv;
+        unsigned         m_bit_width;
 
         lbool check_query();
 
@@ -66,9 +69,8 @@ namespace datalog {
         bool is_linear() const;
 
         lbool check_nonlinear();
-
+        void  setup_nonlinear();
         bool check_model_nonlinear(model_ref& md, expr* trace);
-
         void mk_answer_nonlinear(model_ref& md, expr_ref& trace, expr_ref& path);
         
         func_decl_ref mk_predicate(func_decl* p);
@@ -77,31 +79,39 @@ namespace datalog {
 
         // linear check
         lbool check_linear();
-
         lbool check_linear(unsigned level);
-
         void compile_linear();
-
         void compile_linear(unsigned level);
-
         void compile_linear(rule& r, unsigned level);
-
         expr_ref mk_level_predicate(symbol const& name, unsigned level);
-
         expr_ref mk_level_predicate(func_decl* p, unsigned level);
-
         expr_ref mk_level_arg(func_decl* pred, unsigned idx, unsigned level);
-
         expr_ref mk_level_rule(func_decl* p, unsigned rule_idx, unsigned level);
-
-         expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
-
+        expr_ref mk_level_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx, unsigned level);
         void get_model_linear(unsigned level);
+        void setup_linear();
 
         void assert_expr(expr* e);
 
         void mk_rule_vars(rule& r, unsigned level, unsigned rule_id, expr_ref_vector& sub);
 
+        // quantified linear check
+        void  compile_qlinear();
+        void  setup_qlinear();
+        lbool check_qlinear();
+        lbool get_model_qlinear();
+        sort_ref mk_index_sort();
+        var_ref mk_index_var();
+        void mk_qrule_vars(datalog::rule const& r, unsigned i, expr_ref_vector& sub);
+        expr_ref mk_q_var(func_decl* pred, sort* s, unsigned rule_id, unsigned idx);
+        expr_ref mk_q_arg(func_decl* pred, unsigned idx, bool is_current);
+        expr_ref mk_q_one();
+        expr_ref mk_q_num(unsigned i);
+        expr_ref eval_q(model_ref& model, expr* t, unsigned i);
+        expr_ref eval_q(model_ref& model, func_decl* f, unsigned i);
+        func_decl_ref mk_q_rule(func_decl* f, unsigned rule_id);
+        func_decl_ref mk_q_func_decl(func_decl* f);
+
     public:
         bmc(context& ctx);
 
@@ -119,7 +129,7 @@ namespace datalog {
 
         expr_ref get_answer();
 
-        
+        static void collect_params(param_descrs& p);
     };
 };
 
diff --git a/lib/dl_context.cpp b/lib/dl_context.cpp
index b64bf3925..96a7ecb29 100644
--- a/lib/dl_context.cpp
+++ b/lib/dl_context.cpp
@@ -589,6 +589,7 @@ namespace datalog {
             ensure_pdr();
             return m_pdr->get_num_levels(pred);
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             throw default_exception("get_num_levels is unsupported for bmc");
         default:
             throw default_exception("unknown engine");
@@ -604,6 +605,7 @@ namespace datalog {
             ensure_pdr();
             return m_pdr->get_cover_delta(level, pred);
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             throw default_exception("operation is unsupported for BMC engine");
         default:
             throw default_exception("unknown engine");
@@ -620,6 +622,7 @@ namespace datalog {
             m_pdr->add_cover(level, pred, property);
             break;
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             throw default_exception("operation is unsupported for BMC engine");
         default:
             throw default_exception("unknown engine");
@@ -751,6 +754,7 @@ namespace datalog {
             check_positive_predicates(r);
             break;
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             check_existential_tail(r);
             check_positive_predicates(r);
             break;            
@@ -969,12 +973,14 @@ namespace datalog {
         PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion"););
 
         pdr::dl_interface::collect_params(p);
+        bmc::collect_params(p);
         insert_timeout(p);
     }
 
     void context::updt_params(params_ref const& p) {
         m_params.copy(p);
         if (m_pdr.get()) m_pdr->updt_params();
+        
     }
 
     void context::collect_predicates(decl_set & res) {
@@ -1109,11 +1115,13 @@ namespace datalog {
     void context::cancel() {
         m_cancel = true;
         if (m_pdr.get()) m_pdr->cancel();
+        if (m_bmc.get()) m_bmc->cancel();
     }
 
     void context::cleanup() {
         m_cancel = false;
         if (m_pdr.get()) m_pdr->cleanup();
+        if (m_bmc.get()) m_bmc->cleanup();
     }
 
     class context::engine_type_proc {
@@ -1157,6 +1165,9 @@ namespace datalog {
         else if (e == symbol("bmc")) {
             m_engine = BMC_ENGINE;
         }
+        else if (e == symbol("qbmc")) {
+            m_engine = QBMC_ENGINE;
+        }
 
         if (m_engine == LAST_ENGINE) {
             expr_fast_mark1 mark;
@@ -1190,6 +1201,7 @@ namespace datalog {
         case QPDR_ENGINE:
             return pdr_query(query);
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             return bmc_query(query);
         default:
             UNREACHABLE();
@@ -1450,6 +1462,7 @@ namespace datalog {
             m_last_answer = m_pdr->get_answer();
             return m_last_answer.get();
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             ensure_bmc();
             m_last_answer = m_bmc->get_answer();
             return m_last_answer.get();
@@ -1471,6 +1484,7 @@ namespace datalog {
             m_pdr->display_certificate(out);
             return true;
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             m_bmc->display_certificate(out);
             return true;
         default: 
@@ -1490,6 +1504,7 @@ namespace datalog {
             m_pdr->collect_statistics(st);
             break;
         case BMC_ENGINE:
+        case QBMC_ENGINE:
             m_bmc->collect_statistics(st);
             break;
         default: 
diff --git a/lib/dl_util.h b/lib/dl_util.h
index 1969da1a9..1685bec9c 100644
--- a/lib/dl_util.h
+++ b/lib/dl_util.h
@@ -50,6 +50,7 @@ namespace datalog {
         PDR_ENGINE,
         QPDR_ENGINE,
         BMC_ENGINE,
+        QBMC_ENGINE,
         LAST_ENGINE
     };
 
diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp
index b9ae51859..9d82ce149 100644
--- a/lib/pdr_context.cpp
+++ b/lib/pdr_context.cpp
@@ -278,7 +278,10 @@ namespace pdr {
                    if (is_infty_level(src_level)) {
                        verbose_stream() << "infty"; 
                    }
-                   else verbose_stream() << src_level;
+                   else {
+                       verbose_stream() << src_level;
+                   }
+                   verbose_stream() << "\n";
                    for (unsigned i = 0; i < src.size(); ++i) {
                        verbose_stream() << mk_pp(src[i].get(), m) << "\n";   
                    });
@@ -831,7 +834,11 @@ namespace pdr {
 
     void model_search::set_leaf(model_node& n) {
         erase_children(n);
-        SASSERT(n.is_open());        
+        SASSERT(n.is_open());      
+        enqueue_leaf(n);
+    }
+
+    void model_search::enqueue_leaf(model_node& n) {
         if (m_bfs) {
             m_leaves.push_front(&n);
         }
@@ -1047,7 +1054,7 @@ namespace pdr {
         if (uses_level && m_root->level() > n.level()) {
             IF_VERBOSE(2, verbose_stream() << "Increase level " << n.level() << "\n";);
             n.increase_level();
-            m_leaves.push_back(&n);
+            enqueue_leaf(n);
         }
         else {
             model_node* p = n.parent();
@@ -1076,8 +1083,7 @@ namespace pdr {
           m_search(m_params.get_bool(":bfs-model-search", true)),
           m_last_result(l_undef),
           m_inductive_lvl(0),
-          m_cancel(false),
-          m_is_dl(false)
+          m_cancel(false)
     {
     }
 
@@ -1296,7 +1302,6 @@ namespace pdr {
     void context::init_core_generalizers(datalog::rule_set& rules) {
         reset_core_generalizers();
         classifier_proc classify(m, rules);
-        m_is_dl = false;
         bool use_mc = m_params.get_bool(":use-multicore-generalizer", false);
         if (use_mc) {
             m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
@@ -1312,7 +1317,6 @@ namespace pdr {
                 if (classify.is_dl()) {
                     m_fparams.m_arith_mode = AS_DIFF_LOGIC;
                     m_fparams.m_arith_expand_eqs = true;
-                    m_is_dl = true;
                 }
             }
             else {
@@ -1654,7 +1658,6 @@ namespace pdr {
     void context::create_children(model_node& n) {        
         SASSERT(n.level() > 0);
         bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
-        // use_model_generalizer = use_model_generalizer || is_dl();
  
         pred_transformer& pt = n.pt();
         model_ref M = n.model_ptr();
@@ -1693,12 +1696,14 @@ namespace pdr {
         pt.get_aux_vars(r, aux_vars);
         vars.append(aux_vars.size(), aux_vars.c_ptr());
 
+        scoped_ptr<expr_replacer> rep;
         qe_lite qe(m);
         expr_ref phi1 = m_pm.mk_and(Phi);
         qe(vars, phi1);
         if (!use_model_generalizer) {
             reduce_disequalities(*M, 3, phi1);
         }
+        get_context().get_rewriter()(phi1);
 
         IF_VERBOSE(2, 
                    verbose_stream() << "Vars:\n";
@@ -1720,7 +1725,7 @@ namespace pdr {
                 M->eval(vars[i]->get_decl(), tmp);                
                 sub.insert(vars[i].get(), tmp, pr);
             }
-            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+            if (!rep) rep = mk_expr_simp_replacer(m);
             rep->set_substitution(&sub);
             (*rep)(phi1);
             IF_VERBOSE(2, verbose_stream() << "Projected:\n" << mk_pp(phi1, m) << "\n";);
@@ -1733,7 +1738,7 @@ namespace pdr {
         for (unsigned i = 0; i < Phi.size(); ++i) {            
             m_pm.collect_indices(Phi[i].get(), indices);    
             if (indices.size() == 0) {
-                IF_VERBOSE(2, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";);
+                IF_VERBOSE(3, verbose_stream() << "Skipping " << mk_pp(Phi[i].get(), m) << "\n";);
             }
             else if (indices.size() == 1) {
                 child_states[indices.back()].push_back(Phi[i].get());
@@ -1755,11 +1760,12 @@ namespace pdr {
                     }
                 }
                 tmp = Phi[i].get();
-                scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+                if (!rep) rep = mk_expr_simp_replacer(m);
                 rep->set_substitution(&sub);
                 (*rep)(tmp);
                 child_states[indices[0]].push_back(tmp);
             }
+
         }
         
         expr_ref n_cube(m);
@@ -1774,8 +1780,6 @@ namespace pdr {
             IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
         }
         check_pre_closed(n);
-
-
         TRACE("pdr", m_search.display(tout););
     }
 
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index fe8bc8e90..2a4e91c3e 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -231,31 +231,22 @@ namespace pdr {
         void erase_children(model_node& n);
         void erase_leaf(model_node& n);
         void remove_node(model_node& n);
+        void enqueue_leaf(model_node& n); // add leaf to priority queue.
     public:
         model_search(bool bfs): m_bfs(bfs), m_root(0) {}
-
         ~model_search();
 
         void reset();
-
         model_node* next();
-
         bool is_repeated(model_node& n) const;
-
         void add_leaf(model_node& n); // add fresh node.
-
         void set_leaf(model_node& n); // Set node as leaf, remove children.
 
         void set_root(model_node* n);
-
         model_node& get_root() const { return *m_root; }
-
         std::ostream& display(std::ostream& out) const; 
-
         expr_ref get_trace() const;
-
         proof_ref get_proof_trace(context const& ctx) const;
-
         void backtrack_level(bool uses_level, model_node& n);
     };
 
@@ -308,7 +299,6 @@ namespace pdr {
         volatile bool        m_cancel;
         model_converter_ref  m_mc;
         proof_converter_ref  m_pc;
-        bool                 m_is_dl;
         
         // Functions used by search.
         void solve_impl();
@@ -366,7 +356,7 @@ namespace pdr {
         datalog::context& get_context() const { SASSERT(m_context); return *m_context; }
         expr_ref          get_answer();
 
-        bool              is_dl() const { return m_is_dl; }
+        bool              is_dl() const { return m_fparams.m_arith_mode == AS_DIFF_LOGIC; }
 
 
         void collect_statistics(statistics& st) const;