diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index db8189c64..ac683eca9 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -85,8 +85,6 @@ namespace datalog {
         return BR_FAILED;
     }
 
-    template class rewriter_tpl<rule_manager::remove_label_cfg>;
-
 
     void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
         expr_ref tmp(m);
@@ -1121,3 +1119,5 @@ namespace datalog {
     
 };
 
+template class rewriter_tpl<datalog::rule_manager::remove_label_cfg>;
+
diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg
index 774559cdb..c516806a6 100644
--- a/src/muz_qe/fixedpoint_params.pyg
+++ b/src/muz_qe/fixedpoint_params.pyg
@@ -60,6 +60,7 @@ def_module_params('fixedpoint',
                           ('print_answer', BOOL, False, 'print answer instance(s) to query'),
                           ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'),
                           ('print_statistics',  BOOL, False, 'print statistics'),
+			  ('use_utvpi', BOOL, False, 'experimental use UTVPI strategy'),
 	                  ('tab_selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'),
                           ))
 
diff --git a/src/muz_qe/hnf.cpp b/src/muz_qe/hnf.cpp
index 764d31bb6..bcc3501de 100644
--- a/src/muz_qe/hnf.cpp
+++ b/src/muz_qe/hnf.cpp
@@ -186,6 +186,7 @@ private:
 
 
     void mk_horn(expr_ref& fml, proof_ref& premise) {
+        SASSERT(!premise || fml == m.get_fact(premise));
         expr* e1, *e2;
         expr_ref fml0(m), fml1(m), fml2(m), head(m);
         proof_ref p(m);
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index df95b1f26..dcfbcca2b 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1441,11 +1441,7 @@ namespace pdr {
                     }         
                 }
                 m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr());
-#if 0
-                if (!m_is_dl) {
-                    m_is_utvpi = is_utvpi_logic(m, forms.size(), forms.c_ptr());
-                }
-#endif
+                m_is_utvpi = m_is_dl || is_utvpi_logic(m, forms.size(), forms.c_ptr());
             }
         }
 
