diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f17f7a586..f0c31d800 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -60,6 +60,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_expr(r));
         Z3_CATCH_RETURN(0);
     }
@@ -263,6 +264,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_NON_NULL(f, 0);
         expr * e = to_func_interp_ref(f)->get_else();
+        mk_c(c)->save_ast_trail(e);
         RETURN_Z3(of_expr(e));
         Z3_CATCH_RETURN(0);
     }
@@ -301,6 +303,7 @@ extern "C" {
         LOG_Z3_func_entry_get_value(c, e);
         RESET_ERROR_CODE();
         expr * v = to_func_entry_ref(e)->get_result();
+        mk_c(c)->save_ast_trail(v);
         RETURN_Z3(of_expr(v));
         Z3_CATCH_RETURN(0);
     }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index a76933912..1acdb047e 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -362,6 +362,7 @@ void cmd_context::set_opt(opt_wrapper* opt) {
     for (unsigned i = 0; i < m_scopes.size(); ++i) {
         m_opt->push();
     }
+    m_opt->set_logic(m_logic);
 }
 
 void cmd_context::global_params_updated() {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 0dfea0441..091e0765d 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -123,6 +123,7 @@ public:
     virtual void set_hard_constraints(ptr_vector<expr> & hard) = 0;
     virtual void display_assignment(std::ostream& out) = 0;
     virtual bool is_pareto() = 0;
+    virtual void set_logic(symbol const& s) = 0;
 };
 
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 2ddfd1c01..00e6c0336 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -49,6 +49,7 @@ Notes:
 #include "scoped_proof.h"
 #include "blast_term_ite_tactic.h"
 #include "model_implicant.h"
