diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index e44d10c78..34513cc76 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -434,7 +434,9 @@ namespace datalog {
 
     void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
             symbol const * relation_names) {
-        ensure_engine();
+        if (relation_name_cnt > 0) {
+            ensure_engine();
+        }
         if (relation_name_cnt > 0 && m_rel) {
             m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
         }
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 6f81d93d8..e2b679756 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1556,13 +1556,13 @@ namespace pdr {
         if (use_mc) {
             m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
         }
-        if (m_params.use_farkas() && !classify.is_bool()) {
+        if (!classify.is_bool()) {
             m.toggle_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;
-            if (classify.is_dl()) {
+            if (classify.is_dl() && m_params.use_utvpi()) {
                 m_fparams.m_arith_mode = AS_DIFF_LOGIC;
                 m_fparams.m_arith_expand_eqs = true;
             }
@@ -1571,7 +1571,6 @@ namespace pdr {
                 m_fparams.m_arith_mode = AS_UTVPI;
                 m_fparams.m_arith_expand_eqs = true;                
             }
-
         }
         if (m_params.use_convex_hull_generalizer()) {
             m_core_generalizers.push_back(alloc(core_convex_hull_generalizer, *this));
@@ -1800,6 +1799,7 @@ namespace pdr {
             m_expanded_lvl = n.level();
         }
 
+        n.pt().set_use_farkas(m_params.use_farkas());
         if (n.pt().is_reachable(n.state())) {
             TRACE("pdr", tout << "reachable\n";);
             close_node(n);
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 1785991c6..4c26fc1ac 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -166,6 +166,8 @@ namespace pdr {
 
         prop_solver& get_solver() { return m_solver; }
 
+        void set_use_farkas(bool f) { get_solver().set_use_farkas(f); }
+
     };
 
 
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index 5e777bf7e..e73dcdac8 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -196,6 +196,7 @@ namespace pdr {
 
                   );
             model_node nd(0, state, n.pt(), n.level());
+            n.pt().set_use_farkas(true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 TRACE("pdr", 
                       tout << mk_pp(state, m) << "\n";
@@ -260,6 +261,7 @@ namespace pdr {
             expr_ref state = pm.mk_and(conv1);
             TRACE("pdr", tout << "Try:\n" << mk_pp(state, m) << "\n";);
             model_node nd(0, state, n.pt(), n.level());
+            n.pt().set_use_farkas(true);
             if (l_false == n.pt().is_reachable(nd, &conv2, uses_level)) {
                 IF_VERBOSE(0,
                            verbose_stream() << mk_pp(state, m) << "\n";
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index e3cd0d9c5..c7f0bfbc3 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -237,6 +237,7 @@ namespace pdr {
         m_proxies(m),
         m_core(0),
         m_subset_based_core(false),
+        m_use_farkas(false),
         m_in_level(false)
     {
         m_ctx->assert_expr(m_pm.get_background());
@@ -328,7 +329,11 @@ namespace pdr {
             }
         }
 
-        if (result == l_false && m_core && m.proofs_enabled() && !m_subset_based_core) {
+        if (result == l_false  && 
+            m_core && 
+            m.proofs_enabled() && 
+            m_use_farkas    && 
+            !m_subset_based_core) {
             extract_theory_core(safe);
         }
         else if (result == l_false && m_core) {
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h
index 165a37845..7712573ee 100644
--- a/src/muz_qe/pdr_prop_solver.h
+++ b/src/muz_qe/pdr_prop_solver.h
@@ -50,6 +50,7 @@ namespace pdr {
         model_ref*          m_model;
         bool                m_subset_based_core;
         bool                m_assumes_level;
+        bool                m_use_farkas;
         func_decl_set       m_aux_symbols;      
         bool                m_in_level;         
         unsigned            m_current_level;    // set when m_in_level
@@ -97,6 +98,8 @@ namespace pdr {
             ~scoped_level() { m_lev = false; }
         };
         
+        void set_use_farkas(bool f) { m_use_farkas = f; }
+        
         void add_formula(expr * form);
         void add_level_formula(expr * form, unsigned level);