@@ -1565,15 +1561,15 @@ namespace pdr {
             m_fparams.m_arith_auto_config_simplex = true;
             m_fparams.m_arith_propagate_eqs = false;
             m_fparams.m_arith_eager_eq_axioms = false;
-            if (classify.is_dl()) {
-                m_fparams.m_arith_mode = AS_DIFF_LOGIC;
-                m_fparams.m_arith_expand_eqs = true;
-            }
-            else if (classify.is_utvpi()) {
+            if (classify.is_utvpi() && m_params.use_utvpi()) {
                 IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
                 m_fparams.m_arith_mode = AS_UTVPI;
                 m_fparams.m_arith_expand_eqs = true;                
             }
+            else if (classify.is_dl()) {
+                m_fparams.m_arith_mode = AS_DIFF_LOGIC;
+                m_fparams.m_arith_expand_eqs = true;
+            }
         }
         if (!use_mc && m_params.use_inductive_generalizer()) {
             m_core_generalizers.push_back(alloc(core_bool_inductive_generalizer, *this, 0));
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index f69af93e9..e3cd0d9c5 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -391,7 +391,7 @@ namespace pdr {
              !is_utvpi_logic(m, lemmas.size(), lemmas.c_ptr()));
 
         if (outside_of_logic) {
-            IF_VERBOSE(1, 
+            IF_VERBOSE(2, 
                        verbose_stream() << "not diff\n";
                        for (unsigned i = 0; i < lemmas.size(); ++i) {
                            verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 62185f1d2..9711cffc2 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -1248,7 +1248,11 @@ namespace pdr {
             }
 
             if (!m_is_dl) {
-                IF_VERBOSE(1, verbose_stream() << "non-diff: " << mk_pp(e, m) << "\n";);
+                char const* msg = "non-diff: ";
+                if (m_test_for_utvpi) {
+                    msg = "non-utvpi: ";
+                }
+                IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
             }
         }
 
diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index b32a74c2c..f6576a41f 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -264,13 +264,6 @@ class dl_graph {
             m_assignment[e.get_target()] - m_assignment[e.get_source()] <= e.get_weight();
     }
 
-    bool is_tight(edge_id e) const {
-        edge const& edge = m_edges[e];
-        return edge.is_enabled() &&
-            m_assignment[edge.get_target()] - m_assignment[e.get_source()] == e.get_weight();
-    }
-
-
 public:
     // An assignment is feasible if all edges are feasible.
     bool is_feasible() const {
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 3bfd33b1e..7302ccfd4 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -46,7 +46,6 @@ namespace smt {
         unsigned   m_num_conflicts;
         unsigned   m_num_assertions;
         unsigned   m_num_th2core_eqs;
-        unsigned   m_num_th2core_prop;
 
         unsigned   m_num_core2th_eqs;
         unsigned   m_num_core2th_diseqs;
@@ -260,7 +259,7 @@ namespace smt {
             m_arith_eq_adapter.restart_eh();
         }
 
-        virtual void relevant_eh(app* e);
+        virtual void relevant_eh(app* e) {}
 
         virtual void init_search_eh() {
             m_arith_eq_adapter.init_search_eh();
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 362962620..20448dc74 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -310,9 +310,9 @@ void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
 template<typename Ext>
 void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
     st.update("dl conflicts", m_stats.m_num_conflicts);
-    st.update("dl propagations", m_stats.m_num_th2core_prop);
     st.update("dl asserts", m_stats.m_num_assertions);
     st.update("core->dl eqs", m_stats.m_num_core2th_eqs);
+    st.update("core->dl diseqs", m_stats.m_num_core2th_diseqs);
     m_arith_eq_adapter.collect_statistics(st);
     m_graph.collect_statistics(st);
 }
@@ -598,7 +598,6 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
     literal_vector const& lits = m_nc_functor.get_lits();
     context & ctx = get_context();
     TRACE("arith_conflict", 
-          //display(tout);
           tout << "conflict: ";
           for (unsigned i = 0; i < lits.size(); ++i) {
               ctx.display_literal_info(tout, lits[i]);
@@ -971,10 +970,6 @@ void theory_diff_logic<Ext>::new_diseq_eh(theory_var v1, theory_var v2) {
 }
 
 
-template<typename Ext>
-void theory_diff_logic<Ext>::relevant_eh(app* e) {
-}
-
 
 struct imp_functor {
     conflict_resolution & m_cr;
diff --git a/src/smt/theory_horn_ineq.h b/src/smt/theory_horn_ineq.h
index 441e46a18..fac6e96df 100644
--- a/src/smt/theory_horn_ineq.h
+++ b/src/smt/theory_horn_ineq.h
@@ -85,6 +85,7 @@ namespace smt {
     class theory_horn_ineq : public theory, private Ext {
         
         typedef typename Ext::numeral numeral;
+        typedef typename Ext::inf_numeral inf_numeral;
         typedef literal explanation;
         typedef theory_var th_var;
         typedef svector<th_var> th_var_vector;
diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h
index 0b32c2c8d..505815b4f 100644
--- a/src/smt/theory_horn_ineq_def.h
+++ b/src/smt/theory_horn_ineq_def.h
@@ -797,10 +797,10 @@ namespace smt {
     template<typename Ext>
     typename theory_horn_ineq<Ext>::numeral theory_horn_ineq<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
         if (is_strict) {
-            return numeral(Ext::inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1));
+            return numeral(inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1));
         }
         else {
-            return numeral(Ext::inf_numeral(w));
+            return numeral(inf_numeral(w));
         }
     }
 
@@ -1001,9 +1001,9 @@ namespace smt {
         th_var target = mk_var(ctx.mk_enode(n, false, false, true));        
         coeffs.push_back(std::make_pair(target, rational(-1)));
 
-        VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));        
+        VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal)));        
         negate(coeffs, w);
-        VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));
+        VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal)));
         return target;
     }
     