+#include "expr_safe_replace.h"
 
 namespace pdr {
 
@@ -1073,10 +1074,7 @@ namespace pdr {
             predicates.pop_back();
             for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
                 subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
-                dctx.get_rewriter()(tmp);
-                if (!m.is_true(tmp)) {
-                    constraints.push_back(tmp);
-                }
+                constraints.push_back(tmp);                
             }
             for (unsigned i = 0; i < constraints.size(); ++i) {
                 max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
@@ -1099,7 +1097,27 @@ namespace pdr {
 
             children.append(n->children());
         }            
-        return pm.mk_and(constraints);
+        expr_safe_replace repl(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr* e = constraints[i].get(), *e1, *e2;
+            if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
+                repl.insert(e1, e2);
+            }
+            else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
+                repl.insert(e2, e1);
+            }
+        }
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr_ref tmp(m);
+            tmp = constraints[i].get();
+            repl(tmp);
+            dctx.get_rewriter()(tmp);
+            if (!m.is_true(tmp)) {
+                result.push_back(tmp);
+            }
+        }        
+        return pm.mk_and(result);
     }
 
     proof_ref model_search::get_proof_trace(context const& ctx) {
@@ -1232,6 +1250,7 @@ namespace pdr {
             remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
+            m_cache.reset();
         }
     }
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index caa71eeaa..79986067e 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -284,6 +284,7 @@ namespace opt {
     
     lbool context::execute_lex() {
         lbool r = l_true;
+        IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
         for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
             bool is_last = i + 1 == m_objectives.size();
             r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last);
@@ -435,7 +436,8 @@ namespace opt {
     void context::init_solver() {
         #pragma omp critical (opt_context)
         {
-            m_opt_solver = alloc(opt_solver, m, m_params, m_fm, symbol());
+            m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
+            m_opt_solver->set_logic(m_logic);
             m_solver = m_opt_solver.get();
         }
     }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index c2c9f46d8..bbecb4996 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -128,6 +128,7 @@ namespace opt {
         bool                         m_enable_sat;
         bool                         m_enable_sls;
         symbol                       m_maxsat_engine;
+        symbol                       m_logic;
     public:
         context(ast_manager& m);
         virtual ~context();
@@ -153,6 +154,7 @@ namespace opt {
 
         virtual void display_assignment(std::ostream& out);
         virtual bool is_pareto() { return m_pareto.get() != 0; }
+        virtual void set_logic(symbol const& s) { m_logic = s; }
 
         void display(std::ostream& out);
         static void collect_param_descrs(param_descrs & r);
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 186a63105..470acae38 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -36,17 +36,14 @@ Notes:
 namespace opt {
 
     opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, 
-                           filter_model_converter& fm, symbol const & l):
+                           filter_model_converter& fm):
         solver_na2as(mgr),
         m_params(p),
         m_context(mgr, m_params),
         m(mgr),
         m_dump_benchmarks(false),
-        m_fm(fm) {
-        m_logic = l;
-        if (m_logic != symbol::null) {
-            m_context.set_logic(m_logic);
-        }
+        m_fm(fm),
+        m_first(true) {
         m_params.updt_params(p);
         m_params.m_relevancy_lvl = 0;
     }
@@ -83,6 +80,10 @@ namespace opt {
         m_context.pop(n);
     }
 
+    void opt_solver::set_logic(symbol const& logic) {
+        m_context.set_logic(logic);
+    }
+
     smt::theory_opt& opt_solver::get_optimizer() {
         smt::context& ctx = m_context.get_context();                        
         smt::theory_id arith_id = m_context.m().get_family_id("arith");     
@@ -143,7 +144,14 @@ namespace opt {
             IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "...";
                        verbose_stream().flush(););
         }
-        lbool r = m_context.check(num_assumptions, assumptions);
+        lbool r;
+        if (m_first && num_assumptions == 0 && m_context.get_scope_level() == 0) {
+            r = m_context.setup_and_check();
+        }
+        else {
+            r = m_context.check(num_assumptions, assumptions);
+        }
+        m_first = false;
         if (dump_benchmarks()) {
             w.stop();
             IF_VERBOSE(1, verbose_stream() << ".. " << r << " " << std::fixed << w.get_seconds() << ")\n";);
diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h
index 128e12798..07f2e756b 100644
--- a/src/opt/opt_solver.h
+++ b/src/opt/opt_solver.h
@@ -51,8 +51,9 @@ namespace opt {
         bool                m_dump_benchmarks;
         static unsigned     m_dump_count;
         statistics          m_stats;
+        bool                m_first;
     public:
-        opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm, symbol const & l);
+        opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
         virtual ~opt_solver();
 
         virtual void updt_params(params_ref & p);
@@ -61,7 +62,7 @@ namespace opt {
         virtual void assert_expr(expr * t);
         virtual void push_core();
         virtual void pop_core(unsigned n);
-        virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
+        virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);        
         virtual void get_unsat_core(ptr_vector<expr> & r);
         virtual void get_model(model_ref & m);
         virtual proof * get_proof();
@@ -72,6 +73,7 @@ namespace opt {
         virtual unsigned get_num_assertions() const;
         virtual expr * get_assertion(unsigned idx) const;
         virtual void display(std::ostream & out) const;
+        void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);
         void reset_objectives();
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 8428f03ab..0a441755b 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -235,7 +235,6 @@ namespace opt {
     }
 
     lbool optsmt::lex(unsigned obj_index) {
-        IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
         TRACE("opt", tout << "optsmt:lex\n";);
         solver::scoped_push _push(*m_s);
         SASSERT(obj_index < m_vars.size());
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index d933a5f43..a392f8959 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -301,7 +301,7 @@ namespace smt {
     }
 
     void setup::setup_QF_IDL() {
-        TRACE("setup", tout << "setup_QF_IDL(st)\n";);
+        TRACE("setup", tout << "setup_QF_IDL()\n";);
         m_params.m_relevancy_lvl       = 0;
         m_params.m_arith_expand_eqs    = true;
         m_params.m_arith_reflect       = false;
@@ -351,16 +351,15 @@ namespace smt {
         else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
             TRACE("setup", tout << "using dense diff logic...\n";);
             m_params.m_phase_selection = PS_CACHING_CONSERVATIVE;
-#if 0
-            m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));
-#else
             if (st.m_arith_k_sum < rational(INT_MAX / 8))
                 m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
             else
                 m_context.register_plugin(alloc(smt::theory_dense_i, m_manager, m_params));
-#endif
 
         }
+        else if (!m_params.m_arith_auto_config_simplex && !is_dense(st)) {
+            m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params));            
+        }
         else {
             // if (st.m_arith_k_sum < rational(INT_MAX / 8)) {
             //    TRACE("setup", tout << "using small integer simplex...\n";);
@@ -379,6 +378,7 @@ namespace smt {
         m_params.m_arith_reflect    = false;
         m_params.m_nnf_cnf          = false;
         m_params.m_arith_eq_bounds  = true;
+        m_params.m_arith_expand_eqs = true;
         m_params.m_phase_selection  = PS_ALWAYS_FALSE;
         m_params.m_restart_strategy = RS_GEOMETRIC;
         m_params.m_restart_factor   = 1.5;
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 700ed83a3..d7bc45374 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -81,8 +81,10 @@ template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_term(app * term) {
     bool result = null_theory_var != mk_term(term);
     CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
-    TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
-    found_non_diff_logic_expr(term);
+    if (!result) {
+        TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
+        found_non_diff_logic_expr(term);
+    }
     return result;
 }
 
@@ -273,6 +275,8 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
 template<typename Ext>
 void theory_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
     context & ctx  = get_context();
+    ast_manager& m = get_manager();
+    TRACE("arith", tout << mk_pp(atom, m) << "\n";);
     app * lhs      = to_app(atom->get_arg(0));
     app * rhs      = to_app(atom->get_arg(1));
     app * s;
@@ -1070,13 +1074,13 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v, ex
     ast_manager& m = get_manager();
     objective_term const& objective = m_objectives[v];
 
-    IF_VERBOSE(1,
-        for (unsigned i = 0; i < objective.size(); ++i) {
-            verbose_stream() << "Coefficient " << objective[i].second 
-                             << " of theory_var " << objective[i].first << "\n";
-        }
-        verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";);
-
+    TRACE("arith",
+          for (unsigned i = 0; i < objective.size(); ++i) {
+              tout << "Coefficient " << objective[i].second 
+                   << " of theory_var " << objective[i].first << "\n";
+          }
+          tout << "Free coefficient " << m_objective_consts[v] << "\n";
+          );
     unsigned num_nodes = m_graph.get_num_nodes();
     unsigned num_edges = m_graph.get_num_edges();
     vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();