diff --git a/src/sat/sat_binspr.cpp b/src/sat/sat_binspr.cpp
index 670e7dfd8..c73dab168 100644
--- a/src/sat/sat_binspr.cpp
+++ b/src/sat/sat_binspr.cpp
@@ -132,21 +132,43 @@ namespace sat {
     };
 
     void binspr::operator()() {
-        unsigned num = s.num_vars();
+        s = alloc(solver, m_solver.params(), m_solver.rlimit());
+        m_solver.pop_to_base_level();
+        s->copy(m_solver, true);
+        unsigned num = s->num_vars();
         m_bin_clauses = 0;
 
         report _rep(*this);
         m_use_list.reset();
-        m_use_list.reserve(num*2);
-        for (clause* c : s.m_clauses) {
+        m_use_list.reserve(num * 2);
+        for (clause* c : s->m_clauses) {
             if (!c->frozen() && !c->was_removed()) { 
                 for (literal lit : *c) {
                     m_use_list[lit.index()].push_back(c);
                 }
             }
         }
-        TRACE("sat", s.display(tout););
+        TRACE("sat", s->display(tout););
         algorithm2();
+        if (!s->inconsistent()) {
+            params_ref p;
+            p.set_uint("sat.max_conflicts", 10000);
+            p.set_bool("sat.binspr", false);
+            s->updt_params(p);
+            lbool r = s->check(0, nullptr);
+        }
+
+        if (s->inconsistent()) {
+            s->set_conflict();
+        }
+        else {
+            s->pop_to_base_level();
+            for (unsigned i = m_solver.init_trail_size(); i < s->init_trail_size(); ++i) {
+                literal lit = s->trail_literal(i);
+                m_solver.assign(lit, s->get_justification(lit));
+            }
+            TRACE("sat", tout << "added " << (s->init_trail_size() - m_solver.init_trail_size()) << " units\n";);
+        }
     }
 
 
@@ -167,48 +189,48 @@ namespace sat {
 
     void binspr::algorithm2() {
         mk_masks();
-        unsigned num_lits = 2 * s.num_vars();
-        for (unsigned l_idx = 0; l_idx < num_lits && !s.inconsistent(); ++l_idx) {
-            s.checkpoint();
+        unsigned num_lits = 2 * s->num_vars();
+        for (unsigned l_idx = 0; l_idx < num_lits && !s->inconsistent(); ++l_idx) {
+            s->checkpoint();
             literal p = to_literal(l_idx);
-            TRACE("sat", tout << "p " << p << " " << s.value(p) << "\n";);
-            if (is_used(p) && s.value(p) == l_undef) {
-                s.push();
-                s.assign_scoped(p);
-                unsigned sz_p = s.m_trail.size();
-                s.propagate(false);
-                if (s.inconsistent()) {
-                    s.pop(1);
-                    s.assign_unit(~p);
-                    s.propagate(false);
-                    TRACE("sat", s.display(tout << "unit\n"););
+            TRACE("sat", tout << "p " << p << " " << s->value(p) << "\n";);
+            if (is_used(p) && s->value(p) == l_undef) {
+                s->push();
+                s->assign_scoped(p);
+                unsigned sz_p = s->m_trail.size();
+                s->propagate(false);
+                if (s->inconsistent()) {
+                    s->pop(1);
+                    s->assign_unit(~p);
+                    s->propagate(false);
+                    TRACE("sat", s->display(tout << "unit\n"););
                     IF_VERBOSE(0, verbose_stream() << "unit " << (~p) << "\n");
                     continue;
                 }
-                for (unsigned i = sz_p; !s.inconsistent() && i < s.m_trail.size(); ++i) {
-                    literal u = ~s.m_trail[i];
+                for (unsigned i = sz_p; !s->inconsistent() && i < s->m_trail.size(); ++i) {
+                    literal u = ~s->m_trail[i];
                     TRACE("sat", tout << "p " << p << " u " << u << "\n";);
                     for (clause* cp : m_use_list[u.index()]) {
                         for (literal q : *cp) {
-                            if (s.inconsistent()) 
+                            if (s->inconsistent()) 
                                 break;
-                            if (s.value(q) != l_undef) 
+                            if (s->value(q) != l_undef) 
                                 continue;
 
-                            s.push();
-                            s.assign_scoped(q);
-                            unsigned sz_q = s.m_trail.size();
-                            s.propagate(false);
-                            if (s.inconsistent()) {
+                            s->push();
+                            s->assign_scoped(q);
+                            unsigned sz_q = s->m_trail.size();
+                            s->propagate(false);
+                            if (s->inconsistent()) {
                                 // learn ~p or ~q
-                                s.pop(1);
+                                s->pop(1);
                                 block_binary(p, q, true);
-                                s.propagate(false);
+                                s->propagate(false);
                                 continue;
                             }
                             bool found = false;
-                            for (unsigned j = sz_q; !found && j < s.m_trail.size(); ++j) {
-                                literal v = ~s.m_trail[j];
+                            for (unsigned j = sz_q; !found && j < s->m_trail.size(); ++j) {
+                                literal v = ~s->m_trail[j];
                                 for (clause* cp2 : m_use_list[v.index()]) {                                    
                                     if (cp2->contains(p)) {
                                         if (check_spr(p, q, u, v)) {
@@ -218,29 +240,29 @@ namespace sat {
                                     }
                                 }
                             }
-                            s.pop(1);
+                            s->pop(1);
                             if (found) {
                                 block_binary(p, q, false);
-                                s.propagate(false);
-                                TRACE("sat", s.display(tout););
+                                s->propagate(false);
+                                TRACE("sat", s->display(tout););
                             }
                         }
                     }
                 }
-                s.pop(1);
+                s->pop(1);
             }
         }               
     }
 
     bool binspr::is_used(literal lit) const {
-        return !m_use_list[lit.index()].empty() || !s.get_wlist(~lit).empty();
+        return !m_use_list[lit.index()].empty() || !s->get_wlist(~lit).empty();
     }
     
     bool binspr::check_spr(literal p, literal q, literal u, literal v) {
-        SASSERT(s.value(p) == l_true);
-        SASSERT(s.value(q) == l_true);
-        SASSERT(s.value(u) == l_false);
-        SASSERT(s.value(v) == l_false);
+        SASSERT(s->value(p) == l_true);
+        SASSERT(s->value(q) == l_true);
+        SASSERT(s->value(u) == l_false);
+        SASSERT(s->value(v) == l_false);
         init_g(p, q, u, v);
         literal lits[4] = { p, q, ~u, ~v };
         for (unsigned i = 0; g_is_sat() && i < 4; ++i) {
@@ -252,7 +274,7 @@ namespace sat {
     }
 
     void binspr::binary_are_unit_implied(literal p) {
-        for (watched const& w : s.get_wlist(~p)) {
+        for (watched const& w : s->get_wlist(~p)) {
             if (!g_is_sat()) {
                 break;
             }
@@ -270,13 +292,13 @@ namespace sat {
                 continue;
             }
 
-            bool inconsistent = (s.value(lit) == l_true);
-            if (s.value(lit) == l_undef) {
-                s.push();
-                s.assign_scoped(~lit);
-                s.propagate(false);
-                inconsistent = s.inconsistent();
-                s.pop(1);
+            bool inconsistent = (s->value(lit) == l_true);
+            if (s->value(lit) == l_undef) {
+                s->push();
+                s->assign_scoped(~lit);
+                s->propagate(false);
+                inconsistent = s->inconsistent();
+                s->pop(1);
             }
 
             if (!inconsistent) {            
@@ -295,23 +317,23 @@ namespace sat {
     }
 
     void binspr::clause_is_unit_implied(clause const& c) {
-        s.push();
+        s->push();
         clear_alpha();
         for (literal lit : c) {
             if (touch(lit)) {
                 continue;
             }
-            else if (s.value(lit) == l_true) {
-                s.pop(1);
+            else if (s->value(lit) == l_true) {
+                s->pop(1);
                 return;
             }
-            else if (s.value(lit) != l_false) {
-                s.assign_scoped(~lit);
+            else if (s->value(lit) != l_false) {
+                s->assign_scoped(~lit);
             }
         }
-        s.propagate(false);
-        bool inconsistent = s.inconsistent();
-        s.pop(1);
+        s->propagate(false);
+        bool inconsistent = s->inconsistent();
+        s->pop(1);
         if (!inconsistent) {
             add_touched();
         }
@@ -321,7 +343,7 @@ namespace sat {
     void binspr::block_binary(literal lit1, literal lit2, bool learned) {
         IF_VERBOSE(2, verbose_stream() << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n");
         TRACE("sat", tout << "SPR: " << learned << " " << ~lit1 << " " << ~lit2 << "\n";);
-        s.mk_clause(~lit1, ~lit2, learned);
+        s->mk_clause(~lit1, ~lit2, learned);
         ++m_bin_clauses;
     }
 
diff --git a/src/sat/sat_binspr.h b/src/sat/sat_binspr.h
index ddab19368..7531e592c 100644
--- a/src/sat/sat_binspr.h
+++ b/src/sat/sat_binspr.h
@@ -37,7 +37,8 @@ namespace sat {
             not_pr              = 0x0
         };
 
-        solver& s;
+        solver&                              m_solver;
+        scoped_ptr<solver>                   s;
         unsigned                             m_bin_clauses;
         unsigned                             m_stopped_at;
         vector<clause_vector>                m_use_list;
@@ -92,7 +93,7 @@ namespace sat {
 
     public:
 
-        binspr(solver& s, params_ref const& p): s(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) {}
+        binspr(solver& s): m_solver(s), m_stopped_at(0), m_limit1(1000), m_limit2(300) {}
 
         ~binspr() {}
 
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index b93665430..832b58f6e 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -99,7 +99,7 @@ namespace sat {
         m_local_search_dbg_flips = p.local_search_dbg_flips();
         m_unit_walk       = p.unit_walk();
         m_unit_walk_threads = p.unit_walk_threads();
-        m_binspr            = false; // unsound :-( p.binspr();
+        m_binspr            = p.binspr();
         m_lookahead_simplify = p.lookahead_simplify();
         m_lookahead_double = p.lookahead_double();
         m_lookahead_simplify_bca = p.lookahead_simplify_bca();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 4068adc08..860105583 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -53,6 +53,7 @@ namespace sat {
         m_asymm_branch(*this, p),
         m_probing(*this, p),
         m_mus(*this),
+        m_binspr(*this),
         m_inconsistent(false),
         m_searching(false),
         m_conflict(justification(0)),
@@ -1921,6 +1922,10 @@ namespace sat {
             }
         }
 
+        if (m_config.m_binspr && !inconsistent()) {
+            m_binspr();
+        }
+
 #if 0
         static unsigned file_no = 0;
         #pragma omp critical (print_sat)
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index c5dc7c9d3..4fb587c7c 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -34,6 +34,7 @@ Revision History:
 #include "sat/sat_iff3_finder.h"
 #include "sat/sat_probing.h"
 #include "sat/sat_mus.h"
+#include "sat/sat_binspr.h"
 #include "sat/sat_drat.h"
 #include "sat/sat_parallel.h"
 #include "sat/sat_local_search.h"
@@ -102,6 +103,7 @@ namespace sat {
         asymm_branch            m_asymm_branch;
         probing                 m_probing;
         mus                     m_mus;           // MUS for minimal core extraction
+        binspr                  m_binspr;
         bool                    m_inconsistent;
         bool                    m_searching;
         // A conflict is usually a single justification. That is, a justification
@@ -323,6 +325,8 @@ namespace sat {
         bool  at_base_lvl() const override { return m_scope_lvl == 0; }
         lbool value(literal l) const { return m_assignment[l.index()]; }
         lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
+        justification get_justification(literal l) const { return m_justification[l.var()]; }
+        justification get_justification(bool_var v) const { return m_justification[v]; }
         unsigned lvl(bool_var v) const { return m_justification[v].level(); }
         unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
         unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
@@ -612,6 +616,7 @@ namespace sat {
         void pop_to_base_level() override;
         unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
         reslimit& rlimit() { return m_rlimit; }
+        params_ref const& params() { return m_params; }
         // -----------------------
         //
         // Simplification
diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index e14b9434f..2c64772e0 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -1253,7 +1253,7 @@ namespace smt {
 
 
     case_split_queue * mk_case_split_queue(context & ctx, smt_params & p) {
-        if (p.m_relevancy_lvl < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
+        if (ctx.relevancy_lvl() < 2 && (p.m_case_split_strategy == CS_RELEVANCY || p.m_case_split_strategy == CS_RELEVANCY_ACTIVITY || 
                 p.m_case_split_strategy == CS_RELEVANCY_GOAL)) {
             warning_msg("relevancy must be enabled to use option CASE_SPLIT=3, 4 or 5");
             p.m_case_split_strategy = CS_ACTIVITY;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 1c64901c3..e554ce715 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -46,6 +46,7 @@ namespace smt {
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
+        m_relevancy_lvl(2),
         m_asserted_formulas(m, p, _p),
         m_rewriter(m),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
@@ -321,7 +322,7 @@ namespace smt {
 
         TRACE("relevancy",
               tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
-        if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
+        if (d.is_atom() && (m_relevancy_lvl == 0 || (m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
             m_atom_propagation_queue.push_back(l);
 
         if (m.has_trace_stream())
@@ -1582,7 +1583,7 @@ namespace smt {
             SASSERT(relevancy());
             // Quantifiers are only asserted when marked as relevant.
             // Other atoms are only asserted when marked as relevant if m_relevancy_lvl >= 2
-            if (d.is_atom() && (d.is_quantifier() || m_fparams.m_relevancy_lvl >= 2)) {
+            if (d.is_atom() && (d.is_quantifier() || m_relevancy_lvl >= 2)) {
                 lbool val  = get_assignment(v);
                 if (val != l_undef)
                     m_atom_propagation_queue.push_back(literal(v, val == l_false));
@@ -3391,9 +3392,12 @@ namespace smt {
     }
 
     void context::setup_context(bool use_static_features) {
-        if (m_setup.already_configured() || inconsistent())
+        if (m_setup.already_configured() || inconsistent()) {
+            m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl);
             return;
+        }
         m_setup(get_config_mode(use_static_features));
+        m_relevancy_lvl = m_fparams.m_relevancy_lvl;
         setup_components();
     }
 
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 81e58d7ff..ff0c4609b 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -83,6 +83,7 @@ namespace smt {
         smt_params &                m_fparams;
         params_ref                  m_params;
         setup                       m_setup;
+        unsigned                    m_relevancy_lvl;
         timer                       m_timer;
         asserted_formulas           m_asserted_formulas;
         th_rewriter                 m_rewriter;
@@ -196,8 +197,8 @@ namespace smt {
 
         literal_vector              m_atom_propagation_queue;
 
-        obj_map<expr, unsigned>      m_cached_generation;
-        obj_hashtable<expr>          m_cache_generation_visited;
+        obj_map<expr, unsigned>     m_cached_generation;
+        obj_hashtable<expr>         m_cache_generation_visited;
         dyn_ack_manager             m_dyn_ack_manager;
 
         // -----------------------------------
@@ -280,9 +281,11 @@ namespace smt {
         }
 
         bool relevancy() const {
-            return m_fparams.m_relevancy_lvl > 0;
+            return m_relevancy_lvl > 0;
         }
 
+        unsigned relevancy_lvl() const { return m_relevancy_lvl; }
+
         enode * get_enode(expr const * n) const {
             SASSERT(e_internalized(n));
             return m_app2enode[n->get_id()];
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 0ee56069e..0f3dd2b5c 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1195,7 +1195,7 @@ namespace smt {
         // Reason: when a learned clause becomes unit, it should mark the
         // unit literal as relevant. When binary_clause_opt is used,
         // it is not possible to distinguish between learned and non-learned clauses.
-        if (lemma && m_fparams.m_relevancy_lvl >= 2)
+        if (lemma && m_relevancy_lvl >= 2)
             return false; 
         if (m_base_lvl > 0)
             return false;
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 955327904..7b80c44af 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -497,7 +497,7 @@ namespace smt {
         mk_func_interps();
         finalize_theory_models();
         register_macros();
-        TRACE("model", model_v2_pp(tout, *m_model, true););
+        TRACE("model", model_v2_pp(tout, *m_model, true););        
         return m_model.get();
     }
     
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3a81f18ec..fd2acf42b 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3684,7 +3684,6 @@ bool theory_seq::internalize_term(app* term) {
         return true;
     }
     for (auto arg : *term) {        
-        ensure_enodes(arg);
         mk_var(ensure_enode(arg));
     }
     if (m.is_bool(term)) {
@@ -5135,6 +5134,7 @@ void theory_seq::ensure_enodes(expr* e) {
             }
         }
     }	
+    // TBD: std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), compare_depth);
     for (unsigned i = m_ensure_todo.size(); i-- > 0; ) {
         ensure_enode(m_ensure_todo[i]);
     }