From 832ade3ac8ac89f77c1107df414d33b9154f8a5e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Oct 2012 10:37:05 -0700
Subject: [PATCH 1/2] local changes

---
 src/muz_qe/pdr_context.cpp      | 41 +++++++++++++++++++++++++++++++++
 src/muz_qe/pdr_context.h        |  2 ++
 src/muz_qe/pdr_dl_interface.cpp |  1 +
 3 files changed, 44 insertions(+)

diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index b89e7852f..7d7438f7b 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1297,6 +1297,45 @@ namespace pdr {
         }
     };
 
+    void context::validate() {
+        if (!m_params.get_bool(":validate-result", false)) {
+            return;
+        }
+        switch(m_last_result) {
+        case l_true: {
+            proof_ref pr = get_proof();
+            proof_checker checker(m);
+            expr_ref_vector side_conditions(m);
+            bool ok = check(pr, side_conditions);
+            if (!ok) {
+                IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
+            }
+            break;
+        }            
+        case l_false: {
+            expr_ref_vector refs(m);
+            model_ref model;
+            vector<relation_info> rs;
+            get_level_property(m_inductive_lvl, refs, rs);    
+            inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
+            ex.to_model(model);
+            decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+            var_subst vs(m, false);
+            for (; it != end; ++it) {
+                ptr_vector<datalog::rule> const& rules = it->m_value->rules();
+                for (unsigned i = 0; i < rules.size(); ++i) {
+                    datalog::rule* rule = rules[i];
+                    // vs(rule->get_head(), 
+                    // apply interpretation of predicates to rule.
+                    // create formula and check for unsat.
+                }
+            }
+            break;
+        }
+        default:
+            break;
+        }
+    }
 
     void context::reset_core_generalizers() {
         std::for_each(m_core_generalizers.begin(), m_core_generalizers.end(), delete_proc<core_generalizer>());
@@ -1371,6 +1410,7 @@ namespace pdr {
             check_quantifiers();
             IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream()););  
             m_last_result = l_true;
