diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 3edb26818..733a5e461 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -3,6 +3,8 @@ RELEASE NOTES
 Version 4.2
 ===========
 
+- Fixed compilation problems with clang/llvm. Many thanks to Xi Wang for finding the problem, and suggesting the fix. 
+
 - Now, Z3 automatically adds arithmetic coercions: to_real and to_int.
   Option (set-option :int-real-coercions false) disables this feature.
   If SMTLIB2_COMPLIANT=true in the command line, then :int-real-coercions is also set to false.
diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp
index 1454d79f5..b9ae51859 100644
--- a/lib/pdr_context.cpp
+++ b/lib/pdr_context.cpp
@@ -55,8 +55,8 @@ namespace pdr {
     // ----------------
     // pred_tansformer
 
-    pred_transformer::pred_transformer(manager& pm, func_decl* head): 
-        pm(pm), m(pm.get_manager()), m_head(head, m), 
+    pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): 
+        ctx(ctx), pm(pm), m(pm.get_manager()), m_head(head, m), 
         m_sig(m), m_solver(pm, head->get_name()),
         m_invariants(m), m_transition(m), m_initial_state(m), 
         m_reachable(pm, pm.get_params()) {}
@@ -464,6 +464,10 @@ 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", 
@@ -1072,7 +1076,8 @@ 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_cancel(false),
+          m_is_dl(false)
     {
     }
 
