diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index d72d337fa..e9a0bb30e 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -61,13 +61,20 @@ namespace sat {
         m_steps_since_progress = 0;
         unsigned steps = 0;
         save_best_values();
-        while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000) {
-            if (should_reinit_weights()) do_reinit_weights();
-            else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
-            else if (should_restart()) do_restart(), m_plugin->on_restart();
-            else if (do_flip<true>());
-            else shift_weights(), m_plugin->on_rescale();
-            ++steps;
+        try {
+            while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000) {
+                if (should_reinit_weights()) do_reinit_weights();
+                else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
+                else if (should_restart()) do_restart(), m_plugin->on_restart();
+                else if (do_flip<true>());
+                else shift_weights(), m_plugin->on_rescale();
+                verbose_stream() << "steps: " << steps << " min_sz: " << m_min_sz << " unsat: " << m_unsat.size() << "\n";
+                ++steps;
+            }
+        }
+        catch (z3_exception& ex) {
+            IF_VERBOSE(0, verbose_stream() << "Exception: " << ex.msg() << "\n");
+            throw;
         }
         m_plugin->finish_search();
     }
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index b7a800292..5abb17734 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -214,19 +214,20 @@ namespace sls {
     // or flip on first non-negative score
     template<typename num_t>
     void arith_base<num_t>::repair(sat::literal lit, ineq const& ineq) {
-        num_t new_value;
+        num_t new_value, old_value;
         if (UINT_MAX == ineq.m_var_to_flip)
             dtt_reward(lit);
         auto v = ineq.m_var_to_flip;
+        
         if (v == UINT_MAX) {
-            IF_VERBOSE(1, verbose_stream() << "no var to flip\n");
+            IF_VERBOSE(0, verbose_stream() << "no var to flip\n");
             return;
         }
-        // verbose_stream() << "var to flip " << v << "\n";
         if (!cm(ineq, v, new_value)) {
-            IF_VERBOSE(1, verbose_stream() << "no critical move for " << v << "\n");
+            IF_VERBOSE(0, verbose_stream() << "no critical move for " << v << "\n");
             return;
         }
+        verbose_stream() << "repair " << lit << ": " << ineq << " var: v" << v << " := " << value(v) << " -> " << new_value << "\n";
         update(v, new_value);
     }
 
@@ -331,9 +332,11 @@ namespace sls {
     template<typename num_t>
     void arith_base<num_t>::update(var_t v, num_t const& new_value) {
         auto& vi = m_vars[v];
+        expr* e = vi.m_expr;
         auto old_value = vi.m_value;
         if (old_value == new_value)
             return;
+        verbose_stream() << mk_bounded_pp(e, m) << " := " << new_value << "\n";
         for (auto const& [coeff, bv] : vi.m_bool_vars) {
             auto& ineq = *atom(bv);
             bool old_sign = sign(bv);
@@ -354,7 +357,8 @@ namespace sls {
             auto const& ad = m_adds[idx];
             ctx.new_value_eh(m_vars[ad.m_var].m_expr);
         }
-        expr* e = vi.m_expr;
+
+        SASSERT(!m.is_value(e));
         ctx.new_value_eh(e);
     }
 
@@ -374,7 +378,7 @@ namespace sls {
     template<>
     bool arith_base<checked_int64<true>>::is_num(expr* e, checked_int64<true>& i) {
         rational r;
-        if (a.is_numeral(e, r)) {            
+        if (a.is_extended_numeral(e, r)) {            
             if (!r.is_int64())
                 throw overflow_exception();
             i = r.get_int64();
@@ -385,7 +389,7 @@ namespace sls {
 
     template<>
     bool arith_base<rational>::is_num(expr* e, rational& i) {
-        return a.is_numeral(e, i);
+        return a.is_extended_numeral(e, i);
     }
 
     template<typename num_t>
@@ -431,7 +435,7 @@ namespace sls {
             unsigned_vector m;
             num_t c = coeff;
             for (expr* arg : *to_app(e))
-                if (is_num(x, i))
+                if (is_num(arg, i))
                     c *= i;
                 else
                     m.push_back(mk_term(arg));
@@ -620,16 +624,14 @@ namespace sls {
     }
 
     template<typename num_t>
-    void arith_base<num_t>::propagate_literal(sat::literal lit) {
-        TRACE("sls", tout << "repair is-true: " << ctx.is_true(lit) << " lit: " << lit << "\n");
+    void arith_base<num_t>::propagate_literal(sat::literal lit) {        
         if (!ctx.is_true(lit))
             return;
         auto const* ineq = atom(lit.var());
         if (!ineq)
-            return;
-        TRACE("sls", tout << "repair lit: " << lit << " ineq-is-true: " << ineq->is_true() << "\n");
+            return;      
         if (ineq->is_true() != lit.sign())
-            return;        
+            return;
         repair(lit, *ineq);
     }
 
@@ -750,6 +752,9 @@ namespace sls {
         auto const& coeffs = ad.m_args;
         num_t sum(ad.m_coeff);
         num_t val = value(v);
+
+        verbose_stream() << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << value(v) << "\n";
+
         for (auto const& [c, w] : coeffs)
             sum += c * value(w);
         if (val == sum)
@@ -771,13 +776,14 @@ namespace sls {
         auto const& [v, coeff, monomial] = md;
         num_t product(coeff);
         num_t val = value(v);
+        num_t new_value;
         for (auto v : monomial)
             product *= value(v);
         if (product == val)
             return;
-        if (rand() % 20 == 0) {
-            update(v, product);
-        }
+        verbose_stream() << "repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << val << "(" << product << ")\n";
+        if (rand() % 20 == 0) 
+            update(v, product);        
         else if (val == 0) {
             auto v = monomial[ctx.rand(monomial.size())];
             num_t zero(0);
@@ -801,28 +807,30 @@ namespace sls {
             // value1(v) * product / value(v) = val
             // value1(v) = value(v) * val / product
             auto w = monomial[ctx.rand(monomial.size())];
-            auto old_value = value(w);
-            num_t new_value;
-            if (m_vars[w].m_sort == var_sort::REAL) 
-                new_value = old_value * val / product;
-            else
-                new_value = divide(w, old_value * val, product);
+            auto old_value = value(w);            
+            new_value = divide(w, old_value * val, product);
             update(w, new_value);
         }
         else {
-            product = coeff;
+            auto w = monomial[ctx.rand(monomial.size())];
+            num_t prod(coeff);
             for (auto v : monomial) {
-                num_t new_value{ 1 };
+                if (v == w)
+                    continue;
+                num_t new_value(1);
                 if (rand() % 2 == 0)
                     new_value = -1;
-                product *= new_value;
+                prod *= new_value;
                 update(v, new_value);
             }
-            auto v = monomial[ctx.rand(monomial.size())];
-            if ((product < 0 && 0 < val) || (val < 0 && 0 < product))
-                update(v, -val * value(v));
+
+            verbose_stream() << "select random " << coeff << " " << val << " v" << w << "\n";
+            new_value = divide(w, val * value(w), coeff);
+
+            if ((product < 0 && 0 < new_value) || (new_value < 0 && 0 < product))
+                update(w, -new_value);
             else
-                update(v, val * value(v));
+                update(w, new_value);
         }
     }
 
@@ -1076,6 +1084,19 @@ namespace sls {
                     break;
                 }
             }
+            if (sat)
+                continue;
+            verbose_stream() << clause << "\n";
+            for (auto lit : clause.m_clause) {
+                verbose_stream() << lit << " (" << ctx.is_true(lit) << ") ";
+                auto ineq = atom(lit.var());
+                if (!ineq)
+                    continue;
+                verbose_stream() << *ineq << "\n";
+                for (auto const& [coeff, v] : ineq->m_args)
+                    verbose_stream() << coeff << " " << v << " " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << value(v) << "\n";
+            }
+            exit(0);
             if (!sat)
                 return false;
         }
diff --git a/src/ast/sls/sls_arith_plugin.cpp b/src/ast/sls/sls_arith_plugin.cpp
index a95162093..55c041df9 100644
--- a/src/ast/sls/sls_arith_plugin.cpp
+++ b/src/ast/sls/sls_arith_plugin.cpp
@@ -21,34 +21,35 @@ Author:
 
 namespace sls {
 
+#define WITH_FALLBACK(_fn_) \
+    if (!m_arith) { \
+        try {\
+            return m_arith64->_fn_;\
+        }\
+        catch (overflow_exception&) {\
+            init_backup();\
+        }\
+    }\
+    return m_arith->_fn_; \
+
+    arith_plugin::arith_plugin(context& ctx) :
+        plugin(ctx), m_shared(ctx.get_manager()) {
+        m_arith64 = alloc(arith_base<checked_int64<true>>, ctx);
+        m_fid = m_arith64->fid();
+        init_backup();
+    }
+
     void arith_plugin::init_backup() {
         m_arith = alloc(arith_base<rational>, ctx);
         m_arith->initialize();
     }
 
     void arith_plugin::register_term(expr* e) {
-        if (!m_arith) {
-            try {
-                m_arith64->register_term(e);
-                return;
-            }
-            catch (overflow_exception&) {
-                init_backup();
-            }
-        }
-        m_arith->register_term(e);
+        WITH_FALLBACK(register_term(e));
     }
 
     expr_ref arith_plugin::get_value(expr* e) {
-        if (!m_arith) {
-            try {
-                return m_arith64->get_value(e);
-            }
-            catch (overflow_exception&) {
-                init_backup();
-            }
-        }
-        return m_arith->get_value(e);
+        WITH_FALLBACK(get_value(e));
     }
 
     void arith_plugin::initialize() {
@@ -59,28 +60,11 @@ namespace sls {
     }
 
     void arith_plugin::propagate_literal(sat::literal lit) {
-        if (!m_arith) {
-            try {
-                m_arith64->propagate_literal(lit);
-                return;
-            }
-            catch (overflow_exception&) {
-                init_backup();
-            }
-        }
-        m_arith->propagate_literal(lit);
+        WITH_FALLBACK(propagate_literal(lit));
     }
 
     bool arith_plugin::propagate() {
-        if (!m_arith) {
-            try {
-                return m_arith64->propagate();
-            }
-            catch (overflow_exception&) {
-                init_backup();
-            }
-        }
-        return m_arith->propagate();
+        WITH_FALLBACK(propagate());
     }
 
     bool arith_plugin::is_sat() {
@@ -119,29 +103,14 @@ namespace sls {
     }
 
     void arith_plugin::repair_down(app* e) {
-        if (m_arith) 
-            m_arith->repair_down(e);
-        else 
-            m_arith64->repair_down(e);
+        WITH_FALLBACK(repair_down(e));
     }
 
     void arith_plugin::repair_up(app* e) {
-        if (m_arith)
-            m_arith->repair_up(e);
-        else
-            m_arith64->repair_up(e);
+        WITH_FALLBACK(repair_up(e));
     }
 
     void arith_plugin::set_value(expr* e, expr* v) {
-        if (!m_arith) {
-            try {
-                m_arith64->set_value(e, v);
-                return;
-            }
-            catch (overflow_exception&) {
-                init_backup();
-            }
-        }
-        m_arith->set_value(e, v);
+        WITH_FALLBACK(set_value(e, v));       
     }
 }
diff --git a/src/ast/sls/sls_arith_plugin.h b/src/ast/sls/sls_arith_plugin.h
index 53c1a7ba5..1dbc6f027 100644
--- a/src/ast/sls/sls_arith_plugin.h
+++ b/src/ast/sls/sls_arith_plugin.h
@@ -28,11 +28,7 @@ namespace sls {
 
         void init_backup();
     public:
-        arith_plugin(context& ctx) : 
-            plugin(ctx), m_shared(ctx.get_manager()) { 
-            m_arith64 = alloc(arith_base<checked_int64<true>>,ctx); 
-            m_fid = m_arith64->fid();
-        }
+        arith_plugin(context& ctx);
         ~arith_plugin() override {}
         void register_term(expr* e) override;
         expr_ref get_value(expr* e) override;
diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp
index d98ea2652..eb825db81 100644
--- a/src/ast/sls/sls_basic_plugin.cpp
+++ b/src/ast/sls/sls_basic_plugin.cpp
@@ -17,6 +17,8 @@ Author:
 
 #include "ast/sls/sls_basic_plugin.h"
 #include "ast/ast_ll_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 
 namespace sls {
 
@@ -24,50 +26,76 @@ namespace sls {
         return expr_ref(m.mk_bool_val(bval0(e)), m);
     }
 
+    bool basic_plugin::is_basic(expr* e) const {
+        if (!e || !is_app(e))
+            return false;
+        if (to_app(e)->get_family_id() != basic_family_id)
+            return false;
+        if (!m.is_bool(e))
+            return false;
+        expr* x, * y;
+        if (m.is_eq(e, x, y) && !m.is_bool(x))
+            return false;
+        if (m.is_distinct(e) && !m.is_bool(to_app(e)->get_arg(0)))
+            return false;
+        return true;
+    }
+
     void basic_plugin::propagate_literal(sat::literal lit) {
         auto a = ctx.atom(lit.var());
-        if (!a || !is_app(a))
-            return;
-        if (to_app(a)->get_family_id() != basic_family_id)
+        if (!is_basic(a))
             return;
         if (bval1(to_app(a)) != bval0(to_app(a)))
             ctx.new_value_eh(a);
     }
 
     void basic_plugin::register_term(expr* e) {
-        if (is_app(e) && m.is_bool(e) && to_app(e)->get_family_id() == basic_family_id)
+        if (is_basic(e))
             m_values.setx(e->get_id(), bval1(to_app(e)), false);
     }
 
     void basic_plugin::initialize() {
     }
 
+    bool basic_plugin::propagate() {
+        for (auto t : ctx.subterms())
+            if (is_basic(t) && !m.is_not(t) && 
+                bval0(t) != bval1(to_app(t))) {
+                add_clause(to_app(t));
+                return true;
+            }
+
+        return false;
+    }
+
     bool basic_plugin::is_sat() {
         for (auto t : ctx.subterms())
-            if (is_app(t) && 
-                m.is_bool(t) && 
-                to_app(t)->get_family_id() == basic_family_id && 
-                bval0(t) != bval1(to_app(t)))
-                    return false;
+            if (is_basic(t) && !m.is_not(t) && 
+                bval0(t) != bval1(to_app(t))) {
+                verbose_stream() << mk_bounded_pp(t, m) << " := " << (bval0(t) ? "T" : "F") << " eval: " << (bval1(to_app(t)) ? "T" : "F") << "\n";
+                return false;
+            }
         return true;
     }
 
 
     std::ostream& basic_plugin::display(std::ostream& out) const {
         for (auto t : ctx.subterms())
-            if (is_app(t) && m.is_bool(t) && to_app(t)->get_family_id() == basic_family_id)
+            if (is_basic(t))
                 out << mk_bounded_pp(t, m) << " := " << (bval0(t)?"T":"F") << " eval: " << (bval1(to_app(t))?"T":"F") << "\n";
         return out;
     }
 
     void basic_plugin::set_value(expr* e, expr* v) {
-        if (!m.is_bool(e))
+        if (!is_basic(e))
             return;
         SASSERT(m.is_true(v) || m.is_false(v));
         set_value(e, m.is_true(v));
     }
 
     bool basic_plugin::bval1(app* e) const {
+        if (m.is_not(e))
+            return bval1(to_app(e->get_arg(0)));
         SASSERT(m.is_bool(e));
         SASSERT(e->get_family_id() == basic_family_id);
 
@@ -103,6 +131,7 @@ namespace sls {
             auto b = e->get_arg(1);
             if (m.is_bool(a))
                 return bval0(a) == bval0(b);
+            verbose_stream() << mk_bounded_pp(e, m) << " " << ctx.get_value(a) << " " << ctx.get_value(b) << "\n";
             return ctx.get_value(a) == ctx.get_value(b);
         }
         case OP_DISTINCT: {
@@ -123,11 +152,14 @@ namespace sls {
 
     bool basic_plugin::bval0(expr* e) const {
         SASSERT(m.is_bool(e));
+        bool b = true;
+        while (m.is_not(e, e))
+            b = !b;
         sat::bool_var v = ctx.atom2bool_var(e);
         if (v == sat::null_bool_var)
-            return m_values.get(e->get_id(), false);
+            return b == m_values.get(e->get_id(), false);
         else
-            return ctx.is_true(v);
+            return b == ctx.is_true(v);
     }
 
     bool basic_plugin::try_repair(app* e, unsigned i) {
@@ -158,6 +190,56 @@ namespace sls {
         }
     }
 
+    void basic_plugin::add_clause(app* e) {
+        expr_ref_vector es(m);
+        expr_ref fml(m);
+        expr* x, *y;
+        switch (e->get_decl_kind()) {
+        case OP_AND:
+            for (expr* arg : *e) {
+                ctx.add_constraint(m.mk_or(m.mk_not(e), arg));
+                es.push_back(mk_not(m, arg));
+            }
+            es.push_back(e);
+            ctx.add_constraint(m.mk_or(es));
+            break;
+        case OP_OR:            
+            for (expr* arg : *e) {
+                ctx.add_constraint(m.mk_or(mk_not(m, arg), e));
+                es.push_back(arg);                
+            }
+            es.push_back(m.mk_not(e));
+            ctx.add_constraint(m.mk_or(es));
+            break;
+        case OP_NOT:
+            break;
+        case OP_FALSE:
+            break;
+        case OP_TRUE:
+            break;
+        case OP_EQ:
+            VERIFY(m.is_eq(e, x, y));
+            ctx.add_constraint(m.mk_or(m.mk_not(e), mk_not(m, x), y));
+            ctx.add_constraint(m.mk_or(m.mk_not(e), mk_not(m, y), x));
+            ctx.add_constraint(m.mk_or(e, y, x));
+            ctx.add_constraint(m.mk_or(e, mk_not(m, x), mk_not(m, y)));
+            break;
+        case OP_IMPLIES:
+            NOT_IMPLEMENTED_YET();
+        case OP_XOR:
+            NOT_IMPLEMENTED_YET();
+        case OP_ITE:
+            NOT_IMPLEMENTED_YET();
+        case OP_DISTINCT:
+            NOT_IMPLEMENTED_YET();
+        default:
+            UNREACHABLE();
+            break;
+        }
+        
+    }
+
+
     bool basic_plugin::try_repair_and_or(app* e, unsigned i) {
         auto b = bval0(e);
         if ((b && m.is_and(e)) || (!b && m.is_or(e))) {
@@ -245,7 +327,7 @@ namespace sls {
     }
 
     void basic_plugin::repair_up(app* e) {
-        if (!m.is_bool(e) || e->get_family_id() != basic_family_id)
+        if (!is_basic(e))
             return;
         auto b = bval1(e);
         if (bval0(e) == b)
@@ -256,7 +338,7 @@ namespace sls {
     void basic_plugin::repair_down(app* e) {
         SASSERT(m.is_bool(e));
         unsigned n = e->get_num_args();
-        if (n == 0 || e->get_family_id() != m.get_basic_family_id()) 
+        if (n == 0 || !is_basic(e)) 
             return;
         
         if (bval0(e) == bval1(e))
diff --git a/src/ast/sls/sls_basic_plugin.h b/src/ast/sls/sls_basic_plugin.h
index 9aa3aee10..8f9f6b621 100644
--- a/src/ast/sls/sls_basic_plugin.h
+++ b/src/ast/sls/sls_basic_plugin.h
@@ -19,7 +19,8 @@ namespace sls {
     class basic_plugin : public plugin {
         bool_vector        m_values;
         bool               m_initialized = false;
-
+        
+        bool is_basic(expr* e) const;
         bool bval1(app* e) const;
         bool bval0(expr* e) const;
         bool try_repair(app* e, unsigned i);
@@ -32,6 +33,8 @@ namespace sls {
         bool try_repair_distinct(app* e, unsigned i);
         bool set_value(expr* e, bool b);
 
+        void add_clause(app* e);
+
     public:
         basic_plugin(context& ctx) : 
             plugin(ctx) { 
@@ -42,7 +45,7 @@ namespace sls {
         expr_ref get_value(expr* e) override;
         void initialize() override;
         void propagate_literal(sat::literal lit) override;
-        bool propagate() override { return false; }
+        bool propagate() override;
         void repair_down(app* e) override;
         void repair_up(app* e) override;
         bool is_sat() override;
diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp
index 11e5f2e2a..2a2d59573 100644
--- a/src/ast/sls/sls_context.cpp
+++ b/src/ast/sls/sls_context.cpp
@@ -59,15 +59,19 @@ namespace sls {
         // Use timestamps to make it incremental.
         // 
         init();
+        verbose_stream() << "check " << unsat().size() << "\n";
         while (unsat().empty()) {
 
             propagate_boolean_assignment();
 
+            verbose_stream() << "propagate " << unsat().size() << " " << m_new_constraint << "\n";
             // display(verbose_stream());
 
             if (m_new_constraint || !unsat().empty())
                 return l_undef;
 
+            verbose_stream() << unsat().size() << " " << m_new_constraint << "\n";
+
             if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) {
                 model_ref mdl = alloc(model, m);
                 for (expr* e : subterms()) 
@@ -97,8 +101,8 @@ namespace sls {
         while (!m_new_constraint && (!m_repair_up.empty() || !m_repair_down.empty())) {
             while (!m_repair_down.empty() && !m_new_constraint) {
                 auto id = m_repair_down.erase_min();
-                expr* e = term(id);             
-                // verbose_stream() << "repair down " << mk_bounded_pp(e, m) << "\n";
+                expr* e = term(id);
+                TRACE("sls", tout << "repair down " << mk_bounded_pp(e, m) << "\n");
                 if (is_app(e)) {
                     auto p = m_plugins.get(to_app(e)->get_family_id(), nullptr);
                     if (p)
@@ -108,7 +112,7 @@ namespace sls {
             while (!m_repair_up.empty() && !m_new_constraint) {
                 auto id = m_repair_up.erase_min();
                 expr* e = term(id);
-                // verbose_stream() << "repair up " << mk_bounded_pp(e, m) << "\n";
+                TRACE("sls", tout << "repair up " << mk_bounded_pp(e, m) << "\n");
                 if (is_app(e)) {
                     auto p = m_plugins.get(to_app(e)->get_family_id(), nullptr);
                     if (p)
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index 88ec5dc00..22d4e8d69 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -108,32 +108,73 @@ namespace sls {
         // send clauses to ddfw
         // send expression mapping to m_solver_ctx
         
-        sat::literal_vector clause;
-        for (auto f : m_assertions) {
-            if (m.is_or(f)) {
-                clause.reset();
-                for (auto arg : *to_app(f))
-                    clause.push_back(mk_literal(arg));
-                m_solver_ctx->add_clause(clause.size(), clause.data());
-            }
-            else {
-                sat::literal lit = mk_literal(f);
-                m_solver_ctx->add_clause(1, &lit);
-            }
-        }
+        for (auto f : m_assertions) 
+            add_clause(f);
+        
         IF_VERBOSE(10, m_solver_ctx->display(verbose_stream()));
         return m_ddfw.check(0, nullptr);
     }
 
-    sat::literal smt_solver::mk_literal(expr* e) {
-        bool neg = m.is_not(e, e);
-        sat::bool_var v;
-        if (!m_expr2var.find(e, v)) {
-            v = m_expr2var.size();
-            m_expr2var.insert(e, v);
-            m_solver_ctx->register_atom(v, e);
+    void smt_solver::add_clause(expr* f) {
+        sat::literal_vector clause;
+        if (m.is_or(f)) {
+            clause.reset();
+            for (auto arg : *to_app(f))
+                clause.push_back(mk_literal(arg));
+            m_solver_ctx->add_clause(clause.size(), clause.data());
         }
-        return sat::literal(v, neg);
+        else if (m.is_and(f)) {
+            for (auto arg : *to_app(f))
+                add_clause(arg);
+        }
+        else {
+            sat::literal lit = mk_literal(f);
+            m_solver_ctx->add_clause(1, &lit);
+        }
+    }
+
+    sat::literal smt_solver::mk_literal(expr* e) {
+        sat::literal lit;
+        bool neg = false;
+        while (m.is_not(e,e))
+            neg = !neg;
+        if (m_expr2lit.find(e, lit))
+            return neg ? ~lit : lit;
+        sat::literal_vector clause;
+        if (m.is_and(e)) {
+            lit = mk_literal();
+            for (expr* arg : *to_app(e)) {
+                auto lit2 = mk_literal(arg);
+                clause.push_back(~lit2);
+                sat::literal lits[2] = { ~lit, lit2 };
+                m_solver_ctx->add_clause(2, lits);
+            }
+            clause.push_back(lit);
+            m_solver_ctx->add_clause(clause.size(), clause.data());
+        }
+        else if (m.is_or(e)) {
+            lit = mk_literal();
+            for (expr* arg : *to_app(e)) {
+                auto lit2 = mk_literal(arg);
+                clause.push_back(lit2);
+                sat::literal lits[2] = { lit, ~lit2 };
+                m_solver_ctx->add_clause(2, lits);                
+            }
+            clause.push_back(~lit);
+            m_solver_ctx->add_clause(clause.size(), clause.data());
+        }
+        else {
+            sat::bool_var v = m_num_vars++;
+            lit = sat::literal(v, false);
+            m_solver_ctx->register_atom(lit.var(), e);
+        }
+        m_expr2lit.insert(e, lit);
+        return neg ? ~lit : lit;
+    }
+
+    sat::literal smt_solver::mk_literal() {
+        sat::bool_var v = m_num_vars++;
+        return sat::literal(v, false);
     }
     
     model_ref smt_solver::get_model() {
diff --git a/src/ast/sls/sls_smt_solver.h b/src/ast/sls/sls_smt_solver.h
index ebac65021..0f70da4b2 100644
--- a/src/ast/sls/sls_smt_solver.h
+++ b/src/ast/sls/sls_smt_solver.h
@@ -29,9 +29,12 @@ namespace sls {
         solver_ctx* m_solver_ctx = nullptr;        
         expr_ref_vector m_assertions;
         statistics m_st;
-        obj_map<expr, sat::bool_var> m_expr2var;
+        obj_map<expr, sat::literal> m_expr2lit;
+        unsigned m_num_vars = 0;
 
         sat::literal mk_literal(expr* e);
+        sat::literal mk_literal();
+        void add_clause(expr* f);
     public:
         smt_solver(ast_manager& m, params_ref const& p);
         ~smt_solver();
diff --git a/src/util/sat_sls.h b/src/util/sat_sls.h
index bcd3a1c74..82b84bd03 100644
--- a/src/util/sat_sls.h
+++ b/src/util/sat_sls.h
@@ -32,6 +32,10 @@ namespace sat {
         void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
         void del(literal lit) { SASSERT(m_num_trues > 0); --m_num_trues; m_trues -= lit.index(); }
     };
+
+    inline std::ostream& operator<<(std::ostream& out, clause_info const& ci) {
+        return out << ci.m_clause << " w: " << ci.m_weight << " nt: " << ci.m_num_trues;
+    }
 };