@@ -1024,9 +1024,9 @@ namespace smt {
             // v = k: v <= k k <= v
             coeffs coeffs;
             coeffs.push_back(std::make_pair(v, rational(1)));
-            VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(r)), null_literal)));
+            VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal)));
             coeffs.back().second.neg();
-            VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(-r)), null_literal)));
+            VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal)));
         }
         return v;
     }
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 40a837136..8b19bdab8 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -201,6 +201,7 @@ namespace smt {
         virtual void assign_eh(bool_var v, bool is_true);
 
         virtual void new_eq_eh(th_var v1, th_var v2) {
+            m_stats.m_num_core2th_eqs++;
             m_arith_eq_adapter.new_eq_eh(v1, v2);
         }
 
@@ -322,10 +323,6 @@ namespace smt {
             return v | 0x1;
         }
 
-        th_var not(th_var v) const {
-            return v ^ 0x1;
-        }
-
     };
 
 
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 97e00c54f..905270a46 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -264,7 +264,7 @@ namespace smt {
     template<typename Ext>
     typename theory_utvpi<Ext>::numeral theory_utvpi<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
         if (is_strict) {
-            return numeral(w) + (is_real?m_epsilon:numeral(1));
+            return numeral(w) + (is_real?Ext::m_epsilon:numeral(1));
         }
         else {
             return numeral(w);
@@ -435,6 +435,7 @@ namespace smt {
             m_nc_functor.reset();
             VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, UINT_MAX, m_nc_functor));
             VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, UINT_MAX, m_nc_functor));
+            IF_VERBOSE(1, verbose_stream() << "parity conflict " << mk_pp(e->get_owner(), get_manager()) << "\n";);
             set_conflict();
                         
             return false;            
@@ -453,7 +454,9 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::collect_statistics(::statistics& st) const {
         st.update("utvpi conflicts",   m_stats.m_num_conflicts);
-        st.update("utvpi assignments", m_stats.m_num_assertions);
+        st.update("utvpi asserts", m_stats.m_num_assertions);
+        st.update("core->utvpi eqs", m_stats.m_num_core2th_eqs);
+        st.update("core->utvpi diseqs", m_stats.m_num_core2th_diseqs);
         m_arith_eq_adapter.collect_statistics(st);
         m_graph.collect_statistics(st);
     }
@@ -669,6 +672,9 @@ namespace smt {
         unsigned sz = m_atoms.size();
         for (unsigned i = 0; i < sz; ++i) {
             bool_var b = m_atoms[i].get_bool_var();
+            if (!ctx.is_relevant(b)) {
+                continue;
+            }
             bool ok = true;
             expr* e = ctx.bool_var2expr(b);
             switch(ctx.get_assignment(b)) {
@@ -681,7 +687,9 @@ namespace smt {
             default:
                 break;
             }
-            CTRACE("utvpi", !ok, tout << "validation failed: " << mk_pp(e, get_manager()) << "\n";);
+            CTRACE("utvpi", !ok, tout << "validation failed:  " << mk_pp(e, get_manager()) << "\n";);
+            // CTRACE("utvpi",  ok, tout << "validation success: " << mk_pp(e, get_manager()) << "\n";);
+            SASSERT(ok);
         }
     }
 
@@ -748,6 +756,7 @@ namespace smt {
         numeral val = val1 - val2;
         rational num = val.get_rational() + (m_delta * val.get_infinitesimal().to_rational());
         num = num/rational(2);
+        num = floor(num);
         return num;
     }
     
@@ -755,7 +764,6 @@ namespace smt {
     model_value_proc * theory_utvpi<Ext>::mk_value(enode * n, model_generator & mg) {
         theory_var v = n->get_th_var(get_id());
         rational num = mk_value(v);
-        num = ceil(num);
         TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
         return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner())));
     }