@@ -1104,7 +1109,7 @@ namespace pdr {
             func_decl* pred = dit->m_key;
             TRACE("pdr", tout << mk_pp(pred, m) << "\n";);
             SASSERT(!rels.contains(pred));
-            e = rels.insert_if_not_there2(pred, alloc(pred_transformer, get_pdr_manager(), pred));            
+            e = rels.insert_if_not_there2(pred, alloc(pred_transformer, *this, get_pdr_manager(), pred));            
             datalog::rule_vector const& pred_rules = *dit->m_value;            
             for (unsigned i = 0; i < pred_rules.size(); ++i) {
                 e->get_data().m_value->add_rule(pred_rules[i]);
@@ -1120,7 +1125,7 @@ namespace pdr {
             for (; itf != endf; ++itf) {
                 TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";);
                 if (!rels.find(*itf, pt_user)) {
-                    pt_user = alloc(pred_transformer, get_pdr_manager(), *itf);
+                    pt_user = alloc(pred_transformer, *this, get_pdr_manager(), *itf);
                     rels.insert(*itf, pt_user);
                 }
                 pt_user->add_use(pt);                
@@ -1179,7 +1184,7 @@ namespace pdr {
     void context::add_cover(int level, func_decl* p, expr* property) {
         pred_transformer* pt = 0;
         if (!m_rels.find(p, pt)) {
-            pt = alloc(pred_transformer, get_pdr_manager(), p);
+            pt = alloc(pred_transformer, *this, get_pdr_manager(), p);
             m_rels.insert(p, pt);
             IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";);
         }
@@ -1192,9 +1197,11 @@ namespace pdr {
         arith_util a;
         bool m_is_bool;
         bool m_is_bool_arith;
+        bool m_has_arith;
+        bool m_is_dl;
     public:
         classifier_proc(ast_manager& m, datalog::rule_set& rules):
-            m(m), a(m), m_is_bool(true), m_is_bool_arith(true) {
+            m(m), a(m), m_is_bool(true), m_is_bool_arith(true), m_has_arith(false), m_is_dl(false) {
             classify(rules);
         }
         void operator()(expr* e) {
@@ -1213,6 +1220,9 @@ namespace pdr {
                     m_is_bool = false;
                 }
             }
+
+            m_has_arith = m_has_arith || a.is_int_real(e);
+
             if (m_is_bool_arith) {                
                 if (!m.is_bool(e) && !a.is_int_real(e)) {
                     m_is_bool_arith = false;
@@ -1235,6 +1245,8 @@ namespace pdr {
 
         bool is_bool_arith() const { return m_is_bool_arith; }
 
+        bool is_dl() const { return m_is_dl; }
+
 
     private:
 
@@ -1249,9 +1261,23 @@ namespace pdr {
                     classify_pred(mark, r.get_tail(i));                
                 }
                 for (unsigned i = utsz; i < r.get_tail_size(); ++i) {
-                    quick_for_each_expr(*this, mark, r.get_tail(i));
+                    quick_for_each_expr(*this, mark, r.get_tail(i));                    
                 }
             }
+            mark.reset();
+ 
+            m_is_dl = false;
+            if (m_has_arith) {
+                ptr_vector<expr> forms;
+                for (it = rules.begin(); it != end; ++it) {  
+                    datalog::rule& r = *(*it);
+                    unsigned utsz = r.get_uninterpreted_tail_size();
+                    for (unsigned i = utsz; i < r.get_tail_size(); ++i) {
+                        forms.push_back(r.get_tail(i));
+                    }                                          
+                }
+                m_is_dl = is_difference_logic(m, forms.size(), forms.c_ptr());
+            }
         }
 
         void classify_pred(expr_fast_mark1& mark, app* pred) {
@@ -1270,6 +1296,7 @@ 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));
@@ -1277,12 +1304,16 @@ namespace pdr {
         if (m_params.get_bool(":use-farkas", true) && !classify.is_bool()) {
             if (m_params.get_bool(":inline-proof-mode", true)) {
                 m.toggle_proof_mode(PGM_FINE);
-                m_fparams.m_proof_mode = PGM_FINE;
+                m_fparams.m_proof_mode = PGM_FINE;                
                 m_fparams.m_arith_bound_prop = BP_NONE;
                 m_fparams.m_arith_auto_config_simplex = true;
                 m_fparams.m_arith_propagate_eqs = false;
                 m_fparams.m_arith_eager_eq_axioms = false;
-                m_fparams.m_arith_eq_bounds = false;
+                if (classify.is_dl()) {
+                    m_fparams.m_arith_mode = AS_DIFF_LOGIC;
+                    m_fparams.m_arith_expand_eqs = true;
+                    m_is_dl = true;
+                }
             }
             else {
                 m_core_generalizers.push_back(alloc(core_farkas_generalizer, *this, m, m_fparams));
@@ -1622,6 +1653,8 @@ 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();
@@ -1629,7 +1662,7 @@ namespace pdr {
         expr* T   = pt.get_transition(r);
         expr* phi = n.state();
 
-        IF_VERBOSE(2, verbose_stream() << "Model:\n";
+        IF_VERBOSE(3, verbose_stream() << "Model:\n";
                    model_smt2_pp(verbose_stream(), m, *M, 0);
                    verbose_stream() << "\n";
                    verbose_stream() << "Transition:\n" << mk_pp(T, m) << "\n";
@@ -1641,7 +1674,7 @@ namespace pdr {
         forms.push_back(phi);
         datalog::flatten_and(forms);        
         ptr_vector<expr> forms1(forms.size(), forms.c_ptr());
-        if (m_params.get_bool(":use-model-generalizer", false)) {
+        if (use_model_generalizer) {
             Phi.append(mev.minimize_model(forms1, M));
         }
         else {
@@ -1663,6 +1696,9 @@ namespace pdr {
         qe_lite qe(m);
         expr_ref phi1 = m_pm.mk_and(Phi);
         qe(vars, phi1);
+        if (!use_model_generalizer) {
+            reduce_disequalities(*M, 3, phi1);
+        }
 
         IF_VERBOSE(2, 
                    verbose_stream() << "Vars:\n";
diff --git a/lib/pdr_context.h b/lib/pdr_context.h
index cd56c7536..fe8bc8e90 100644
--- a/lib/pdr_context.h
+++ b/lib/pdr_context.h
@@ -40,11 +40,13 @@ namespace pdr {
 
     class pred_transformer;
     class model_node;
+    class context;
 
     typedef obj_map<datalog::rule const, qinst*> qinst_map;
     typedef obj_map<datalog::rule const, app_ref_vector*> rule2inst;
     typedef obj_map<func_decl, pred_transformer*> decl2rel;
 
+
     // 
     // Predicate transformer state.
     // A predicate transformer corresponds to the 
@@ -64,6 +66,7 @@ namespace pdr {
 
         manager&                     pm;        // pdr-manager
         ast_manager&                 m;         // manager
+        context&                     ctx;
         
         func_decl_ref                m_head;    // predicate 
         func_decl_ref_vector         m_sig;     // signature
@@ -106,7 +109,7 @@ namespace pdr {
         void add_premises(decl2rel const& pts, unsigned lvl, datalog::rule& rule, expr_ref_vector& r);
 
     public:
-        pred_transformer(manager& pm, func_decl* head);
+        pred_transformer(context& ctx, manager& pm, func_decl* head);
         ~pred_transformer();
 
         void add_rule(datalog::rule* r) { m_rules.push_back(r); }
@@ -259,7 +262,6 @@ namespace pdr {
     struct model_exception { };
     struct inductive_exception {};
 
-    class context;
 
     // 'state' is unsatisfiable at 'level' with 'core'. 
     // Minimize or weaken core.
@@ -306,6 +308,7 @@ 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();
@@ -361,9 +364,11 @@ namespace pdr {
         decl2rel const&   get_pred_transformers() const { return m_rels; }
         pred_transformer& get_pred_transformer(func_decl* p) const { return *m_rels.find(p); }
         datalog::context& get_context() const { SASSERT(m_context); return *m_context; }
-
         expr_ref          get_answer();
 
+        bool              is_dl() const { return m_is_dl; }
+
+
         void collect_statistics(statistics& st) const;
 
         std::ostream& display(std::ostream& strm) const;        
diff --git a/lib/pdr_farkas_learner.cpp b/lib/pdr_farkas_learner.cpp
index c5dfd62f3..6494bd223 100644
--- a/lib/pdr_farkas_learner.cpp
+++ b/lib/pdr_farkas_learner.cpp
@@ -204,6 +204,7 @@ namespace pdr {
                     is_eq = false;
                 }
             }
+
             zero = a.mk_numeral(rational::zero(), a.is_int(res));
             if (is_eq) {
                 res = m.mk_eq(res, zero);
@@ -219,8 +220,28 @@ namespace pdr {
             proof_ref pr(m);
             expr_ref tmp(m);
             rw(res, tmp, pr);
+            fix_dl(tmp);
             res = tmp;
         }
+
+        // patch: swap addends to make static 
+        // features recognize difference constraint.
+        void fix_dl(expr_ref& r) {
+            expr* e;
+            if (m.is_not(r, e)) {
+                r = e;
+                fix_dl(r);
+                r = m.mk_not(r);
+                return;
+            }
+            expr* e1, *e2, *e3, *e4;
+            if ((m.is_eq(r, e1, e2) || a.is_lt(r, e1, e2) || a.is_gt(r, e1, e2) || 
+                 a.is_le(r, e1, e2) || a.is_ge(r, e1, e2))) {
+                if (a.is_add(e1, e3, e4) && a.is_mul(e3)) {
+                    r = m.mk_app(to_app(r)->get_decl(), a.mk_add(e4,e3), e2);
+                }
+            }
+        }
     };
     
     farkas_learner::farkas_learner(front_end_params& params, ast_manager& outer_mgr) 
@@ -366,6 +387,7 @@ namespace pdr {
         for (unsigned i = 0; i < lemmas.size(); ++i) {
             g->assert_expr(lemmas[i].get()); 
         }
+        expr_ref tmp(m);
         model_converter_ref mc;
         proof_converter_ref pc;
         expr_dependency_ref core(m);
diff --git a/lib/pdr_prop_solver.cpp b/lib/pdr_prop_solver.cpp
index 2908bf4f6..865bfe32b 100644
--- a/lib/pdr_prop_solver.cpp
+++ b/lib/pdr_prop_solver.cpp
@@ -342,12 +342,23 @@ namespace pdr {
         fl.get_lemmas(pr, bs, lemmas);
         safe.elim_proxies(lemmas);
         fl.simplify_lemmas(lemmas); // redundant
+        if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
+            !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
+                IF_VERBOSE(1, 
+                    verbose_stream() << "not diff\n";
+                    for (unsigned i = 0; i < lemmas.size(); ++i) {
+                        verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+                    });
+                extract_subset_core(safe);
+                return;
+        }
+        
 
         IF_VERBOSE(2, 
-            verbose_stream() << "Lemmas\n";            
-        for (unsigned i = 0; i < lemmas.size(); ++i) {
-            verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
-        });
+                   verbose_stream() << "Lemmas\n";            
+                   for (unsigned i = 0; i < lemmas.size(); ++i) {
+                       verbose_stream() << mk_pp(lemmas[i].get(), m) << "\n";
+                   });
 
         m_core->reset();
         m_core->append(lemmas);
diff --git a/lib/pdr_util.cpp b/lib/pdr_util.cpp
index 13f2dbb29..56876af5e 100644
--- a/lib/pdr_util.cpp
+++ b/lib/pdr_util.cpp
@@ -41,48 +41,51 @@ Notes:
 #include "pdr_prop_solver.h"
 #include "pdr_util.h"
 #include "arith_decl_plugin.h"
+#include "expr_replacer.h"
+#include "static_features.h"
+
 
 namespace pdr {
 
-unsigned ceil_log2(unsigned u)
-{
-    if (u==0) { return 0; }
-    unsigned pow2 = next_power_of_two(u);
-    return get_num_1bits(pow2-1);
-}
-
-
-std::string pp_cube(const ptr_vector<expr>& model, ast_manager& m) {
-    return pp_cube(model.size(), model.c_ptr(), m);
-}
-std::string pp_cube(const expr_ref_vector& model, ast_manager& m) {
-    return pp_cube(model.size(), model.c_ptr(), m);
-}
-std::string pp_cube(const app_ref_vector& model, ast_manager& m) {
-    return pp_cube(model.size(), model.c_ptr(), m);
-}
-
-std::string pp_cube(const app_vector& model, ast_manager& m) {
-    return pp_cube(model.size(), model.c_ptr(), m);
-}
-
-std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) {
-    return pp_cube(sz, reinterpret_cast<expr * const *>(lits), m);
-}
-
-std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
-    std::stringstream res;
-    res << "(";
-    expr * const * end = lits+sz;
-    for (expr * const * it = lits; it!=end; it++) {
-        res << mk_pp(*it, m);
-        if (it+1!=end) {
-            res << ", ";
-        }
+    unsigned ceil_log2(unsigned u) {
+        if (u == 0) { return 0; }
+        unsigned pow2 = next_power_of_two(u);
+        return get_num_1bits(pow2-1);
+    }
+
+    std::string pp_cube(const ptr_vector<expr>& model, ast_manager& m) {
+        return pp_cube(model.size(), model.c_ptr(), m);
+    }
+
+    std::string pp_cube(const expr_ref_vector& model, ast_manager& m) {
+        return pp_cube(model.size(), model.c_ptr(), m);
+    }
+
+    std::string pp_cube(const app_ref_vector& model, ast_manager& m) {
+        return pp_cube(model.size(), model.c_ptr(), m);
+    }
+    
+    std::string pp_cube(const app_vector& model, ast_manager& m) {
+        return pp_cube(model.size(), model.c_ptr(), m);
+    }
+
+    std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) {
+        return pp_cube(sz, reinterpret_cast<expr * const *>(lits), m);
+    }
+
+    std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
+        std::stringstream res;
+        res << "(";
+        expr * const * end = lits+sz;
+        for (expr * const * it = lits; it!=end; it++) {
+            res << mk_pp(*it, m);
+            if (it+1!=end) {
+                res << ", ";
+            }
+        }
+        res << ")";
+        return res.str();
     }
-    res << ")";
-    return res.str();
-}
 
 
 /////////////////////////
@@ -105,7 +108,7 @@ void model_evaluator::assign_value(expr* e, expr* val) {
         set_value(e, val);
     }
     else {
-        IF_VERBOSE(2, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
+        IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
         TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
         set_x(e);
     }
@@ -673,8 +676,7 @@ void model_evaluator::eval_basic(app* e) {
 }
 
 bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
-    ptr_vector<expr> todo;
-    assign_vector_with_casting(todo, formulas);
+    ptr_vector<expr> todo(formulas);
 
     while (!todo.empty()) {
         expr * curr_e = todo.back();
@@ -735,69 +737,235 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
     return !has_x;
 }
 
-func_decl * mk_store(ast_manager& m, sort * arr_sort)
-{
-    family_id array_fid = m.get_family_id(symbol("array"));
-
-    unsigned num_params = arr_sort->get_num_parameters();
-
-    ptr_vector<sort> domain;
-    domain.push_back(arr_sort);
-
-    //we push params of the array as remaining arguments of the store. The first 
-    //num_params-1 parameters are indices and the last one is the range of the array
-    for (unsigned i=0; i<num_params; ++i) {
-        domain.push_back(to_sort(arr_sort->get_parameter(i).get_ast()));
+    func_decl * mk_store(ast_manager& m, sort * arr_sort)
+    {
+        family_id array_fid = m.get_family_id(symbol("array"));
+        
+        unsigned num_params = arr_sort->get_num_parameters();
+        
+        ptr_vector<sort> domain;
+        domain.push_back(arr_sort);
+        
+        //we push params of the array as remaining arguments of the store. The first 
+        //num_params-1 parameters are indices and the last one is the range of the array
+        for (unsigned i=0; i<num_params; ++i) {
+            domain.push_back(to_sort(arr_sort->get_parameter(i).get_ast()));
+        }
+        
+        return m.mk_func_decl(array_fid, OP_STORE, 
+                              arr_sort->get_num_parameters(), arr_sort->get_parameters(), 
+                              domain.size(), domain.c_ptr(), arr_sort);
     }
 
-    return m.mk_func_decl(array_fid, OP_STORE, 
-        arr_sort->get_num_parameters(), arr_sort->get_parameters(), 
-        domain.size(), domain.c_ptr(), arr_sort);
-}
+    void get_as_array_value(const model_core & mdl, expr * arr_e, expr_ref& res) {
+        ast_manager& m = mdl.get_manager();
+        array_util pl(m);
+        SASSERT(pl.is_as_array(arr_e));
+        
+        app * arr = to_app(arr_e);
+    
+        unsigned sz = 0;
+        func_decl_ref f(pl.get_as_array_func_decl(arr), m);
+        sort * arr_sort = arr->get_decl()->get_range();
+        func_interp* g = mdl.get_func_interp(f);
+        
+        res = pl.mk_const_array(arr_sort, g->get_else());
 
-void get_as_array_value(const model_core & mdl, expr * arr_e, expr_ref& res) {
-    ast_manager& m = mdl.get_manager();
-    array_util pl(m);
-    SASSERT(pl.is_as_array(arr_e));
-
-    app * arr = to_app(arr_e);
-
-    unsigned sz = 0;
-    func_decl_ref f(pl.get_as_array_func_decl(arr), m);
-    sort * arr_sort = arr->get_decl()->get_range();
-    func_interp* g = mdl.get_func_interp(f);
-
-    res = pl.mk_const_array(arr_sort, g->get_else());
-
-    unsigned arity = f->get_arity();
-
-    sz = g->num_entries();
-    if (sz) {
-        func_decl_ref store_fn(mk_store(m, arr_sort), m);
-        ptr_vector<expr> store_args;
-        for (unsigned i = 0; i < sz; ++i) {
-            const func_entry * fe = g->get_entry(i);
-            store_args.reset();
-            store_args.push_back(res);
-            store_args.append(arity, fe->get_args());
-            store_args.push_back(fe->get_result());
-            res = m.mk_app(store_fn, store_args.size(), store_args.c_ptr());
+        unsigned arity = f->get_arity();
+        
+        sz = g->num_entries();
+        if (sz) {
+            func_decl_ref store_fn(mk_store(m, arr_sort), m);
+            ptr_vector<expr> store_args;
+            for (unsigned i = 0; i < sz; ++i) {
+                const func_entry * fe = g->get_entry(i);
+                store_args.reset();
+                store_args.push_back(res);
+                store_args.append(arity, fe->get_args());
+                store_args.push_back(fe->get_result());
+                res = m.mk_app(store_fn, store_args.size(), store_args.c_ptr());
+            }
         }
     }
-}
 
-void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res) {
-    SASSERT(f->get_arity()==0);
-    ast_manager& m = mdl.get_manager();
-
-    res = mdl.get_const_interp(f);
-
-    array_util pl(m);
-
-    if (pl.is_as_array(res)) {
-        get_as_array_value(mdl, res, res);
+    void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res) {
+        SASSERT(f->get_arity()==0);
+        ast_manager& m = mdl.get_manager();
+        
+        res = mdl.get_const_interp(f);
+        
+        array_util pl(m);
+        
+        if (pl.is_as_array(res)) {
+            get_as_array_value(mdl, res, res);
+        }
     }
-}
+    
+    void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
+        ast_manager& m = fml.get_manager();
+        expr_ref_vector conjs(m);
+        datalog::flatten_and(fml, conjs);
+        obj_map<expr, unsigned> diseqs;
+        expr* n, *lhs, *rhs;
+        for (unsigned i = 0; i < conjs.size(); ++i) {
+            if (m.is_not(conjs[i].get(), n) &&
+                m.is_eq(n, lhs, rhs)) {
+                if (!m.is_value(rhs)) {
+                    std::swap(lhs, rhs);
+                }
+                if (!m.is_value(rhs)) {
+                    continue;
+                }
+                diseqs.insert_if_not_there2(lhs, 0)->get_data().m_value++;
+            }
+        }
+        expr_substitution sub(m);
+
+        unsigned orig_size = conjs.size();
+        unsigned num_deleted = 0;
+        expr_ref val(m), tmp(m);
+        proof_ref pr(m);
+        pr = m.mk_asserted(m.mk_true());
+        obj_map<expr, unsigned>::iterator it  = diseqs.begin();
+        obj_map<expr, unsigned>::iterator end = diseqs.end();
+        for (; it != end; ++it) {
+            if (it->m_value >= threshold) {
+                model.eval(it->m_key, val);
+                sub.insert(it->m_key, val, pr);
+                conjs.push_back(m.mk_eq(it->m_key, val));
+                num_deleted += it->m_value;
+            }
+        }
+        if (orig_size < conjs.size()) {
+            scoped_ptr<expr_replacer> rep = mk_expr_simp_replacer(m);
+            rep->set_substitution(&sub);
+            for (unsigned i = 0; i < orig_size; ++i) {
+                tmp = conjs[i].get();
+                (*rep)(tmp);
+                if (m.is_true(tmp)) {
+                    conjs[i] = conjs.back();
+                    SASSERT(orig_size <= conjs.size());
+                    conjs.pop_back();
+                    SASSERT(orig_size <= 1 + conjs.size());
+                    if (i + 1 == orig_size) {
+                        // no-op.
+                    }
+                    else if (orig_size <= conjs.size()) {
+                        // no-op
+                    }
+                    else {
+                        SASSERT(orig_size == 1 + conjs.size());
+                        --orig_size;
+                        --i;
+                    }
+                }
+                else {
+                    conjs[i] = tmp;
+                }
+            }            
+            IF_VERBOSE(2, verbose_stream() << "Deleted " << num_deleted << " disequalities " << conjs.size() << " conjuncts\n";);
+        }
+        fml = m.mk_and(conjs.size(), conjs.c_ptr());        
+    }
+
+    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) {
+            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)) {
+                    expr_ref e1(m), e2(m);
+                    ptr_vector<expr> args1(num_args, args);
+                    args1[i] = t;
+                    e1 = m.mk_app(f, num_args, args1.c_ptr());
+                    args1[i] = e;
+                    e2 = m.mk_app(f, num_args, args1.c_ptr());
+                    result = m.mk_ite(c, e1, e2);
+                    return BR_REWRITE3;
+                }
+            }
+            return BR_FAILED;
+        }
+    };
+
+    struct ite_hoister_cfg: public default_rewriter_cfg {
+        ite_hoister m_r;
+        bool rewrite_patterns() const { return false; }
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            return m_r.mk_app_core(f, num, args, result);
+        }
+        ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}
+        
+    };
+
+    class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
+        ite_hoister_cfg m_cfg;
+    public:
+        ite_hoister_star(ast_manager & m, params_ref const & p):
+            rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
+            m_cfg(m, p) {}
+    };
+
+    template class rewriter_tpl<ite_hoister_cfg>;
 
 
+    class scoped_no_proof {
+        ast_manager& m;
+        proof_gen_mode m_mode;
+    public:
+        scoped_no_proof(ast_manager& m): m(m) {
+            m_mode = m.proof_mode();
+            m.toggle_proof_mode(PGM_DISABLED);
+        }
+        ~scoped_no_proof() {
+            m.toggle_proof_mode(m_mode);            
+        }
+    };
+
+    void hoist_non_bool_if(expr_ref& fml) {
+        ast_manager& m = fml.get_manager();
+        scoped_no_proof _sp(m);
+        params_ref p;
+        ite_hoister_star ite_rw(m, p);
+        expr_ref tmp(m);
+        ite_rw(fml, tmp);
+        fml = tmp;
+    }
+
+    class test_diff_logic {
+        ast_manager& m;
+        arith_util a;
+        bool m_is_dl;
+    public:
+        test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {}
+        
+        void operator()(expr* e) {
+            if (m_is_dl && a.is_arith_expr(e) && !a.is_numeral(e) && 
+                !a.is_add(e) && !a.is_mul(e) && !m.is_bool(e)) {
+                m_is_dl = false;
+            }
+        }
+
+        bool is_dl() const { return m_is_dl; }
+    };
+
+    bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
+        static_features st(m);
+        st.collect(num_fmls, fmls);
+        if (st.m_num_arith_eqs != st.m_num_diff_eqs ||
+            st.m_num_arith_terms != st.m_num_diff_terms ||
+            st.m_num_arith_ineqs != st.m_num_diff_ineqs) {     
+            return false;
+        }
+        test_diff_logic test(m);
+        expr_fast_mark1 mark;
+        for (unsigned i = 0; i < num_fmls; ++i) {
+            quick_for_each_expr(test, mark, fmls[i]);
+        } 
+        return test.is_dl();
+    }  
+
 }
diff --git a/lib/pdr_util.h b/lib/pdr_util.h
index 4f6ab1ad3..810831592 100644
--- a/lib/pdr_util.h
+++ b/lib/pdr_util.h
@@ -25,231 +25,123 @@ Revision History:
 #include "obj_hashtable.h"
 #include "ref_vector.h"
 #include "simplifier.h"
-#include "th_rewriter.h"
 #include "trace.h"
 #include "vector.h"
 #include "arith_decl_plugin.h"
 #include "bv_decl_plugin.h"
 
 
-struct front_end_params;
 class model;
 class model_core;
 
 namespace pdr {
-    class manager;
-    class prop_solver;
 
-/**
- * Return the ceiling of base 2 logarithm of a number, 
- * or zero if the nmber is zero.
- */
-unsigned ceil_log2(unsigned u);
-
-typedef ptr_vector<app> app_vector;
-typedef ptr_vector<func_decl> decl_vector;
-typedef obj_hashtable<func_decl> func_decl_set;
-
-
-std::string pp_cube(const ptr_vector<expr>& model, ast_manager& manager);
-std::string pp_cube(const expr_ref_vector& model, ast_manager& manager);
-std::string pp_cube(const ptr_vector<app>& model, ast_manager& manager);
-std::string pp_cube(const app_ref_vector& model, ast_manager& manager);
-std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager);
-std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager);
-
-
-template<class TgtVect, class SrcVect>
-void assign_vector_with_casting(TgtVect& tgt, const SrcVect& src)
-{
-    SASSERT(static_cast<const void*>(&tgt)!=static_cast<const void*>(&src));
-    tgt.reset();
-    typename SrcVect::data const * begin = src.c_ptr();
-    typename SrcVect::data const * end = begin + src.size();
-    for(typename SrcVect::data const * it = begin; it!=end; it++)
-    {
-        tgt.push_back(static_cast<typename TgtVect::data>(*it));
-    }
-/*    tgt.reset();
-    typename SrcVect::const_iterator end = src.end();
-    for(typename SrcVect::const_iterator it = src.begin(); it!=end; it++)
-    {
-        tgt.push_back(static_cast<typename TgtVect::data>(*it));
-    }*/
-}
-
-template<class TgtType, class SrcType, class Mgr>
-void append_ref_vector_with_casting(ref_vector<TgtType,Mgr> & tgt, const ref_vector<SrcType,Mgr> & src)
-{
-    SASSERT(static_cast<const void*>(&tgt)!=static_cast<const void*>(&src));
-    SrcType * const * begin = src.c_ptr();
-    SrcType * const * end = begin + src.size();
-    for(SrcType * const * it = begin; it!=end; it++)
-    {
-        tgt.push_back(static_cast<TgtType *>(*it));
-    }
-}
-
-template<class TgtType, class SrcType, class Mgr>
-void assign_ref_vector_with_casting(ref_vector<TgtType,Mgr> & tgt, const ref_vector<SrcType,Mgr> & src)
-{
-    SASSERT(static_cast<const void*>(&tgt)!=static_cast<const void*>(&src));
-    tgt.reset();
-    append_ref_vector_with_casting(tgt, src);
-}
-
-template<class T,class M>
-ref_vector<T,M>& assign_ref_vector(ref_vector<T,M> & tgt, const ref_vector<T,M> & src)
-{
-    SASSERT(static_cast<const void*>(&tgt)!=static_cast<const void*>(&src));
-    //we support assignment only on vectors with the same manager
-    SASSERT(&tgt.get_manager()==&src.get_manager());
-    tgt.reset();
-    tgt.append(src);
-    return tgt;
-}
-
-template<class Type, class Mgr, class Comp>
-void sort_ref_vect(ref_vector<Type,Mgr> & vect, Comp cmp)
-{
-    Type * * begin = vect.c_ptr();
-    Type * * end = begin + vect.size();
-    std::sort(begin, end, cmp);
-}
-
-/**
-Into res put all elements that are in left but not in right.
-
-This function can change the order of elements in left.
-*/
-template<class Type, class Mgr, class Comp>
-void vect_set_diff(ref_vector<Type,Mgr> & left, ref_vector<Type,Mgr> & right, 
-    ref_vector<Type,Mgr> & res, Comp cmp)
-{
-    sort_ref_vect(left, cmp);
-    sort_ref_vect(right, cmp);
-
-    res.reset();
-
-    Type * const * lbegin = left.c_ptr();
-    Type * const * lend = lbegin + left.size();
-    Type * const * lit = lbegin;
-    Type * const * rbegin = right.c_ptr();
-    Type * const * rend = rbegin + right.size();
-    Type * const * rit = rbegin;
-
-    while(lit!=lend) {
-        while(rit!=rend && lit!=lend && *rit==*lit) {
-            ++rit;
-            ++lit;
-        }
-        if(lit==lend) {
-            return;
-        }
-        while(rit!=rend && cmp(*rit, *lit)) {
-            ++rit;
-        }
-        while(lit!=lend && (rit==rend || cmp(*lit, *rit))) {
-            res.push_back(*lit);
-            ++lit;
-        }
-    }
-}
-
-/**
-Ensure all elements from src are in tgt
-
-This function can change the order of elements in tgt and src.
-*/
-template<class Type, class Mgr, class Comp>
-void vect_set_union(ref_vector<Type,Mgr> & tgt, ref_vector<Type,Mgr> & src, Comp cmp)
-{
-    ref_vector<Type,Mgr> diff(tgt.get_manager());
-    vect_set_diff(src, tgt, diff, cmp);
-    tgt.append(diff);
-}
-
-
-
-class model_evaluator {
-    ast_manager& m;
-    arith_util   m_arith;
-    bv_util      m_bv;
-    obj_map<expr,rational> m_numbers;
-    expr_ref_vector        m_refs;
-    obj_map<expr, expr*>   m_values;
-    model_ref m_model;
-
-    //00 -- non-visited
-    //01 -- X
-    //10 -- false
-    //11 -- true
-    ast_fast_mark1 m1;
-    ast_fast_mark2 m2;
-    unsigned m_level1;
-    unsigned m_level2;
-    expr_mark m_visited;
-
-
-    void reset();
-    void setup_model(model_ref& model);
-    void assign_value(expr* e, expr* v);
-    void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
-    void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
-    expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
-    void eval_arith(app* e);
-    void eval_basic(app* e);
-    void eval_iff(app* e, expr* arg1, expr* arg2);
-    void inherit_value(expr* e, expr* v);
-
-    //00 -- non-visited
-    //01 -- X
-    //10 -- false
-    //11 -- true
-    inline bool is_unknown(expr* x)  { return !m1.is_marked(x) && !m2.is_marked(x); }
-    inline void set_unknown(expr* x)  { m1.reset_mark(x); m2.reset_mark(x); }
-    inline bool is_x(expr* x)  { return !m1.is_marked(x) && m2.is_marked(x); }
-    inline bool is_false(expr* x)  { return m1.is_marked(x) && !m2.is_marked(x); }
-    inline bool is_true(expr* x)  { return m1.is_marked(x) && m2.is_marked(x); }
-    inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
-    inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
-    inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
-    inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
-    inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
-    inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
-    inline void set_number(expr* x, rational const& v) { set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); }
-    inline expr* get_value(expr* x) { return m_values.find(x); }
-    inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
+    /**
+     * Return the ceiling of base 2 logarithm of a number, 
+     * or zero if the nmber is zero.
+     */
+    unsigned ceil_log2(unsigned u);
 
+    typedef ptr_vector<app> app_vector;
+    typedef ptr_vector<func_decl> decl_vector;
+    typedef obj_hashtable<func_decl> func_decl_set;
     
-protected:
+    std::string pp_cube(const ptr_vector<expr>& model, ast_manager& manager);
+    std::string pp_cube(const expr_ref_vector& model, ast_manager& manager);
+    std::string pp_cube(const ptr_vector<app>& model, ast_manager& manager);
+    std::string pp_cube(const app_ref_vector& model, ast_manager& manager);
+    std::string pp_cube(unsigned sz, app * const * lits, ast_manager& manager);
+    std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& manager);
+    
+    class model_evaluator {
+        ast_manager&           m;
+        arith_util             m_arith;
+        obj_map<expr,rational> m_numbers;
+        expr_ref_vector        m_refs;
+        obj_map<expr, expr*>   m_values;
+        model_ref              m_model;
+        
+        //00 -- non-visited
+        //01 -- X
+        //10 -- false
+        //11 -- true
+        ast_fast_mark1 m1;
+        ast_fast_mark2 m2;
+        unsigned       m_level1;
+        unsigned       m_level2;
+        expr_mark      m_visited;
+        
 
-    bool check_model(ptr_vector<expr> const & formulas);
+        void reset();
+        void setup_model(model_ref& model);
+        void assign_value(expr* e, expr* v);
+        void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect);
+        void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect);
+        expr_ref_vector prune_by_cone_of_influence(ptr_vector<expr> const & formulas);
+        void eval_arith(app* e);
+        void eval_basic(app* e);
+        void eval_iff(app* e, expr* arg1, expr* arg2);
+        void inherit_value(expr* e, expr* v);
+        
+        inline bool is_unknown(expr* x)  { return !m1.is_marked(x) && !m2.is_marked(x); }
+        inline void set_unknown(expr* x)  { m1.reset_mark(x); m2.reset_mark(x); }
+        inline bool is_x(expr* x)  { return !m1.is_marked(x) && m2.is_marked(x); }
+        inline bool is_false(expr* x)  { return m1.is_marked(x) && !m2.is_marked(x); }
+        inline bool is_true(expr* x)  { return m1.is_marked(x) && m2.is_marked(x); }
+        inline void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); }
+        inline void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+        inline void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); }
+        inline void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); }
+        inline void set_bool(expr* x, bool v) { if (v) { set_true(x); } else { set_false(x); } }
+        inline rational const& get_number(expr* x) const { return m_numbers.find(x); }
+        inline void set_number(expr* x, rational const& v) { 
+            set_v(x); TRACE("pdr_verbose", tout << mk_pp(x,m) << " " << v << "\n";); m_numbers.insert(x,v); 
+        }
+        inline expr* get_value(expr* x) { return m_values.find(x); }
+        inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); }
+        
+        bool check_model(ptr_vector<expr> const & formulas);
+        
+    public:
+        model_evaluator(ast_manager& m) : m(m), m_arith(m), m_refs(m) {}
+            
+        /**
+           \brief extract equalities from model that suffice to satisfy formula.
+               
+           \pre model satisfies formulas
+        */
+            
+       expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
+            
+       /**
+          \brief extract literals from formulas that satisfy formulas.
 
-public:
-    model_evaluator(ast_manager& m) : m(m), m_arith(m), m_bv(m), m_refs(m) {}
+          \pre model satisfies formulas
+       */
+       expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
+
+
+       // for_each_expr visitor.
+       void operator()(expr* e) {} 
+    };
+
+    void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);
 
     /**
-       \brief extract equalities from model that suffice to satisfy formula.
-
-       \pre model satisfies formulas
-    */
-
-    expr_ref_vector minimize_model(ptr_vector<expr> const & formulas, model_ref& mdl);
+       \brief replace variables that are used in many disequalities by
+       an equality using the model. 
+       
+       Assumption: the model satisfies the conjunctions.       
+     */
+    void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml);
+    
 
     /**
-       \brief extract literals from formulas that satisfy formulas.
+       \brief hoist non-boolean if expressions.
+     */
+    void hoist_non_bool_if(expr_ref& fml);
 