+            validate();
             return l_true;
         }
         catch (inductive_exception) {
@@ -1378,6 +1418,7 @@ namespace pdr {
             m_last_result = l_false;
             TRACE("pdr",  display_certificate(tout););      
             IF_VERBOSE(1, display_certificate(verbose_stream()););
+            validate();
             return l_false;
         }
         catch (unknown_exception) {
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 5e7f08b85..71b59ac26 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -333,6 +333,8 @@ namespace pdr {
 
         void reset_core_generalizers();
 
+        void validate();
+
     public:       
         
         /**
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index e336d314b..69f0995f0 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -206,6 +206,7 @@ void dl_interface::collect_params(param_descrs& p) {
     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)");
     PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););
     PRIVATE_PARAMS(p.insert(":use-inductive-generalizer", CPK_BOOL, "PDR: (default true) generalize lemmas using induction strengthening"););
     PRIVATE_PARAMS(p.insert(":use-interpolants", CPK_BOOL, "PDR: (default false) use iZ3 interpolation for lemma generation"););

From c4cb66bbfa0eb6e9e708f9d97de6ee5066b29de6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 31 Oct 2012 13:23:24 -0700
Subject: [PATCH 2/2] fix bugs in inliner and usage of unbound variable fix,
 reported by Arie Gurfinkel

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz_qe/dl_context.cpp                   |  20 +---
 src/muz_qe/dl_finite_product_relation.cpp   |   5 +-
 src/muz_qe/dl_mk_coalesce.cpp               |   3 -
 src/muz_qe/dl_mk_rule_inliner.cpp           |  42 ++++----
 src/muz_qe/dl_mk_slice.cpp                  |   4 +-
 src/muz_qe/dl_mk_subsumption_checker.cpp    |   1 +
 src/muz_qe/dl_mk_unbound_compressor.cpp     |   2 +-
 src/muz_qe/dl_rule.cpp                      | 104 ++++++++++----------
 src/muz_qe/dl_util.cpp                      |   1 -
 src/muz_qe/horn_subsume_model_converter.cpp |  10 +-
 src/muz_qe/pdr_context.cpp                  |   3 +-
 src/muz_qe/pdr_interpolant_provider.cpp     |   2 +-
 src/muz_qe/qe.cpp                           |   2 +-
 src/muz_qe/qe_lite.cpp                      |   3 +
 src/smt/theory_diff_logic_def.h             |   1 -
 src/util/diff_logic.h                       |   1 -
 16 files changed, 94 insertions(+), 110 deletions(-)

diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index ae7bc360d..dd94796a0 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -969,7 +969,8 @@ namespace datalog {
         
         p.insert(":fix-unbound-vars", CPK_BOOL, "fix unbound variables in tail");
         p.insert(":default-table-checker", CPK_SYMBOL, "see :default-table-checked");
-        p.insert(":inline-linear", CPK_BOOL, "try linear inlining method");
+        p.insert(":inline-linear", CPK_BOOL, "(default true) try linear inlining method");
+        p.insert(":inline-eager", CPK_BOOL, "(default true) try eager inlining of rules");
         PRIVATE_PARAMS(p.insert(":inline-linear-branch", CPK_BOOL, "try linear inlining method with potential expansion"););
 
         pdr::dl_interface::collect_params(p);
@@ -1551,23 +1552,6 @@ namespace datalog {
         }
     }
     
-#if 0
-    // [Leo] dead code?
-    static func_decl* get_head_relation(ast_manager& m, expr* fml) {
-        while (is_quantifier(fml)) {
-            fml = to_quantifier(fml)->get_expr();            
-        }
-        expr* f1;
-        while (m.is_implies(fml, f1, fml)) {};
-        if (is_app(fml)) {
-            return to_app(fml)->get_decl();
-        }
-        else {
-            return 0;
-        }
-    }
-#endif
-
     void context::display_smt2(
         unsigned num_queries, 
         expr* const* queries, 
diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz_qe/dl_finite_product_relation.cpp
index 3ab3da45d..3070475ac 100644
--- a/src/muz_qe/dl_finite_product_relation.cpp
+++ b/src/muz_qe/dl_finite_product_relation.cpp
@@ -986,6 +986,7 @@ namespace datalog {
         }
     };
 
+#if 0
     /**
        Union operation taking advantage of the fact that the inner relation of all the arguments
        is a singleton relation.
@@ -1003,7 +1004,7 @@ namespace datalog {
 
         // [Leo]: gcc complained about the following class.
         // It does not have a constructor and uses a reference
-#if 0
+
         class inner_relation_copier : public table_row_mutator_fn {
             finite_product_relation & m_tgt;
             const finite_product_relation & m_src;
@@ -1026,7 +1027,6 @@ namespace datalog {
                 return true;
             }
         };
-#endif
 
         scoped_ptr<table_union_fn> m_t_union_fun;
         offset_row_mapper * m_offset_mapper_obj; //initialized together with m_offset_mapper_fun, and deallocated by it
@@ -1083,6 +1083,7 @@ namespace datalog {
             NOT_IMPLEMENTED_YET();
         }
     };
+#endif
 
     class finite_product_relation_plugin::converting_union_fn : public relation_union_fn {
         scoped_ptr<relation_union_fn> m_tr_union_fun;
diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp
index cd825b7c7..251988a84 100644
--- a/src/muz_qe/dl_mk_coalesce.cpp
+++ b/src/muz_qe/dl_mk_coalesce.cpp
@@ -179,9 +179,7 @@ namespace datalog {
         }
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
-        // bool change = false;
         for (; it != end; ++it) {
-            // func_decl* p = it->m_key;
             rule_ref_vector d_rules(rm);
             d_rules.append(it->m_value->size(), it->m_value->c_ptr());
             for (unsigned i = 0; i < d_rules.size(); ++i) {
@@ -191,7 +189,6 @@ namespace datalog {
                         merge_rules(r1, *d_rules[j].get());
                         d_rules[j] = d_rules.back();
                         d_rules.pop_back();
-                        // change = true;
                         --j;
                     }
                 }
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index c6908292a..b7e31a75d 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -17,6 +17,7 @@ Revision History:
 
     Added linear_inline 2012-9-10 (nbjorner)
 
+    Disable inliner for quantified rules 2012-10-31 (nbjorner)
     
 Notes:
 
@@ -118,9 +119,7 @@ namespace datalog {
         res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
         res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
         res->norm_vars(m_rm);
-        if (m_context.fix_unbound_vars()) {
-            m_rm.fix_unbound_vars(res, true);
-        }
+        m_rm.fix_unbound_vars(res, true);        
         if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
             res = simpl_rule;
             return true;
@@ -164,9 +163,7 @@ namespace datalog {
 
         tgt.norm_vars(m_context.get_rule_manager());
 
-        if (has_quantifier(src)) {
-            return false;
-        }
+        SASSERT(!has_quantifier(src));
 
         if (!m_unifier.unify_rules(tgt, tail_index, src)) {
             return false;
@@ -433,9 +430,7 @@ namespace datalog {
 
             for  (; i < pt_len && !inlining_allowed(r->get_decl(i)); ++i) {};
 
-            if (has_quantifier(*r.get())) {
-                continue;
-            }
+            SASSERT(!has_quantifier(*r.get()));
 
             if (i == pt_len) {
                 //there's nothing we can inline in this rule
@@ -842,11 +837,20 @@ namespace datalog {
         bool something_done = false;
         ref<horn_subsume_model_converter> hsmc;        
         ref<replace_proof_converter> hpc;
+        params_ref const& params = m_context.get_params();
 
         if (source.get_num_rules() == 0) {
             return 0;
         }
 
+        rule_set::iterator end = source.end();
+        for (rule_set::iterator it = source.begin(); it != end; ++ it) {
+            if (has_quantifier(**it)) {
+                return 0;
+            }
+        }
+        
+
         if (mc) {
             hsmc = alloc(horn_subsume_model_converter, m);
         }
@@ -858,18 +862,18 @@ namespace datalog {
 
         scoped_ptr<rule_set> res = alloc(rule_set, m_context);
 
-        plan_inlining(source);
-
-        something_done = transform_rules(source, *res);
-
-        VERIFY(res->close()); //this transformation doesn't break the negation stratification
-
-        // try eager inlining
-        if (do_eager_inlining(res)) {
-            something_done = true;
+        if (params.get_bool(":inline-eager", true)) {
+            TRACE("dl", source.display(tout << "before eager inlining\n"););
+            plan_inlining(source);            
+            something_done = transform_rules(source, *res);            
+            VERIFY(res->close()); //this transformation doesn't break the negation stratification
+            // try eager inlining
+            if (do_eager_inlining(res)) {
+                something_done = true;
+            }
+            TRACE("dl", res->display(tout << "after eager inlining\n"););
         }
 
-        params_ref const& params = m_context.get_params();
         if (params.get_bool(":inline-linear", true) && inline_linear(res)) {
             something_done = true;
         }
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index cfe168629..4edfb5b65 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -206,7 +206,7 @@ namespace datalog {
             TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";);
             rule* orig0    = m_sliceform2rule.find(fact0);
             /* rule* slice0   = */ m_rule2slice.find(orig0);
-            /* unsigned_vector const& renaming0 = */ m_renaming.find(orig0);
+            /* unsigned_vector const& renaming0 = m_renaming.find(orig0); */
             premises.push_back(p0_new);
             rule_ref r1(rm), r2(rm), r3(rm);
             r1 = orig0;
@@ -218,7 +218,7 @@ namespace datalog {
                 TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";);
                 rule* orig1     = m_sliceform2rule.find(fact1);
                 /* rule* slice1    = */ m_rule2slice.find(orig1);
-                /* unsigned_vector const& renaming1 = */ m_renaming.find(orig1); //TBD
+                /* unsigned_vector const& renaming1 =  m_renaming.find(orig1); TBD */
                 premises.push_back(p1_new);
 
                 // TODO: work with substitutions.
diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp
index 31d569796..d20ad5055 100644
--- a/src/muz_qe/dl_mk_subsumption_checker.cpp
+++ b/src/muz_qe/dl_mk_subsumption_checker.cpp
@@ -166,6 +166,7 @@ namespace datalog {
         res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
         res->set_accounting_parent_object(m_context, r);
         m_context.get_rule_manager().fix_unbound_vars(res, true);
+        
         return true;
     }
 
diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp
index 6f15260ea..000a70b22 100644
--- a/src/muz_qe/dl_mk_unbound_compressor.cpp
+++ b/src/muz_qe/dl_mk_unbound_compressor.cpp
@@ -229,7 +229,7 @@ namespace datalog {
 
         res = m_context.get_rule_manager().mk( r->get_head(), tails.size(), tails.c_ptr(), tails_negated.c_ptr());
         res->set_accounting_parent_object(m_context, r);
-        m_context.get_rule_manager().fix_unbound_vars(res, true);
+        m_context.get_rule_manager().fix_unbound_vars(res, true);        
     }
 
     void mk_unbound_compressor::add_decompression_rule(rule * r, unsigned tail_index, unsigned arg_index) {
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index 30624c90c..34868c7e5 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -11,10 +11,14 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2010-05-17.
+    Krystof Hoder (t-khoder) 2011-10-19.
 
 Revision History:
 
+    Nikolaj Bjorner (nbjorner) 2012-10-31.
+      Check for enabledness of fix_unbound_vars inside call.
+      This function gets called from many rule tansformers.
+
 --*/
 
 #include<algorithm>
@@ -36,6 +40,7 @@ Revision History:
 #include"used_symbols.h"
 #include"quant_hoist.h"
 #include"expr_replacer.h"
+#include"bool_rewriter.h"
 
 namespace datalog {
 
@@ -59,7 +64,7 @@ namespace datalog {
         if (r) {
             SASSERT(r->m_ref_cnt>0);
             r->m_ref_cnt--;
-            if(r->m_ref_cnt==0) {
+            if (r->m_ref_cnt==0) {
                 r->deallocate(m);
             }
         }
@@ -202,10 +207,10 @@ namespace datalog {
         
         if (m_ctx.fix_unbound_vars()) {
             unsigned rule_cnt = rules.size();
-            for(unsigned i=0; i<rule_cnt; ++i) {
+            for (unsigned i=0; i<rule_cnt; ++i) {
                 rule_ref r(rules[i].get(), *this);
                 fix_unbound_vars(r, true);
-                if(r.get()!=rules[i].get()) {
+                if (r.get()!=rules[i].get()) {
                     rules[i] = r;
                 }
             }
@@ -252,7 +257,7 @@ namespace datalog {
         body.push_back(to_app(q));
         flatten_body(body);
         func_decl* body_pred = 0;
-        for(unsigned i = 0; i < body.size(); i++) {
+        for (unsigned i = 0; i < body.size(); i++) {
             if (is_uninterp(body[i].get())) {
                 body_pred = body[i]->get_decl();
                 break;
@@ -269,7 +274,7 @@ namespace datalog {
         qpred = m_ctx.mk_fresh_head_predicate(symbol("query"), symbol(), vars.size(), vars.c_ptr(), body_pred);
 
         expr_ref_vector qhead_args(m);
-        for(unsigned i = 0; i < vars.size(); i++) {
+        for (unsigned i = 0; i < vars.size(); i++) {
             qhead_args.push_back(m.mk_var(vars.size()-i-1, vars[i]));
         }
         app_ref qhead(m.mk_app(qpred, qhead_args.c_ptr()), m);
@@ -539,15 +544,15 @@ namespace datalog {
             bool  is_neg = (is_negated != 0 && is_negated[i]); 
             app * curr = tail[i];
 
-            if(is_neg && !is_predicate(curr)) {
+            if (is_neg && !is_predicate(curr)) {
                 curr = m.mk_not(curr);
                 is_neg = false;
             }
-            if(is_neg) {
+            if (is_neg) {
                 has_neg = true;
             }
             app * tail_entry = TAG(app *, curr, is_neg);
-            if(is_predicate(curr)) {
+            if (is_predicate(curr)) {
                 *uninterp_tail=tail_entry;
                 uninterp_tail++;
             }
@@ -561,13 +566,13 @@ namespace datalog {
 
         r->m_uninterp_cnt = static_cast<unsigned>(uninterp_tail - r->m_tail);
 
-        if(has_neg) {
+        if (has_neg) {
             //put negative predicates between positive and interpreted
             app * * it = r->m_tail;
             app * * end = r->m_tail + r->m_uninterp_cnt;
             while(it!=end) {
                 bool  is_neg = GET_TAG(*it)!=0;
-                if(is_neg) {
+                if (is_neg) {
                     --end;
                     std::swap(*it, *end);
                 }
@@ -610,7 +615,11 @@ namespace datalog {
 
     void rule_manager::fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination) {
 
-        if(r->get_uninterpreted_tail_size()==r->get_tail_size()) {
+        if (!m_ctx.fix_unbound_vars()) {
+            return;
+        }
+
+        if (r->get_uninterpreted_tail_size() == r->get_tail_size()) {
             //no interpreted tail to fix
             return;
         }
@@ -640,17 +649,13 @@ namespace datalog {
         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();
-
             ::get_free_vars(t, interp_vars);
-            //collect_vars(m, t, interp_vars);
-
             bool has_unbound = false;
             unsigned iv_size = interp_vars.size();
-            for(unsigned i=0; i<iv_size; i++) {
-                if(!interp_vars[i]) { continue; }
-                if(vctr.get(i)==0) {
+            for (unsigned i=0; i<iv_size; i++) {
+                if (!interp_vars[i]) { continue; }
+                if (vctr.get(i)==0) {
                     has_unbound = true;
                     unbound_vars.insert(i);
                 }
@@ -670,13 +675,7 @@ namespace datalog {
             return;
         }
         expr_ref unbound_tail(m);
-        switch(tails_with_unbound.size()) {
-        case 0: unbound_tail = m.mk_true(); break;
-        case 1: unbound_tail = tails_with_unbound[0].get(); break;
-        default: 
-            unbound_tail = m.mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr());
-            break;
-        }
+        bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
 
         unsigned q_var_cnt = unbound_vars.num_elems();
         unsigned max_var = m_var_counter.get_max_var(*r);
@@ -687,15 +686,15 @@ namespace datalog {
         qsorts.resize(q_var_cnt);
 
         unsigned q_idx = 0;
-        for(unsigned v = 0; v <= max_var; ++v) {
+        for (unsigned v = 0; v <= max_var; ++v) {
             sort * v_sort = free_rule_vars[v];
-            if(!v_sort) {
+            if (!v_sort) {
                 //this variable index is not used
                 continue;
             }
 
             unsigned new_idx;
-            if(unbound_vars.contains(v)) {
+            if (unbound_vars.contains(v)) {
                 new_idx = q_idx++;
                 qsorts.push_back(v_sort);
             }
@@ -704,27 +703,24 @@ namespace datalog {
             }
             subst.push_back(m.mk_var(new_idx, v_sort));
         }
-        SASSERT(q_idx==q_var_cnt);
+        SASSERT(q_idx == q_var_cnt);
 
         svector<symbol> qnames;
-        for(unsigned i=0; i<q_var_cnt; i++) {
+        for (unsigned i = 0; i < q_var_cnt; i++) {
             qnames.push_back(symbol(i));
         }
         //quantifiers take this reversed
         qsorts.reverse();
         qnames.reverse();
 
-        expr_ref unbound_tail_pre_quant(m);
+        expr_ref unbound_tail_pre_quant(m), fixed_tail(m), quant_tail(m);
 
         var_subst vs(m, false);
         vs(unbound_tail, subst.size(), subst.c_ptr(), unbound_tail_pre_quant);
 
-        expr_ref quant_tail(m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(),
-            unbound_tail_pre_quant), m);
+        quant_tail = m.mk_exists(q_var_cnt, qsorts.c_ptr(), qnames.c_ptr(), unbound_tail_pre_quant);
 
-        expr_ref fixed_tail(m);
-
-        if(try_quantifier_elimination) {
+        if (try_quantifier_elimination) {
             TRACE("dl_rule_unbound_fix_pre_qe", 
                 tout<<"rule: ";
                 r->display(m_ctx, tout);
@@ -748,12 +744,12 @@ namespace datalog {
             tout<<"fixed tail: "<<mk_pp(fixed_tail, m)<<"\n";
         );
 
-        if(is_var(fixed_tail) || ::is_quantifier(fixed_tail)) {
+        if (is_var(fixed_tail) || ::is_quantifier(fixed_tail)) {
             fixed_tail = m.mk_eq(fixed_tail, m.mk_true());
         }
         SASSERT(is_app(fixed_tail));
 
-        if(!m.is_true(fixed_tail.get())) {
+        if (!m.is_true(fixed_tail.get())) {
             tail.push_back(to_app(fixed_tail.get()));
             tail_neg.push_back(false);
         }
@@ -829,7 +825,7 @@ namespace datalog {
     bool rule::is_in_tail(const func_decl * p, bool only_positive) const {
         unsigned len = only_positive ? get_positive_tail_size() : get_uninterpreted_tail_size();
         for (unsigned i = 0; i < len; i++) {
-            if(get_tail(i)->get_decl()==p) {
+            if (get_tail(i)->get_decl()==p) {
                 return true;
             }
         }
@@ -843,7 +839,7 @@ namespace datalog {
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
-            if(is_uninterp(n)) {
+            if (is_uninterp(n)) {
                 m_found = true;
                 m_func = n->get_decl();
             }
@@ -860,7 +856,7 @@ namespace datalog {
         unsigned sz = get_tail_size();
         uninterpreted_function_finder_proc proc;
         expr_mark visited;
-        for(unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
+        for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
             for_each_expr(proc, visited, get_tail(i));
         }
         return proc.found(f);
@@ -872,7 +868,7 @@ namespace datalog {
         quantifier_finder_proc() : m_exist(false), m_univ(false) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) {
-            if(n->is_forall()) {
+            if (n->is_forall()) {
                 m_univ = true;
             }
             else {
@@ -891,7 +887,7 @@ namespace datalog {
         unsigned sz = get_tail_size();
         quantifier_finder_proc proc;
         expr_mark visited;
-        for(unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
+        for (unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
             for_each_expr(proc, visited, get_tail(i));
         }
         existential = proc.m_exist;
@@ -934,9 +930,9 @@ namespace datalog {
 
         unsigned next_fresh_var = 0;
         expr_ref_vector subst_vals(m);
-        for(unsigned i=0; i<first_unsused; ++i) {
+        for (unsigned i=0; i<first_unsused; ++i) {
             sort* var_srt = used.contains(i);
-            if(var_srt) {
+            if (var_srt) {
                 subst_vals.push_back(m.mk_var(next_fresh_var++, var_srt));
             }
             else {
@@ -980,7 +976,7 @@ namespace datalog {
             if (is_neg_tail(i))
                 out << "not ";
             app * t = get_tail(i);
-            if(ctx.get_rule_manager().is_predicate(t)) {
+            if (ctx.get_rule_manager().is_predicate(t)) {
                 output_predicate(ctx, t, out);
             }
             else {
@@ -988,7 +984,7 @@ namespace datalog {
             }
         }
         out << '.';
-        if(ctx.output_profile()) {
+        if (ctx.output_profile()) {
             out << " {";
             output_profile(ctx, out);
             out << '}';
@@ -1050,16 +1046,16 @@ namespace datalog {
     }
 
     bool rule_eq_proc::operator()(const rule * r1, const rule * r2) const {
-        if(r1->get_head()!=r2->get_head()) { return false; }
+        if (r1->get_head()!=r2->get_head()) { return false; }
         unsigned tail_len = r1->get_tail_size();
-        if(r2->get_tail_size()!=tail_len) {
+        if (r2->get_tail_size()!=tail_len) {
             return false;
         }
-        for(unsigned i=0; i<tail_len; ++i) {
-            if(r1->get_tail(i)!=r2->get_tail(i)) {
+        for (unsigned i=0; i<tail_len; ++i) {
+            if (r1->get_tail(i)!=r2->get_tail(i)) {
                 return false;
             }
-            if(r1->is_neg_tail(i)!=r2->is_neg_tail(i)) {
+            if (r1->is_neg_tail(i)!=r2->is_neg_tail(i)) {
                 return false;
             }
         }
@@ -1069,7 +1065,7 @@ namespace datalog {
     unsigned rule::hash() const {
         unsigned res = get_head()->hash();
         unsigned tail_len = get_tail_size();
-        for(unsigned i=0; i<tail_len; ++i) {
+        for (unsigned i=0; i<tail_len; ++i) {
             res = combine_hash(res, combine_hash(get_tail(i)->hash(), is_neg_tail(i)));
         }
         return res;
diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp
index b1c5e129c..d29df7ef9 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz_qe/dl_util.cpp
@@ -594,7 +594,6 @@ namespace datalog {
 
     void del_rule(horn_subsume_model_converter* mc, rule& r) {
         if (mc) {
-            // app* head = r.get_head();
             ast_manager& m = mc->get_manager();
             expr_ref_vector body(m);
             for (unsigned i = 0; i < r.get_tail_size(); ++i) {
diff --git a/src/muz_qe/horn_subsume_model_converter.cpp b/src/muz_qe/horn_subsume_model_converter.cpp
index 2cf0f4650..048f492fe 100644
--- a/src/muz_qe/horn_subsume_model_converter.cpp
+++ b/src/muz_qe/horn_subsume_model_converter.cpp
@@ -112,7 +112,7 @@ bool horn_subsume_model_converter::mk_horn(
         m_rewrite(body_res);
         
     }
-    TRACE("dl",
+    TRACE("mc",
           tout << mk_pp(head, m) << " :- " << mk_pp(body, m) << "\n";
           tout << pred->get_name() << " :- " << mk_pp(body_res.get(), m) << "\n";);
 
@@ -155,7 +155,7 @@ void horn_subsume_model_converter::add_default_proc::operator()(app* n) {
     if (m.is_bool(n) && 
         !m_md->has_interpretation(n->get_decl()) &&
         (n->get_family_id() == null_family_id)) {
-        TRACE("dl_mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
+        TRACE("mc", tout << "adding: " << n->get_decl()->get_name() << "\n";);
         if (n->get_decl()->get_arity() == 0) {
             m_md->register_decl(n->get_decl(), m.mk_false());
         }
@@ -174,7 +174,7 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
 
 
 void horn_subsume_model_converter::operator()(model_ref& mr) {
-    TRACE("dl_mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
+    TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
     for (unsigned i = m_funcs.size(); i > 0; ) {
         --i;
         func_decl* h = m_funcs[i].get();
@@ -183,11 +183,11 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
         add_default_false_interpretation(body, mr);
         SASSERT(m.is_bool(body));
                 
-        TRACE("dl_mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
+        TRACE("mc", tout << "eval: " << h->get_name() << "\n" << mk_pp(body, m) << "\n";);
         expr_ref tmp(body);
         mr->eval(tmp, body);
         
-        TRACE("dl_mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
+        TRACE("mc", tout << "to:\n" << mk_pp(body, m) << "\n";);
                 
         if (arity == 0) {
             expr* e = mr->get_const_interp(h);
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 27e0f7e6a..3b5044b7d 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -43,6 +43,7 @@ Notes:
 #include "ast_smt2_pp.h"
 #include "qe_lite.h"
 #include "ast_ll_pp.h"
+#include "proof_checker.h"
 
 namespace pdr {
 
@@ -1306,7 +1307,7 @@ namespace pdr {
             proof_ref pr = get_proof();
             proof_checker checker(m);
             expr_ref_vector side_conditions(m);
-            bool ok = check(pr, side_conditions);
+            bool ok = checker.check(pr, side_conditions);
             if (!ok) {
                 IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
             }
diff --git a/src/muz_qe/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp
index a243ed899..85655c737 100644
--- a/src/muz_qe/pdr_interpolant_provider.cpp
+++ b/src/muz_qe/pdr_interpolant_provider.cpp
@@ -307,7 +307,7 @@ lbool interpolant_provider_impl::get_interpolant(expr * f1, expr * f2, expr_ref&
     }
 
     front_end_params dummy_params;
-    cmd_context cctx(dummy_params, false, &m);
+    cmd_context cctx(&dummy_params, false, &m);
     for_each_expr(used_symbol_inserter(cctx), f1);
 
     parse_smt2_commands(cctx, std::istringstream(res_text), false);
diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp
index 08b737609..1b92aa6e8 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/muz_qe/qe.cpp
@@ -1767,7 +1767,7 @@ namespace qe {
 
         void propagate_assignment(model_evaluator& model_eval) {
             if (m_fml) {
-                /* update_status st = */ update_current(model_eval, true);
+                update_current(model_eval, true);
             }
         }
 
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index 93a3dbfbf..ce7b85a87 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -474,6 +474,9 @@ public:
     impl(ast_manager& m): m(m), m_der(m) {}
     
     void operator()(app_ref_vector& vars, expr_ref& fml) {
+        if (vars.empty()) {
+            return;
+        }
         expr_ref tmp(fml);
         quantifier_ref q(m);
         proof_ref pr(m);     
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 2c7d32cf7..f0c491f64 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -675,7 +675,6 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
     inc_conflicts();
     literal_vector const& lits = m_nc_functor.get_lits();
     context & ctx = get_context();
-    // region& r = ctx.get_region();
     TRACE("arith_conflict", 
           //display(tout);
           tout << "conflict: ";
diff --git a/src/util/diff_logic.h b/src/util/diff_logic.h
index b4b22029f..49d7313d1 100644
--- a/src/util/diff_logic.h
+++ b/src/util/diff_logic.h
@@ -1041,7 +1041,6 @@ private:
         for (unsigned i = 0; i < edges.size(); ++i) {
             
             potential0 += m_edges[edges[i]].get_weight();
-            // numeral potential1 = potentials[i];
             if (potential0 != potentials[i] || 
                 nodes[i] != m_edges[edges[i]].get_source()) {
                 TRACE("diff_logic_traverse", tout << "checking index " << i << " ";