-       \pre model satisfies formulas
-    */
-    expr_ref_vector minimize_literals(ptr_vector<expr> const & formulas, model_ref& mdl);
-
-
-    // for_each_expr visitor.
-    void operator()(expr* e) {} 
-};
-
-void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res);
+    bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls);
 
 }
 
diff --git a/lib/static_features.cpp b/lib/static_features.cpp
index 7de27ca62..234626365 100644
--- a/lib/static_features.cpp
+++ b/lib/static_features.cpp
@@ -130,20 +130,23 @@ bool static_features::is_diff_atom(expr const * e) const {
         return false;
     SASSERT(to_app(e)->get_num_args() == 2);
     expr * lhs = to_app(e)->get_arg(0);
-    SASSERT(is_numeral(to_app(e)->get_arg(1)));
+    expr * rhs = to_app(e)->get_arg(1);
+    if (!is_arith_expr(lhs) && !is_arith_expr(rhs)) 
+        return true;    
+    if (!is_numeral(rhs)) 
+        return false;    
     // lhs can be 'x' or '(+ x (* -1 y))'
     if (!is_arith_expr(lhs))
         return true;
-    SASSERT(is_app(lhs));
-    // lhs must be (+ x (* -1 y))
-    if (to_app(lhs)->get_decl_kind() != OP_ADD || to_app(lhs)->get_num_args() != 2)
-        return false;
+    expr* arg1, *arg2;
+    if (!m_autil.is_add(lhs, arg1, arg2)) 
+        return false;    
     // x
-    if (is_arith_expr(to_app(lhs)->get_arg(0)))
+    if (is_arith_expr(arg1))
         return false;
-    expr * arg2 = to_app(lhs)->get_arg(1);
     // arg2: (* -1 y)
-    return m_autil.is_mul(arg2) && to_app(arg2)->get_num_args() == 2 && is_minus_one(to_app(arg2)->get_arg(0)) && !is_arith_expr(to_app(arg2)->get_arg(1));
+    expr* m1, *m2;
+    return m_autil.is_mul(arg2, m1, m2) &&  is_minus_one(m1) && !is_arith_expr(m2);
 }
 
 bool static_features::is_gate(expr const * e) const {
diff --git a/lib/theory_diff_logic.cpp b/lib/theory_diff_logic.cpp
index ec8cc2d68..86351e36f 100644
--- a/lib/theory_diff_logic.cpp
+++ b/lib/theory_diff_logic.cpp
@@ -16,14 +16,6 @@ Author:
 
 Revision History:
 
-TODO:
-
-- port diff_logic.*
-- port theory_diff_logic
-- fix theory propagation 
-- fix/add equality propagation
-- fix relaxation.
-
 --*/
 #include "theory_diff_logic.h"
 
diff --git a/lib/theory_diff_logic.h b/lib/theory_diff_logic.h
index 20de5b464..80d729001 100644
--- a/lib/theory_diff_logic.h
+++ b/lib/theory_diff_logic.h
@@ -16,30 +16,6 @@ Author:
 
 Revision History:
 
-TODO:
-
-- check regressions with smt::solver.
-
-- what should be done properly (during internalization) for reflect()
-
-- fix theory propagation:
-  - x <= y + 2, then x <= y + 3
-  - x = y, then x <= y + 2
-  - x = y, x <= z <= y, then x = z
-
-- fix/add equality propagation
-
-- add relaxation (somewhat easy)
-
-- Currently stored explanation in edges is stored at creation time
-  (not at propagation time).
-  Is this flexible enough for processing equalities?
-  - eq_justification present in smt::context when calling new_eq_eh.
-    pass such to the edge?
-  
-- context::assume_eq is absent.
-- context::add_eq and context::push_eq are protected. Cannot propagate equalities back to core.
-- 
 
 --*/
 
@@ -76,13 +52,7 @@ namespace smt {
         unsigned   m_num_core2th_diseqs;
         unsigned   m_num_core2th_new_diseqs;
         void reset() {
-            m_num_conflicts          = 0;
-            m_num_assertions         = 0;
-            m_num_th2core_prop       = 0;
-            m_num_th2core_eqs        = 0;
-            m_num_core2th_eqs        = 0;
-            m_num_core2th_diseqs     = 0;
-            m_num_core2th_new_diseqs = 0;
+            memset(this, 0, sizeof(*this));
         }
         theory_diff_logic_statistics() {
             reset();
@@ -93,17 +63,12 @@ namespace smt {
     public:
         dl_conflict(region & r, unsigned nls, literal const * lits): simple_justification(r, nls, lits) { }
             
-        virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; }
+        virtual proof * mk_proof(conflict_resolution & cr) { 
+            NOT_IMPLEMENTED_YET();
+            return 0;
+        }
     };
 
-    class dl_propagate : public simple_justification {
-    public:
-        dl_propagate(region & r, unsigned nls, literal const * lits): simple_justification(r, nls, lits) { }
-
-        virtual proof * mk_proof(conflict_resolution & cr) { NOT_IMPLEMENTED_YET(); return 0; }
-    };
-
-
 
     template<typename Ext>
     class theory_diff_logic : public theory, private Ext {
diff --git a/lib/theory_diff_logic_def.h b/lib/theory_diff_logic_def.h
index 54518cd8d..05785f3cd 100644
--- a/lib/theory_diff_logic_def.h
+++ b/lib/theory_diff_logic_def.h
@@ -403,18 +403,23 @@ void theory_diff_logic<Ext>::del_atoms(unsigned old_size) {
 
 template<typename Ext>
 bool theory_diff_logic<Ext>::is_negative(app* n, app*& m) { 
-    if (!m_util.is_mul(n) || n->get_num_args() != 2) {
+    expr* a0, *a1, *a2;
+    rational r;
+    if (!m_util.is_mul(n, a0, a1)) {
         return false;
     }
-    rational r;
-    expr* a0 = n->get_arg(0);
-    expr* a1 = n->get_arg(1);
+    if (m_util.is_numeral(a1)) {
+        std::swap(a0, a1);
+    }
     if (m_util.is_numeral(a0, r) && r.is_minus_one() && is_app(a1)) {
         m = to_app(a1);
         return true;
     }
-    if (m_util.is_numeral(a1, r) && r.is_minus_one() && is_app(a0)) {
-        m = to_app(a0);
+    if (m_util.is_uminus(a1)) {
+        std::swap(a0, a1);
+    }
+    if (m_util.is_uminus(a0, a2) && m_util.is_numeral(a2, r) && r.is_one() && is_app(a1)) {
+        m = to_app(a1);
         return true;
     }
     return false;
@@ -615,7 +620,12 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
 
     justification * js = 0;
     if (get_manager().proofs_enabled()) {
-        js = 0; // TBD?
+        vector<parameter> params;
+        params.push_back(parameter(symbol("farkas")));
+        params.resize(lits.size()+1, parameter(rational(1)));
+        js = new (ctx.get_region()) theory_lemma_justification(get_id(), ctx, 
+                   lits.size(), lits.c_ptr(), 
+                   params.size(), params.c_ptr());
     }
     clause_del_eh* del_eh = alloc(theory_diff_logic_del_eh, *this);
     clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, del_eh);
@@ -675,7 +685,18 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
         ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
     }
 
-    ctx.set_conflict(ctx.mk_justification(dl_conflict(r, lits.size(), lits.c_ptr())));
+    vector<parameter> params;
+    if (get_manager().proofs_enabled()) {
+        params.push_back(parameter(symbol("farkas")));
+        params.resize(lits.size()+1, parameter(rational(1)));
+    } 
+   
+    ctx.set_conflict(
+        ctx.mk_justification(
+            ext_theory_conflict_justification(
+                get_id(), ctx.get_region(), 
+                lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr())));
+
 }
 
 template<typename Ext>