diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index bd7e6291d..fb49b679e 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -63,6 +63,7 @@ namespace polysat {
     }
 
     void bool_var_manager::reset_marks() {
+        LOG_V("-------------------------- (reset boolean marks)");
         m_marks.reserve(size());
         m_clock++;
         if (m_clock != 0)
@@ -72,7 +73,19 @@ namespace polysat {
     }
 
     void bool_var_manager::set_mark(sat::bool_var var) {
+        LOG_V("Marking: b" << var);
         SASSERT(var != sat::null_bool_var);
         m_marks[var] = m_clock;
     }
+
+    std::ostream& bool_var_manager::display(std::ostream& out) const {
+        for (sat::bool_var v = 0; v < size(); ++v) {
+            sat::literal lit{v};
+            if (value(lit) == l_true)
+                out << " " << lit;
+            if (value(lit) == l_false)
+                out << " " << ~lit;
+        }
+        return out;
+    }
 }
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index 977dcfc22..c7e40bd98 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -58,6 +58,10 @@ namespace polysat {
         /// Set the given literal to true
         void assign(sat::literal lit, unsigned lvl, clause* reason, clause* lemma);
         void unassign(sat::literal lit);
+
+        std::ostream& display(std::ostream& out) const;
     };
 
+    inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); }
+
 }
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index b4610b757..9ec8ca6bc 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -22,31 +22,51 @@ Author:
 
 namespace polysat {
 
-    constraint* constraint_manager::insert(scoped_ptr<constraint>&& sc) {
-        constraint* c = sc.detach();
+    constraint* constraint_manager::insert(constraint_ref c) {
         LOG_V("Inserting constraint: " << show_deref(c));
         SASSERT(c);
         SASSERT(c->bvar() != sat::null_bool_var);
-        SASSERT(get_bv2c(c->bvar()) == nullptr);
-        insert_bv2c(c->bvar(), c);
+        SASSERT(get_bv2c(c->bvar()) == c.get());
         // TODO: use explicit insert_external(constraint* c, unsigned dep) for that.
         if (c->dep() && c->dep()->is_leaf()) {
             unsigned dep = c->dep()->leaf_value();
             SASSERT(!m_external_constraints.contains(dep));
-            m_external_constraints.insert(dep, c);
+            m_external_constraints.insert(dep, c.get());
         }
         while (m_constraints.size() <= c->level())
             m_constraints.push_back({});
-        m_constraints[c->level()].push_back(c);
-        return c;
+        constraint* pc = c.get();
+        m_constraints[c->level()].push_back(std::move(c));
+        return pc;
+    }
+
+    clause* constraint_manager::insert(clause_ref cl) {
+        SASSERT(cl);
+        // Insert new constraints
+        for (constraint* c : cl->m_new_constraints)
+            // TODO: if (!inserted) ?
+            insert(c);
+        cl->m_new_constraints = {};  // free vector memory
+        // Insert clause
+        while (m_clauses.size() <= cl->level())
+            m_clauses.push_back({});
+        clause* pcl = cl.get();
+        m_clauses[cl->level()].push_back(std::move(cl));
+        return pcl;
     }
 
     // Release constraints at the given level and above.
     void constraint_manager::release_level(unsigned lvl) {
+        for (unsigned l = m_clauses.size(); l-- > lvl; ) {
+            for (auto const& cl : m_clauses[l]) {
+                SASSERT_EQ(cl->m_ref_count, 1);  // otherwise there is a leftover reference somewhere
+            }
+            m_clauses[l].reset();
+        }
         for (unsigned l = m_constraints.size(); l-- > lvl; ) {
-            for (constraint* c : m_constraints[l]) {
+            for (auto const& c : m_constraints[l]) {
                 LOG_V("Removing constraint: " << show_deref(c));
-                erase_bv2c(c->bvar());
+                SASSERT_EQ(c->m_ref_count, 1);  // otherwise there is a leftover reference somewhere
                 if (c->dep() && c->dep()->is_leaf()) {
                     unsigned dep = c->dep()->leaf_value();
                     SASSERT(m_external_constraints.contains(dep));
@@ -57,6 +77,12 @@ namespace polysat {
         }
     }
 
+    constraint_manager::~constraint_manager() {
+        // Release explicitly to check for leftover references in debug mode,
+        // and to make sure all constraints are destructed before the bvar->constraint mapping.
+        release_level(0);
+    }
+
     constraint* constraint_manager::lookup(sat::bool_var var) const {
         return get_bv2c(var);
     }
@@ -85,19 +111,19 @@ namespace polysat {
         return *dynamic_cast<var_constraint const*>(this);
     }
 
-    scoped_ptr<constraint> constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) {
         return alloc(eq_constraint, *this, lvl, sign, p, d);
     }
 
-    scoped_ptr<constraint> constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) {
         return alloc(var_constraint, *this, lvl, sign, v, b, d);
     }
 
-    scoped_ptr<constraint> constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
         return alloc(ule_constraint, *this, lvl, sign, a, b, d);
     }
 
-    scoped_ptr<constraint> constraint_manager::ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
         // a < b  <=>  !(b <= a)
         return ule(lvl, static_cast<csign_t>(!sign), b, a, d);
     }
@@ -118,12 +144,12 @@ namespace polysat {
     //
     // Argument: flipping the msb swaps the negative and non-negative blocks
     //
-    scoped_ptr<constraint> constraint_manager::sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
         auto shift = rational::power_of_two(a.power_of_2() - 1);
         return ule(lvl, sign, a + shift, b + shift, d);
     }
 
-    scoped_ptr<constraint> constraint_manager::slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
+    constraint_ref constraint_manager::slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d) {
         auto shift = rational::power_of_two(a.power_of_2() - 1);
         return ult(lvl, sign, a + shift, b + shift, d);
     }
@@ -156,8 +182,19 @@ namespace polysat {
         narrow(s);
     }
 
-    clause* clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals) {
-        return alloc(clause, lvl, d, literals);
+    clause_ref clause::from_unit(constraint_ref c) {
+        SASSERT(c);
+        unsigned const lvl = c->level();
+        auto const& dep = c->m_dep;
+        sat::literal_vector lits;
+        lits.push_back(sat::literal(c->bvar()));
+        constraint_ref_vector cs;
+        cs.push_back(std::move(c));
+        return clause::from_literals(lvl, dep, std::move(lits), std::move(cs));
+    }
+
+    clause_ref clause::from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector constraints) {
+        return alloc(clause, lvl, d, literals, constraints);
     }
 
     bool clause::is_always_false(solver& s) const {
@@ -173,6 +210,31 @@ namespace polysat {
             return c->is_currently_false(s);
         });
     }
+
+    bool clause::resolve(sat::bool_var var, clause const& other) {
+        DEBUG_CODE({
+            bool this_has_pos = std::count(begin(), end(), sat::literal(var)) > 0;
+            bool this_has_neg = std::count(begin(), end(), ~sat::literal(var)) > 0;
+            bool other_has_pos = std::count(other.begin(), other.end(), sat::literal(var)) > 0;
+            bool other_has_neg = std::count(other.begin(), other.end(), ~sat::literal(var)) > 0;
+            SASSERT(!this_has_pos || !this_has_neg);  // otherwise this is tautology
+            SASSERT(!other_has_pos || !other_has_neg);  // otherwise other is tautology
+            SASSERT((this_has_pos && other_has_neg) || (this_has_neg && other_has_pos));
+        });
+        // The resolved var should not be one of the new constraints
+        SASSERT(std::all_of(new_constraints().begin(), new_constraints().end(), [var](constraint* c) { return c->bvar() != var; }));
+        SASSERT(std::all_of(other.new_constraints().begin(), other.new_constraints().end(), [var](constraint* c) { return c->bvar() != var; }));
+        int j = 0;
+        for (int i = 0; i < m_literals.size(); ++i)
+            if (m_literals[i].var() != var)
+                m_literals[j++] = m_literals[i];
+        m_literals.shrink(j);
+        for (sat::literal lit : other.literals())
+            if (lit.var() != var)
+                m_literals.push_back(lit);
+        return true;
+    }
+
     std::ostream& clause::display(std::ostream& out) const {
         bool first = true;
         for (auto lit : literals()) {
@@ -185,31 +247,16 @@ namespace polysat {
         return out;
     }
 
-    scoped_clause::scoped_clause(scoped_ptr<constraint>&& c) {
-        SASSERT(c);
-        sat::literal_vector lits;
-        lits.push_back(sat::literal(c->bvar()));
-        m_clause = clause::from_literals(c->level(), c->m_dep, lits);
-        m_owned.push_back(c.detach());
-    }
-
-    std::ostream& scoped_clause::display(std::ostream& out) const {
-        if (m_clause)
-            return out << *m_clause;
-        else
-            return out << "<NULL>";
-    }
-
     std::ostream& constraints_and_clauses::display(std::ostream& out) const {
         bool first = true;
-        for (auto* c : units()) {
+        for (auto c : units()) {
             if (first)
                 first = false;
             else
                 out << "  ;  ";
             out << show_deref(c);
         }
-        for (auto* cl : clauses()) {
+        for (auto cl : clauses()) {
             if (first)
                 first = false;
             else
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index e5b88e6fc..d93795447 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -15,7 +15,10 @@ Author:
 #include "math/polysat/boolean.h"
 #include "math/polysat/types.h"
 #include "math/polysat/interval.h"
+#include "math/polysat/log.h"
 #include "util/map.h"
+#include "util/ref.h"
+#include "util/ref_vector.h"
 
 namespace polysat {
 
@@ -23,11 +26,16 @@ namespace polysat {
     enum csign_t : bool { neg_t = false, pos_t = true };
 
     class constraint;
+    class constraint_manager;
     class clause;
     class scoped_clause;
     class eq_constraint;
     class var_constraint;
     class ule_constraint;
+    using constraint_ref = ref<constraint>;
+    using constraint_ref_vector = sref_vector<constraint>;
+    using clause_ref = ref<clause>;
+    using clause_ref_vector = sref_vector<clause>;
 
     // Manage constraint lifetime, deduplication, and connection to boolean variables/literals.
     class constraint_manager {
@@ -35,15 +43,16 @@ namespace polysat {
 
         bool_var_manager& m_bvars;
 
-        // Constraint storage per level
-        vector<scoped_ptr_vector<constraint>> m_constraints;
-
         // Association to boolean variables
         ptr_vector<constraint>   m_bv2constraint;
-        void insert_bv2c(sat::bool_var bv, constraint* c) { m_bv2constraint.setx(bv, c, nullptr); }
-        void erase_bv2c(sat::bool_var bv) { m_bv2constraint[bv] = nullptr; }
+        void insert_bv2c(sat::bool_var bv, constraint* c) { /* NOTE: will be called with incompletely constructed c! */ m_bv2constraint.setx(bv, c, nullptr); }
+        void erase_bv2c(sat::bool_var bv) {  m_bv2constraint[bv] = nullptr; }
         constraint* get_bv2c(sat::bool_var bv) const { return m_bv2constraint.get(bv, nullptr); }
 
+        // Constraint storage per level; should be destructed before m_bv2constraint
+        vector<vector<constraint_ref>> m_constraints;
+        vector<vector<clause_ref>> m_clauses;
+
         // Association to external dependency values (i.e., external names for constraints)
         u_map<constraint*> m_external_constraints;
 
@@ -51,9 +60,12 @@ namespace polysat {
 
     public:
         constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
+        ~constraint_manager();
 
         // Start managing lifetime of the given constraint
-        constraint* insert(scoped_ptr<constraint>&& c);
+        // TODO: rename to "store", or "keep"... because the bvar->constraint mapping is already inserted at creation.
+        constraint* insert(constraint_ref c);
+        clause* insert(clause_ref cl);
 
         // Release constraints at the given level and above.
         void release_level(unsigned lvl);
@@ -61,12 +73,12 @@ namespace polysat {
         constraint* lookup(sat::bool_var var) const;
         constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); }
 
-        scoped_ptr<constraint> eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d);
-        scoped_ptr<constraint> viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d);
-        scoped_ptr<constraint> ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
-        scoped_ptr<constraint> ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
-        scoped_ptr<constraint> sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
-        scoped_ptr<constraint> slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
+        constraint_ref eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d);
+        constraint_ref viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d);
+        constraint_ref ule(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
+        constraint_ref ult(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
+        constraint_ref sle(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
+        constraint_ref slt(unsigned lvl, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref const& d);
     };
 
     class constraint {
@@ -76,7 +88,10 @@ namespace polysat {
         friend class var_constraint;
         friend class eq_constraint;
         friend class ule_constraint;
+
         constraint_manager* m_manager;
+        unsigned         m_ref_count = 0;
+        // bool             m_stored = false;  ///< Whether it has been inserted into the constraint_manager to be tracked by level
         unsigned         m_storage_level;  ///< Controls lifetime of the constraint object. Always a base level (for external dependencies the level at which it was created, and for others the maximum storage level of its external dependencies).
         unsigned         m_active_level;  ///< Level at which the constraint was activated. Possibly different from m_storage_level because constraints in lemmas may become activated only at a higher level.
         ckind_t          m_kind;
@@ -85,10 +100,23 @@ namespace polysat {
         sat::bool_var    m_bvar;  ///< boolean variable associated to this constraint; convention: a constraint itself always represents the positive sat::literal
         csign_t          m_sign;  ///< sign/polarity
         lbool            m_status = l_undef;  ///< current constraint status, computed from value of m_lit and m_sign
+        lbool            m_bvalue = l_undef;  ///< TODO: remove m_sign and m_bvalue, use m_status as current value. the constraint itself is always the positive literal. use unit clauses for unit/external constraints; negation may come in through there.
+
         constraint(constraint_manager& m, unsigned lvl, csign_t sign, p_dependency_ref const& dep, ckind_t k):
-            m_manager(&m), m_storage_level(lvl), m_kind(k), m_dep(dep), m_bvar(m_manager->m_bvars.new_var()), m_sign(sign) {}
+            m_manager(&m), m_storage_level(lvl), m_kind(k), m_dep(dep), m_bvar(m_manager->m_bvars.new_var()), m_sign(sign) {
+            SASSERT_EQ(m_manager->get_bv2c(bvar()), nullptr);
+            m_manager->insert_bv2c(bvar(), this);
+        }
+
     public:
-        virtual ~constraint() { m_manager->m_bvars.del_var(m_bvar); }
+        void inc_ref() { m_ref_count++; }
+        void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
+        virtual ~constraint() {
+            SASSERT_EQ(m_manager->get_bv2c(bvar()), this);
+            m_manager->erase_bv2c(bvar());
+            m_manager->m_bvars.del_var(m_bvar);
+        }
+
         bool is_eq() const { return m_kind == ckind_t::eq_t; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
         bool is_bit() const { return m_kind == ckind_t::bit_t; }
@@ -96,7 +124,6 @@ namespace polysat {
         virtual std::ostream& display(std::ostream& out) const = 0;
         bool propagate(solver& s, pvar v);
         virtual void propagate_core(solver& s, pvar v, pvar other_v);
-        virtual scoped_ptr<constraint> resolve(solver& s, pvar v) = 0;
         virtual bool is_always_false() = 0;
         virtual bool is_currently_false(solver& s) = 0;
         virtual bool is_currently_true(solver& s) = 0;
@@ -112,34 +139,45 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_vars; }
         unsigned level() const { return m_storage_level; }
         sat::bool_var bvar() const { return m_bvar; }
+        sat::literal blit() const { SASSERT(m_bvalue != l_undef); return m_bvalue == l_true ? sat::literal(m_bvar) : ~sat::literal(m_bvar); }
         bool sign() const { return m_sign; }
         void assign(bool is_true) {
+            SASSERT(m_bvalue == l_undef || m_bvalue == to_lbool(is_true));
+            m_bvalue = to_lbool(is_true);
             lbool new_status = (is_true ^ !m_sign) ? l_true : l_false;
             SASSERT(is_undef() || new_status == m_status);
             m_status = new_status;
         }
-        void unassign() { m_status = l_undef; }
+        void unassign() { m_status = l_undef; m_bvalue = l_undef; }
         bool is_undef() const { return m_status == l_undef; }
         bool is_positive() const { return m_status == l_true; }
         bool is_negative() const { return m_status == l_false; }
 
+        // TODO: must return a 'clause_ref' instead. If we resolve with a non-base constraint, we need to keep it in the clause (or should we track those as dependencies? the level needs to be higher then.)
+        virtual constraint_ref resolve(solver& s, pvar v) = 0;
+
         /** Precondition: all variables other than v are assigned.
          *
          * \param[out] out_interval     The forbidden interval for this constraint
          * \param[out] out_neg_cond     Negation of the side condition (the side condition is true when the forbidden interval is trivial). May be NULL if the condition is constant.
          * \returns True iff a forbidden interval exists and the output parameters were set.
          */
-        virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr<constraint>& out_neg_cond) { return false; }
+        virtual bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) { return false; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
 
     // Disjunction of constraints represented by boolean literals
     class clause {
+        friend class constraint_manager;
+
+        unsigned m_ref_count = 0;
         unsigned m_level;
-        unsigned m_next_guess = UINT_MAX;  // next guess for enumerative backtracking
+        // unsigned m_next_guess = UINT_MAX;  // next guess for enumerative backtracking
+        unsigned m_next_guess = 0;  // next guess for enumerative backtracking
         p_dependency_ref m_dep;
         sat::literal_vector m_literals;
+        constraint_ref_vector m_new_constraints;  // new constraints, temporarily owned by this clause
 
         /* TODO: embed literals to save an indirection?
         unsigned m_num_literals;
@@ -150,23 +188,27 @@ namespace polysat {
         }
         */
 
-        clause(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals):
-            m_level(lvl), m_dep(d), m_literals(literals)
+        clause(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints):
+            m_level(lvl), m_dep(d), m_literals(std::move(literals)), m_new_constraints(std::move(new_constraints))
         {
-            SASSERT(std::all_of(m_literals.begin(), m_literals.end(), [this](sat::literal l) { return l != sat::null_literal; }));
+            SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
         }
 
     public:
-        // static clause* unit(constraint* c);
-        static clause* from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector const& literals);
+        void inc_ref() { m_ref_count++; }
+        void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (!m_ref_count) dealloc(this); }
+
+        static clause_ref from_unit(constraint_ref c);
+        static clause_ref from_literals(unsigned lvl, p_dependency_ref const& d, sat::literal_vector literals, constraint_ref_vector new_constraints);
 
         // Resolve with 'other' upon 'var'.
-        bool resolve(sat::bool_var var, clause const* other);
+        bool resolve(sat::bool_var var, clause const& other);
 
         sat::literal_vector const& literals() const { return m_literals; }
         p_dependency* dep() const { return m_dep; }
         unsigned level() const { return m_level; }
 
+        constraint_ref_vector const& new_constraints() const { return m_new_constraints; }
         bool empty() const { return m_literals.empty(); }
         unsigned size() const { return m_literals.size(); }
         sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
@@ -188,55 +230,17 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }
 
-    // A clause that owns (some of) the constraints represented by its literals.
-    class scoped_clause {
-        scoped_ptr<clause> m_clause;
-        scoped_ptr_vector<constraint> m_owned;
-
-    public:
-        scoped_clause() {}
-        scoped_clause(std::nullptr_t) {}
-
-        scoped_clause(scoped_ptr<constraint>&& c);
-
-        scoped_clause(scoped_ptr<clause>&& clause, scoped_ptr_vector<constraint>&& owned_literals):
-            m_clause(std::move(clause)), m_owned(std::move(owned_literals)) {}
-
-        operator bool() const { return m_clause; }
-
-        bool is_owned_unit() const { return m_clause && m_clause->size() == 1 && m_owned.size() == 1; }
-
-        bool empty() const { SASSERT(m_clause); return m_clause->empty(); }
-        unsigned size() const { SASSERT(m_clause); return m_clause->size(); }
-        sat::literal operator[](unsigned idx) const { SASSERT(m_clause); return (*m_clause)[idx]; }
-
-        bool is_always_false(solver& s) const { return m_clause->is_always_false(s); }
-        bool is_currently_false(solver& s) const { return m_clause->is_currently_false(s); }
-
-        clause* get() { return m_clause.get(); }
-        clause* detach() { SASSERT(m_owned.empty()); return m_clause.detach(); }
-        ptr_vector<constraint> detach_constraints() { return m_owned.detach(); }
-
-        using const_iterator = typename clause::const_iterator;
-        const_iterator begin() const { SASSERT(m_clause); return m_clause->begin(); }
-        const_iterator end() const { SASSERT(m_clause); return m_clause->end(); }
-
-        std::ostream& display(std::ostream& out) const;
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, scoped_clause const& c) { return c.display(out); }
-
     // Container for unit constraints and clauses.
     class constraints_and_clauses {
-        ptr_vector<constraint> m_units;
-        ptr_vector<clause> m_clauses;
+        constraint_ref_vector m_units;
+        clause_ref_vector m_clauses;
 
     public:
-        ptr_vector<constraint> const& units() const { return m_units; }
-        ptr_vector<constraint>& units() { return m_units; }
+        constraint_ref_vector const& units() const { return m_units; }
+        constraint_ref_vector& units() { return m_units; }
 
-        ptr_vector<clause> const& clauses() const { return m_clauses; }
-        ptr_vector<clause>& clauses() { return m_clauses; }
+        clause_ref_vector const& clauses() const { return m_clauses; }
+        clause_ref_vector& clauses() { return m_clauses; }
 
         bool is_unit() const { return units().size() == 1 && clauses().empty(); }
         constraint* get_unit() const { SASSERT(is_unit()); return units()[0]; }
@@ -258,19 +262,20 @@ namespace polysat {
         }
 
         void append(ptr_vector<constraint> const& cs) {
-            m_units.append(cs);
+            for (constraint* c : cs)
+                m_units.push_back(c);
         }
 
         void push_back(std::nullptr_t) { m_units.push_back(nullptr); }
-        void push_back(constraint* c) { m_units.push_back(c); }
-        void push_back(clause* cl) { m_clauses.push_back(cl); }
+        void push_back(constraint_ref c) { m_units.push_back(std::move(c)); }
+        void push_back(clause_ref cl) { m_clauses.push_back(std::move(cl)); }
 
         // TODO: use iterator instead
         unsigned_vector vars(constraint_manager const& cm) const {
             unsigned_vector vars;
-            for (constraint* c : m_units)
+            for (auto const& c : m_units)
                 vars.append(c->vars());
-            for (clause* cl : m_clauses)
+            for (auto const& cl : m_clauses)
                 for (auto lit : *cl) {
                     constraint* c = cm.lookup(lit.var());
                     if (c)
diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp
index 45122d0b5..d946d1262 100644
--- a/src/math/polysat/eq_constraint.cpp
+++ b/src/math/polysat/eq_constraint.cpp
@@ -19,13 +19,13 @@ Author:
 namespace polysat {
 
     std::ostream& eq_constraint::display(std::ostream& out) const {
-        out << p() << (sign() == pos_t ? " == 0" : " != 0") << " @" << level();
+        out << p() << (sign() == pos_t ? " == 0" : " != 0") << " @" << level() << " b" << bvar();
         if (is_undef())
             out << " [inactive]";
         return out;
     }
 
-    scoped_ptr<constraint> eq_constraint::resolve(solver& s, pvar v) {
+    constraint_ref eq_constraint::resolve(solver& s, pvar v) {
         if (is_positive())
             return eq_resolve(s, v);
         if (is_negative())
@@ -115,7 +115,7 @@ namespace polysat {
      * Equality constraints
      */
 
-    scoped_ptr<constraint> eq_constraint::eq_resolve(solver& s, pvar v) {
+    constraint_ref eq_constraint::eq_resolve(solver& s, pvar v) {
         LOG("Resolve " << *this << " upon v" << v);
         if (s.m_conflict.size() != 1)
             return nullptr;
@@ -147,7 +147,7 @@ namespace polysat {
      * Disequality constraints
      */
 
-    scoped_ptr<constraint> eq_constraint::diseq_resolve(solver& s, pvar v) {
+    constraint_ref eq_constraint::diseq_resolve(solver& s, pvar v) {
         NOT_IMPLEMENTED_YET();
         return nullptr;
     }
@@ -155,7 +155,7 @@ namespace polysat {
 
 
     /// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality)
-    bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr<constraint>& out_neg_cond)
+    bool eq_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond)
     {
         SASSERT(!is_undef());
 
diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h
index 953aa330e..848df0904 100644
--- a/src/math/polysat/eq_constraint.h
+++ b/src/math/polysat/eq_constraint.h
@@ -27,16 +27,16 @@ namespace polysat {
         ~eq_constraint() override {}
         pdd const & p() const { return m_poly; }
         std::ostream& display(std::ostream& out) const override;
-        scoped_ptr<constraint> resolve(solver& s, pvar v) override;
+        constraint_ref resolve(solver& s, pvar v) override;
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
         bool is_currently_true(solver& s) override;
         void narrow(solver& s) override;
-        bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr<constraint>& out_neg_cond) override;
+        bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) override;
 
     private:
-        scoped_ptr<constraint> eq_resolve(solver& s, pvar v);
-        scoped_ptr<constraint> diseq_resolve(solver& s, pvar v);
+        constraint_ref eq_resolve(solver& s, pvar v);
+        constraint_ref diseq_resolve(solver& s, pvar v);
     };
 
 }
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index d171eb001..38e672088 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -20,7 +20,7 @@ namespace polysat {
 
     struct fi_record {
         eval_interval interval;
-        scoped_ptr<constraint> neg_cond;  // could be multiple constraints later
+        constraint_ref neg_cond;  // could be multiple constraints later
         constraint* src;
     };
 
@@ -62,7 +62,7 @@ namespace polysat {
         return true;
     }
 
-    bool forbidden_intervals::explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, scoped_clause& out_lemma) {
+    bool forbidden_intervals::explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma) {
 
         // Extract forbidden intervals from conflicting constraints
         vector<fi_record> records;
@@ -72,7 +72,7 @@ namespace polysat {
         for (constraint* c : conflict) {
             LOG_H3("Computing forbidden interval for: " << *c);
             eval_interval interval = eval_interval::full();
-            scoped_ptr<constraint> neg_cond;
+            constraint_ref neg_cond;
             if (c->forbidden_interval(s, v, interval, neg_cond)) {
                 LOG("interval: " << interval);
                 LOG("neg_cond: " << show_deref(neg_cond));
@@ -100,15 +100,15 @@ namespace polysat {
             auto& full_record = records.back();
             SASSERT(full_record.interval.is_full());
             sat::literal_vector literals;
-            scoped_ptr_vector<constraint> new_constraints;
-            literals.push_back(~sat::literal(full_record.src->bvar()));  // TODO: only do this if it's not a base-level constraint! (from unit clauses, e.g., external constraints)
+            constraint_ref_vector new_constraints;
+            literals.push_back(~full_record.src->blit());  // TODO: only do this if it's not a base-level constraint! (from unit clauses, e.g., external constraints)
             if (full_record.neg_cond) {
                 literals.push_back(sat::literal(full_record.neg_cond.get()->bvar()));
-                new_constraints.push_back(full_record.neg_cond.detach());
+                new_constraints.push_back(std::move(full_record.neg_cond));
             }
             unsigned lemma_lvl = full_record.src->level();
             p_dependency_ref lemma_dep(full_record.src->dep(), s.m_dm);
-            out_lemma = scoped_clause(clause::from_literals(lemma_lvl, lemma_dep, literals), std::move(new_constraints));
+            out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints));
             return true;
         }
 
@@ -146,12 +146,12 @@ namespace polysat {
         // We learn the negation of this conjunction.
 
         sat::literal_vector literals;
-        scoped_ptr_vector<constraint> new_constraints;
+        constraint_ref_vector new_constraints;
         // Add negation of src constraints as antecedents (may be resolved during backtracking)
         for (unsigned const i : seq) {
             // TODO: don't add base-level constraints! (from unit clauses, e.g., external constraints)
             //       (maybe extract that into a helper function on 'clause'... it could sort out base-level and other constraints; add the first to lemma_dep and the other to antecedents)
-            sat::literal src_lit{records[i].src->bvar()};
+            sat::literal src_lit = records[i].src->blit();
             literals.push_back(~src_lit);
         }
         // Add side conditions and interval constraints
@@ -165,20 +165,19 @@ namespace polysat {
             auto const& next_hi = records[next_i].interval.hi();
             auto const& lhs = hi - next_lo;
             auto const& rhs = next_hi - next_lo;
-            scoped_ptr<constraint> c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency));
+            constraint_ref c = s.m_constraints.ult(lemma_lvl, neg_t, lhs, rhs, s.mk_dep_ref(null_dependency));
             LOG("constraint: " << *c);
             literals.push_back(sat::literal(c->bvar()));
-            new_constraints.push_back(c.detach());
+            new_constraints.push_back(std::move(c));
             // Side conditions
             // TODO: check whether the condition is subsumed by c?  maybe at the end do a "lemma reduction" step, to try and reduce branching?
-            scoped_ptr<constraint>& neg_cond = records[i].neg_cond;
+            constraint_ref& neg_cond = records[i].neg_cond;
             if (neg_cond) {
                 literals.push_back(sat::literal(neg_cond->bvar()));
-                new_constraints.push_back(neg_cond.detach());
+                new_constraints.push_back(std::move(neg_cond));
             }
         }
-        scoped_ptr<clause> cl = clause::from_literals(lemma_lvl, lemma_dep, literals);
-        out_lemma = scoped_clause(std::move(cl), std::move(new_constraints));
+        out_lemma = clause::from_literals(lemma_lvl, lemma_dep, std::move(literals), std::move(new_constraints));
         return true;
     }
 
diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h
index 6e733b47f..b36fdcb08 100644
--- a/src/math/polysat/forbidden_intervals.h
+++ b/src/math/polysat/forbidden_intervals.h
@@ -23,7 +23,7 @@ namespace polysat {
     class forbidden_intervals {
 
     public:
-        static bool explain(solver& s, ptr_vector<constraint> const& conflict, pvar v, scoped_clause& out_lemma);
+        static bool explain(solver& s, constraint_ref_vector const& conflict, pvar v, clause_ref& out_lemma);
 
     };
 }
diff --git a/src/math/polysat/log.cpp b/src/math/polysat/log.cpp
index 145a71b80..e41c99063 100644
--- a/src/math/polysat/log.cpp
+++ b/src/math/polysat/log.cpp
@@ -27,27 +27,18 @@ get_max_log_level(std::string const& fn, std::string const& pretty_fn)
   (void)fn;
   (void)pretty_fn;
 
-  // bool const from_decision_queue = pretty_fn.find("DecisionQueue") != std::string::npos;
-  // if (from_decision_queue) {
-  //   return LogLevel::Info;
-  // }
+  if (fn == "push_cjust")
+    return LogLevel::Verbose;
 
-  // if (pretty_fn.find("add_") != std::string::npos) {
-  //   return LogLevel::Info;
-  // }
+  // if (fn == "pop_levels")
+  //   return LogLevel::Default;
 
-  // if (fn == "analyze") {
-  //   return LogLevel::Trace;
-  // }
-  // if (fn.find("minimize") != std::string::npos) {
-  //   return LogLevel::Trace;
-  // }
-  // if (fn == "propagate_literal") {
-  //     return LogLevel::Trace;
-  // }
+  // also covers 'reset_marks' and 'set_marks'
+  if (fn.find("set_mark") != std::string::npos)
+    return LogLevel::Default;
 
   return LogLevel::Verbose;
-  // return LogLevel::Warn;
+  return LogLevel::Default;
 }
 
 /// Filter log messages
diff --git a/src/math/polysat/log_helper.h b/src/math/polysat/log_helper.h
index dd316fdde..76ad7b99a 100644
--- a/src/math/polysat/log_helper.h
+++ b/src/math/polysat/log_helper.h
@@ -18,11 +18,13 @@ Author:
 #pragma once
 
 #include <iostream>
+#include <utility>
+#include "util/ref.h"
 #include "util/util.h"
 
 template <typename T>
 struct show_deref_t {
-  T* ptr;
+  T const* ptr;
 };
 
 template <typename T>
@@ -38,7 +40,22 @@ show_deref_t<T> show_deref(T* ptr) {
   return show_deref_t<T>{ptr};
 }
 
-template <typename T>
-show_deref_t<T> show_deref(scoped_ptr<T> const& ptr) {
+// template <typename T>
+// show_deref_t<T> show_deref(ref<T> const& ptr) {
+//   return show_deref_t<T>{ptr.get()};
+// }
+
+// template <typename T>
+// show_deref_t<T> show_deref(scoped_ptr<T> const& ptr) {
+//   return show_deref_t<T>{ptr.get()};
+// }
+
+// template <typename Ptr, typename T = decltype(&*std::declval<Ptr>())>
+// show_deref_t<T> show_deref(Ptr const& ptr) {
+//   return show_deref_t<T>{&*ptr};
+// }
+
+template <typename Ptr, typename T = typename std::remove_pointer<decltype(std::declval<Ptr>().get())>::type>
+show_deref_t<T> show_deref(Ptr const& ptr) {
   return show_deref_t<T>{ptr.get()};
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index eb6630ac7..85de2b31d 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -20,6 +20,9 @@ Author:
 #include "math/polysat/log.h"
 #include "math/polysat/forbidden_intervals.h"
 
+// For development; to be removed once the linear solver works well enough
+#define ENABLE_LINEAR_SOLVER 0
+
 namespace polysat {
 
     
@@ -76,7 +79,10 @@ namespace polysat {
         m_constraints(m_bvars) {
     }
 
-    solver::~solver() {}
+    solver::~solver() {
+        // Need to remove any lingering clause/constraint references before the constraint manager is destructed
+        m_conflict.reset();
+    }
 
 #if POLYSAT_LOGGING_ENABLED
     void solver::log_viable(pvar v) {
@@ -155,11 +161,11 @@ namespace polysat {
         m_free_vars.del_var_eh(v);
     }
 
-    scoped_ptr<constraint> solver::mk_eq(pdd const& p, unsigned dep) {
+    constraint_ref solver::mk_eq(pdd const& p, unsigned dep) {
         return m_constraints.eq(m_level, pos_t, p, mk_dep_ref(dep));
     }
 
-    scoped_ptr<constraint> solver::mk_diseq(pdd const& p, unsigned dep) {
+    constraint_ref solver::mk_diseq(pdd const& p, unsigned dep) {
         if (p.is_val()) {
             // if (!p.is_zero())
             //     return nullptr;  // TODO: probably better to create a dummy always-true constraint?
@@ -175,48 +181,38 @@ namespace polysat {
         return m_constraints.viable(m_level, pos_t, slack, non_zero, mk_dep_ref(dep));
     }
 
-    scoped_ptr<constraint> solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) {
+    constraint_ref solver::mk_ule(pdd const& p, pdd const& q, unsigned dep) {
         return m_constraints.ule(m_level, pos_t, p, q, mk_dep_ref(dep));
     }
 
-    scoped_ptr<constraint> solver::mk_ult(pdd const& p, pdd const& q, unsigned dep) {
+    constraint_ref solver::mk_ult(pdd const& p, pdd const& q, unsigned dep) {
         return m_constraints.ult(m_level, pos_t, p, q, mk_dep_ref(dep));
     }
 
-    scoped_ptr<constraint> solver::mk_sle(pdd const& p, pdd const& q, unsigned dep) {
+    constraint_ref solver::mk_sle(pdd const& p, pdd const& q, unsigned dep) {
         return m_constraints.sle(m_level, pos_t, p, q, mk_dep_ref(dep));
     }
 
-    scoped_ptr<constraint> solver::mk_slt(pdd const& p, pdd const& q, unsigned dep) {
+    constraint_ref solver::mk_slt(pdd const& p, pdd const& q, unsigned dep) {
         return m_constraints.slt(m_level, pos_t, p, q, mk_dep_ref(dep));
     }
 
-    void solver::new_constraint(scoped_ptr<constraint>&& sc, bool activate) {
-        SASSERT(sc);
-        SASSERT(activate || sc->dep());  // if we don't activate the constraint, we need the dependency to access it again later.
-        constraint* c = m_constraints.insert(std::move(sc));
+    void solver::new_constraint(constraint_ref cr, bool activate) {
+        VERIFY(at_base_level());
+        SASSERT(cr);
+        SASSERT(activate || cr->dep());  // if we don't activate the constraint, we need the dependency to access it again later.
+        constraint* c = m_constraints.insert(std::move(cr));
         LOG("New constraint: " << *c);
         m_original.push_back(c);
+#if ENABLE_LINEAR_SOLVER
         m_linear_solver.new_constraint(*c);
+#endif
         if (activate && !is_conflict())
             activate_constraint_base(c);
     }
 
-    void solver::new_eq(pdd const& p, unsigned dep)                 { new_constraint(mk_eq(p, dep), false); }
-    void solver::new_diseq(pdd const& p, unsigned dep)              { new_constraint(mk_diseq(p, dep), false); }
-    void solver::new_ule(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_ule(p, q, dep), false); }
-    void solver::new_ult(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_ult(p, q, dep), false); }
-    void solver::new_sle(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_sle(p, q, dep), false); }
-    void solver::new_slt(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_slt(p, q, dep), false); }
-
-    void solver::add_eq(pdd const& p, unsigned dep)                 { new_constraint(mk_eq(p, dep), true); }
-    void solver::add_diseq(pdd const& p, unsigned dep)              { new_constraint(mk_diseq(p, dep), true); }
-    void solver::add_ule(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_ule(p, q, dep), true); }
-    void solver::add_ult(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_ult(p, q, dep), true); }
-    void solver::add_sle(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_sle(p, q, dep), true); }
-    void solver::add_slt(pdd const& p, pdd const& q, unsigned dep)  { new_constraint(mk_slt(p, q, dep), true); }
-
     void solver::assign_eh(unsigned dep, bool is_true) {
+        VERIFY(at_base_level());
         constraint* c = m_constraints.lookup_external(dep);
         if (!c) {
             LOG("WARN: there is no constraint for dependency " << dep);
@@ -246,6 +242,7 @@ namespace polysat {
     }
 
     void solver::linear_propagate() {
+#if ENABLE_LINEAR_SOLVER
         switch (m_linear_solver.check()) {
         case l_false:
             // TODO extract conflict
@@ -253,6 +250,7 @@ namespace polysat {
         default:
             break;
         }
+#endif
     }
 
     void solver::propagate(sat::literal lit) {
@@ -260,7 +258,6 @@ namespace polysat {
         constraint* c = m_constraints.lookup(lit.var());
         SASSERT(c);
         SASSERT(!c->is_undef());
-        SASSERT(c->is_positive() == !lit.sign());
         // c->narrow(*this);
     }
 
@@ -289,14 +286,18 @@ namespace polysat {
     void solver::push_level() {
         ++m_level;
         m_trail.push_back(trail_instr_t::inc_level_i);
+#if ENABLE_LINEAR_SOLVER
         m_linear_solver.push();
+#endif
     }
 
     void solver::pop_levels(unsigned num_levels) {
         SASSERT(m_level >= num_levels);
         unsigned const target_level = m_level - num_levels;
         LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
+#if ENABLE_LINEAR_SOLVER
         m_linear_solver.pop(num_levels);
+#endif
         while (num_levels > 0) {
             switch (m_trail.back()) {
             case trail_instr_t::qhead_i: {
@@ -412,6 +413,7 @@ namespace polysat {
             // NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing)
             //       (fail here in debug mode so we notice if we miss some)
             DEBUG_CODE( UNREACHABLE(); );
+            m_free_vars.unassign_var_eh(v);
             set_conflict(v);
             break;
         case dd::find_t::singleton:
@@ -437,7 +439,9 @@ namespace polysat {
         m_search.push_assignment(v, val);
         m_trail.push_back(trail_instr_t::assign_i);
         m_justification[v] = j; 
+#if ENABLE_LINEAR_SOLVER
         m_linear_solver.set_value(v, val);
+#endif
     }
 
     void solver::set_conflict(constraint& c) { 
@@ -455,6 +459,7 @@ namespace polysat {
     }
 
     void solver::set_marks(constraint const& c) {
+        LOG_V("Marking in: " << c);
         if (c.bvar() != sat::null_bool_var)
             m_bvars.set_mark(c.bvar());
         for (auto v : c.vars())
@@ -462,6 +467,7 @@ namespace polysat {
     }
 
     void solver::set_marks(clause const& cl) {
+        LOG_V("Marking in: " << cl);
         for (auto lit : cl)
             set_marks(*m_constraints.lookup(lit.var()));
     }
@@ -502,7 +508,7 @@ namespace polysat {
         }
 
         pvar conflict_var = null_var;
-        scoped_clause lemma;
+        clause_ref lemma;
         for (auto v : m_conflict.vars(m_constraints))
             if (!has_viable(v)) {
                 SASSERT(conflict_var == null_var || conflict_var == v);  // at most one variable can be empty
@@ -514,7 +520,7 @@ namespace polysat {
 
         if (m_conflict.clauses().empty() && conflict_var != null_var) {
             LOG_H2("Conflict due to empty viable set for pvar " << conflict_var);
-            scoped_clause new_lemma;
+            clause_ref new_lemma;
             if (forbidden_intervals::explain(*this, m_conflict.units(), conflict_var, new_lemma)) {
                 SASSERT(new_lemma);
                 clause& cl = *new_lemma.get();
@@ -528,7 +534,7 @@ namespace polysat {
                 SASSERT(cl.size() > 0);
                 lemma = std::move(new_lemma);
                 m_conflict.reset();
-                m_conflict.push_back(lemma.get());
+                m_conflict.push_back(lemma);
                 reset_marks();
                 m_bvars.reset_marks();
                 set_marks(*lemma.get());
@@ -554,12 +560,12 @@ namespace polysat {
                     return;
                 }
                 SASSERT(j.is_propagation());
-                scoped_clause new_lemma = resolve(v);
+                clause_ref new_lemma = resolve(v);
                 if (!new_lemma) {
                     backtrack(i, lemma);
                     return;
                 }
-                if (new_lemma.is_always_false(*this)) {
+                if (new_lemma->is_always_false(*this)) {
                     clause* cl = new_lemma.get();
                     learn_lemma(v, std::move(new_lemma));
                     m_conflict.reset();
@@ -567,7 +573,7 @@ namespace polysat {
                     report_unsat();
                     return;
                 }
-                if (!new_lemma.is_currently_false(*this)) {
+                if (!new_lemma->is_currently_false(*this)) {
                     backtrack(i, lemma);
                     return;
                 }
@@ -591,19 +597,50 @@ namespace polysat {
                     return;
                 }
                 if (m_bvars.is_decision(var)) {
+                    // SASSERT(std::count(lemma->begin(), lemma->end(), ~lit) > 0);
                     revert_bool_decision(lit, lemma);
                     return;
                 }
                 SASSERT(m_bvars.is_propagation(var));
-                clause* other = m_bvars.reason(var);
-                // TODO: boolean resolution
-                NOT_IMPLEMENTED_YET();
+                clause_ref new_lemma = resolve_bool(lit);
+                SASSERT(new_lemma);
+                if (new_lemma->is_always_false(*this)) {
+                    // learn_lemma(v, new_lemma);
+                    m_conflict.reset();
+                    m_conflict.push_back(std::move(new_lemma));
+                    report_unsat();
+                    return;
+                }
+                if (!new_lemma->is_currently_false(*this)) {
+                    backtrack(i, lemma);
+                    return;
+                }
+                lemma = std::move(new_lemma);
+                reset_marks();
+                m_bvars.reset_marks();
+                set_marks(*lemma.get());
+                m_conflict.reset();
+                m_conflict.push_back(lemma.get());
             }
         }
         report_unsat();
     }
 
-    void solver::backtrack(unsigned i, scoped_clause& lemma) {
+    clause_ref solver::resolve_bool(sat::literal lit) {
+        if (m_conflict.size() != 1)
+            return nullptr;
+        if (m_conflict.clauses().size() != 1)
+            return nullptr;
+        clause* lemma = m_conflict.clauses()[0];
+        SASSERT(lemma);
+        SASSERT(m_bvars.is_propagation(lit.var()));
+        clause* other = m_bvars.reason(lit.var());
+        SASSERT(other);
+        VERIFY(lemma->resolve(lit.var(), *other));
+        return lemma;  // currently modified in-place
+    }
+
+    void solver::backtrack(unsigned i, clause_ref lemma) {
         do {
             auto const& item = m_search[i];
             if (item.is_assignment()) {
@@ -627,7 +664,7 @@ namespace polysat {
                         set_mark(w);
                     if (c->bvar() != sat::null_bool_var)
                         m_bvars.set_mark(c->bvar());
-                    m_conflict.units().push_back(c);
+                    m_conflict.push_back(c);
                 }
             }
             else {
@@ -639,9 +676,6 @@ namespace polysat {
                 SASSERT(m_bvars.is_assigned(var));
                 if (!m_bvars.is_marked(var))
                     continue;
-                // NOTE: currently, we should never reach this point (but check)
-                // UNREACHABLE();
-
                 if (m_bvars.level(var) <= base_level())
                     break;
                 if (m_bvars.is_decision(var)) {
@@ -649,13 +683,13 @@ namespace polysat {
                     return;
                 }
                 SASSERT(m_bvars.is_propagation(var));
-                // Note: here, bvar being marked need not mean it's part of the reason (could come from a cjust)
                 clause* other = m_bvars.reason(var);
-                NOT_IMPLEMENTED_YET();
+                set_marks(*other);
+                m_conflict.push_back(other);
             }
         }
         while (i-- > 0);
-        // TODO: learn lemma
+        add_lemma_clause(lemma);  // TODO: handle units correctly
         report_unsat();
     }
 
@@ -667,10 +701,10 @@ namespace polysat {
     void solver::unsat_core(unsigned_vector& deps) {
         deps.reset();
         p_dependency_ref conflict_dep(m_dm);
-        for (auto* c : m_conflict.units())
+        for (auto& c : m_conflict.units())
             if (c)
                 conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
-        for (auto* c : m_conflict.clauses())
+        for (auto& c : m_conflict.clauses())
             conflict_dep = m_dm.mk_join(c->dep(), conflict_dep);
         m_dm.linearize(conflict_dep, deps);
     }
@@ -682,22 +716,22 @@ namespace polysat {
      * We add 'p == 0' as a lemma. The lemma depends on the dependencies used
      * to derive p, and the level of the lemma is the maximal level of the dependencies.
      */
-    void solver::learn_lemma(pvar v, scoped_clause&& lemma) {
+    void solver::learn_lemma(pvar v, clause_ref lemma) {
         if (!lemma)
             return;
-        LOG("Learning: " << lemma);
+        LOG("Learning: " << show_deref(lemma));
         SASSERT(m_conflict_level <= m_justification[v].level());
-        if (lemma.is_owned_unit()) {
-            scoped_ptr<constraint> c = lemma.detach_constraints()[0];
-            SASSERT(lemma[0].var() == c->bvar());
-            SASSERT(!lemma[0].sign()); // that case is handled incorrectly atm
+        if (lemma->size() == 1) {
+            constraint_ref c = lemma->new_constraints()[0];  // TODO: probably wrong
+            SASSERT_EQ(lemma->literals()[0].var(), c->bvar());
+            SASSERT(!lemma->literals()[0].sign()); // that case is handled incorrectly atm
             learn_lemma_unit(v, std::move(c));
         }
         else
             learn_lemma_clause(v, std::move(lemma));
     }
 
-    void solver::learn_lemma_unit(pvar v, scoped_ptr<constraint>&& lemma) {
+    void solver::learn_lemma_unit(pvar v, constraint_ref lemma) {
         SASSERT(lemma);
         constraint* c = lemma.get();
         add_lemma_unit(std::move(lemma));
@@ -705,23 +739,82 @@ namespace polysat {
         activate_constraint_base(c);
     }
 
-    void solver::learn_lemma_clause(pvar v, scoped_clause&& lemma) {
+    void solver::learn_lemma_clause(pvar v, clause_ref lemma) {
         SASSERT(lemma);
-        clause& cl = *lemma.get();
-        add_lemma_clause(std::move(lemma));
-        // Guess one of the new literals
-        constraint* c = nullptr;
-        while (true) {
-            unsigned next_idx = cl.next_guess();
-            SASSERT(next_idx < cl.size()); // must succeed for at least one
-            sat::literal lit = cl[next_idx];
-            c = m_constraints.lookup(lit.var());
-            c->assign(!lit.sign());
-            if (!c->is_currently_false(*this))
-                break;
-        }
-        decide_bool(sat::literal(c->bvar()), &cl);
+        sat::literal lit = decide_bool(*lemma);
+        constraint* c = m_constraints.lookup(lit.var());
         push_cjust(v, c);
+        add_lemma_clause(std::move(lemma));
+    }
+
+    // Guess a literal from the given clause; returns the guessed constraint
+    sat::literal solver::decide_bool(clause& lemma) {
+        LOG_H3("Guessing literal in lemma: " << lemma);
+        IF_LOGGING({
+            for (pvar v = 0; v < m_viable.size(); ++v) {
+                log_viable(v);
+            }
+        });
+        LOG("Boolean assignment: " << m_bvars);
+
+        auto is_suitable = [this](sat::literal lit) -> bool {
+            if (m_bvars.value(lit) == l_false)  // already assigned => cannot decide on this (comes from either lemma LHS or previously decided literals that are now changed to propagation)
+                return false;
+            SASSERT(m_bvars.value(lit) != l_true);  // cannot happen in a valid lemma
+            constraint* c = m_constraints.lookup(lit.var());
+            c->assign(!lit.sign());
+            bool result = true;
+            if (c->is_currently_false(*this))
+                result = false;
+            c->unassign();
+            return result;
+        };
+
+        // constraint *choice = nullptr;
+        sat::literal choice = sat::null_literal;
+        unsigned num_choices = 0;  // TODO: should probably cache this?
+
+        for (sat::literal lit : lemma) {
+            if (is_suitable(lit)) {
+                num_choices++;
+                if (choice == sat::null_literal)
+                    choice = lit;
+            }
+        }
+
+        SASSERT(choice != sat::null_literal);  // must succeed for at least one
+        if (num_choices == 1)
+            propagate_bool(choice, &lemma);
+        else
+            decide_bool(choice, lemma);
+        return choice;
+
+        // constraint* c = nullptr;
+        // while (true) {
+        //     unsigned next_idx = lemma.next_guess();
+        //     SASSERT(next_idx < lemma.size());  // must succeed for at least one
+        //     sat::literal lit = lemma[next_idx];
+        //     // LOG_V("trying: "
+        //     if (m_bvars.value(lit) == l_false)
+        //         continue;
+        //     SASSERT(m_bvars.value(lit) != l_true);  // cannot happen in a valid lemma
+        //     c = m_constraints.lookup(lit.var());
+        //     c->assign(!lit.sign());
+        //     if (c->is_currently_false(*this))
+        //         continue;
+        //     // Choose c as next literal
+        //     break;
+        // }
+        // sat::literal const new_lit{c->bvar()};
+        // TODO: this will not be needed once we add boolean watchlists; alternatively replace with an incremental counter on the clause
+        // unsigned const unassigned_count =
+        //     std::count_if(lemma.begin(), lemma.end(),
+        //     [this](sat::literal lit) { return !m_bvars.is_assigned(lit); });
+        // if (unassigned_count == 1)
+        //     propagate_bool(new_lit, &lemma);
+        // else
+        //     decide_bool(new_lit, lemma);
+        // return c;
     }
 
     /**
@@ -735,9 +828,9 @@ namespace polysat {
      * In general form it can rely on factoring.
      * Root finding can further prune viable.
      */
-    void solver::revert_decision(pvar v, scoped_clause& reason) {
+    void solver::revert_decision(pvar v, clause_ref reason) {
         rational val = m_value[v];
-        LOG_H3("Reverting decision: pvar " << v << " -> " << val);
+        LOG_H3("Reverting decision: pvar " << v << " := " << val);
         SASSERT(m_justification[v].is_decision());
         bdd viable = m_viable[v];
         constraints just(m_cjust[v]);
@@ -753,7 +846,6 @@ namespace polysat {
         //     push_cjust(v, just[i]);
 
         add_non_viable(v, val);
-        learn_lemma(v, std::move(reason));
 
         for (constraint* c : m_conflict.units()) {
             // Add the conflict as justification for the exclusion of 'val'
@@ -764,6 +856,13 @@ namespace polysat {
         }
         m_conflict.reset();
 
+        learn_lemma(v, std::move(reason));
+
+        if (is_conflict()) {
+            LOG_H1("Conflict during revert_decision!");
+            return;
+        }
+
         narrow(v);
         if (m_justification[v].is_unassigned()) {
             m_free_vars.del_var_eh(v);
@@ -771,33 +870,73 @@ namespace polysat {
         }
     }
     
-    void solver::revert_bool_decision(sat::literal lit, scoped_clause& reason) {
+    void solver::revert_bool_decision(sat::literal lit, clause_ref reason) {
         sat::bool_var const var = lit.var();
         LOG_H3("Reverting boolean decision: " << lit);
         SASSERT(m_bvars.is_decision(var));
+
+        if (reason) {
+            LOG("Reason: " << show_deref(reason));
+            bool contains_var = std::any_of(reason->begin(), reason->end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; });
+            if (!contains_var) {
+                // TODO: in this case, we got here via 'backtrack'. What to do if the reason does not contain lit?
+                // * 'reason' is still a perfectly good lemma and a summary of the conflict (the lemma roughly corresponds to ~conflict)
+                // * the conflict is the reason for flipping 'lit'
+                // * thus we just add '~lit' to 'reason' and see it as "conflict => ~lit".
+                auto lits = reason->literals();
+                lits.push_back(~lit);
+                reason = clause::from_literals(reason->level(), {reason->dep(), m_dm}, lits, reason->new_constraints());
+            }
+            bool contains_opp = std::any_of(reason->begin(), reason->end(), [lit](sat::literal reason_lit) { return reason_lit == ~lit; });
+            SASSERT(contains_opp);
+        }
+        else {
+            LOG_H3("Empty reason");
+            LOG("Conflict: " << m_conflict);
+            // TODO: what to do when reason is NULL?
+            // * this means we were unable to build a lemma for the current conflict.
+            // * the reason for reverting this decision then needs to be the (negation of the) conflicting literals. Or we give up on resolving this lemma?
+            SASSERT(m_conflict.clauses().empty());  // not sure how to handle otherwise
+            unsigned reason_lvl = m_constraints.lookup(lit.var())->level();
+            p_dependency_ref reason_dep(m_constraints.lookup(lit.var())->dep(), m_dm);
+            sat::literal_vector reason_lits;
+            reason_lits.push_back(~lit);  // propagated literal
+            for (auto c : m_conflict.units()) {
+                if (c->bvar() == var)
+                    continue;
+                reason_lvl = std::max(reason_lvl, c->level());
+                reason_dep = m_dm.mk_join(reason_dep, c->dep());
+                reason_lits.push_back(c->blit());
+            }
+            reason = clause::from_literals(reason_lvl, reason_dep, reason_lits, {});
+            LOG("Made-up reason: " << show_deref(reason));
+        }
+
+        clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned
+        SASSERT(lemma);
+
         backjump(m_bvars.level(var) - 1);
 
-        bool contains_var = std::any_of(reason.begin(), reason.end(), [var](sat::literal reason_lit) { return reason_lit.var() == var; });
-        bool contains_opp = std::any_of(reason.begin(), reason.end(), [lit](sat::literal reason_lit) { return reason_lit == ~lit; });
-        SASSERT(contains_var && contains_opp);  // TODO: hm...
+        for (constraint* c : m_conflict.units()) {
+            if (c->bvar() == var)
+                continue;
+            // NOTE: in general, narrow may change the conflict.
+            //       But since we just backjumped, narrowing should not result in an additional conflict.
+            c->narrow(*this);
+        }
+        m_conflict.reset();
+
         clause* reason_cl = reason.get();
         add_lemma_clause(std::move(reason));
         propagate_bool(~lit, reason_cl);
 
-        clause* lemma = m_bvars.lemma(var);
-        unsigned next_idx = lemma->next_guess();
-        sat::literal next_lit = (*lemma)[next_idx];
-        // If the guess is the last literal then do a propagation, otherwise a decision
-        if (next_idx == lemma->size() - 1)
-            propagate_bool(next_lit, lemma);
-        else
-            decide_bool(next_lit, lemma);
+        decide_bool(*lemma);
     }
 
-    void solver::decide_bool(sat::literal lit, clause* lemma) {
+    void solver::decide_bool(sat::literal lit, clause& lemma) {
         push_level();
         LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
-        assign_bool_backtrackable(lit, nullptr, lemma);
+        assign_bool_backtrackable(lit, nullptr, &lemma);
     }
 
     void solver::propagate_bool(sat::literal lit, clause* reason) {
@@ -842,12 +981,14 @@ namespace polysat {
 
     /// Activate constraint immediately
     void solver::activate_constraint(constraint& c, bool is_true) {
-        LOG("Activating constraint: " << c);
+        LOG("Activating constraint: " << c << " ; is_true = " << is_true);
         SASSERT(m_bvars.value(c.bvar()) == to_lbool(is_true));
         c.assign(is_true);
         add_watch(c);
         c.narrow(*this);
+#if ENABLE_LINEAR_SOLVER
         m_linear_solver.activate_constraint(c);
+#endif
     }
 
     /// Deactivate constraint immediately
@@ -867,20 +1008,21 @@ namespace polysat {
     /**
      * Return residue of superposing p and q with respect to v.
      */
-    scoped_clause solver::resolve(pvar v) {
-        scoped_clause result;
+    clause_ref solver::resolve(pvar v) {
         SASSERT(!m_cjust[v].empty());
         SASSERT(m_justification[v].is_propagation());
         LOG("resolve pvar " << v);
         if (m_cjust[v].size() != 1)
             return nullptr;
         constraint* d = m_cjust[v].back();
-        scoped_ptr<constraint> res = d->resolve(*this, v);
+        constraint_ref res = d->resolve(*this, v);
         LOG("resolved: " << show_deref(res));
         if (res) {
             res->assign(true);
+            return clause::from_unit(res);
         }
-        return res;
+        else
+            return nullptr;
     }
 
     /**
@@ -891,27 +1033,22 @@ namespace polysat {
     }
 
     // Add lemma to storage but do not activate it
-    void solver::add_lemma_unit(scoped_ptr<constraint>&& lemma) {
+    void solver::add_lemma_unit(constraint_ref lemma) {
         if (!lemma)
             return;
         LOG("Lemma: " << show_deref(lemma));
-        constraint* c = m_constraints.insert(lemma.detach());
+        constraint* c = m_constraints.insert(std::move(lemma));
         insert_constraint(m_redundant, c);
     }
 
     // Add lemma to storage but do not activate it
-    void solver::add_lemma_clause(scoped_clause&& lemma) {
+    void solver::add_lemma_clause(clause_ref lemma) {
         if (!lemma)
             return;
-        LOG("Lemma: " << lemma);
-        ptr_vector<constraint> constraints = lemma.detach_constraints();
-        for (constraint* c : constraints)
-            m_constraints.insert(c);
-
-        clause* clause = lemma.detach();
-        m_redundant_clauses.push_back(clause);
-
-        // TODO:  also update clause->m_next_guess (probably needs to sort the literals too)
+        LOG("Lemma: " << show_deref(lemma));
+        SASSERT(lemma->size() > 1);
+        clause* cl = m_constraints.insert(lemma);
+        m_redundant_clauses.push_back(cl);
     }
 
     void solver::insert_constraint(ptr_vector<constraint>& cs, constraint* c) {
@@ -927,6 +1064,7 @@ namespace polysat {
     }
     
     void solver::reset_marks() {
+        LOG_V("-------------------------- (reset variable marks)");
         m_marks.reserve(m_vars.size());
         m_clock++;
         if (m_clock != 0)
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 580fba0fa..cb0264927 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -75,7 +75,7 @@ namespace polysat {
         constraint_manager       m_constraints;
         ptr_vector<constraint>   m_original;
         ptr_vector<constraint>   m_redundant;
-        scoped_ptr_vector<clause>       m_redundant_clauses;
+        ptr_vector<clause>       m_redundant_clauses;
 
         svector<sat::bool_var>   m_disjunctive_lemma;
 
@@ -195,7 +195,8 @@ namespace polysat {
         // void assign_bool_base(sat::literal lit);
         void activate_constraint(constraint& c, bool is_true);
         void deactivate_constraint(constraint& c);
-        void decide_bool(sat::literal lit, clause* lemma);
+        sat::literal decide_bool(clause& lemma);
+        void decide_bool(sat::literal lit, clause& lemma);
         void propagate_bool(sat::literal lit, clause* reason);
 
         void assign_core(pvar v, rational const& val, justification const& j);
@@ -219,7 +220,7 @@ namespace polysat {
         unsigned        m_clock { 0 };
         void reset_marks();
         bool is_marked(pvar v) const { return m_clock == m_marks[v]; }
-        void set_mark(pvar v) { m_marks[v] = m_clock; }
+        void set_mark(pvar v) { LOG_V("Marking: v" << v); m_marks[v] = m_clock; }
 
         void set_marks(constraints_and_clauses const& cc);
         void set_marks(constraint const& c);
@@ -227,7 +228,8 @@ namespace polysat {
 
         unsigned                 m_conflict_level { 0 };
 
-        scoped_clause resolve(pvar v);
+        clause_ref resolve(pvar v);
+        clause_ref resolve_bool(sat::literal lit);
 
         bool can_decide() const { return !m_free_vars.empty(); }
         void decide();
@@ -244,25 +246,24 @@ namespace polysat {
         unsigned base_level() const;
 
         void resolve_conflict();
-        void resolve_conflict_clause(scoped_clause& lemma);
-        void backtrack(unsigned i, scoped_clause& lemma);
+        void backtrack(unsigned i, clause_ref lemma);
         void report_unsat();
-        void revert_decision(pvar v, scoped_clause& reason);
-        void revert_bool_decision(sat::literal lit, scoped_clause& reason);
-        void learn_lemma(pvar v, scoped_clause&& lemma);
-        void learn_lemma_unit(pvar v, scoped_ptr<constraint>&& lemma);
-        void learn_lemma_clause(pvar v, scoped_clause&& lemma);
+        void revert_decision(pvar v, clause_ref reason);
+        void revert_bool_decision(sat::literal lit, clause_ref reason);
+        void learn_lemma(pvar v, clause_ref lemma);
+        void learn_lemma_unit(pvar v, constraint_ref lemma);
+        void learn_lemma_clause(pvar v, clause_ref lemma);
         void backjump(unsigned new_level);
-        void add_lemma_unit(scoped_ptr<constraint>&& lemma);
-        void add_lemma_clause(scoped_clause&& lemma);
+        void add_lemma_unit(constraint_ref lemma);
+        void add_lemma_clause(clause_ref lemma);
 
-        scoped_ptr<constraint> mk_eq(pdd const& p, unsigned dep);
-        scoped_ptr<constraint> mk_diseq(pdd const& p, unsigned dep);
-        scoped_ptr<constraint> mk_ule(pdd const& p, pdd const& q, unsigned dep);
-        scoped_ptr<constraint> mk_ult(pdd const& p, pdd const& q, unsigned dep);
-        scoped_ptr<constraint> mk_sle(pdd const& p, pdd const& q, unsigned dep);
-        scoped_ptr<constraint> mk_slt(pdd const& p, pdd const& q, unsigned dep);
-        void new_constraint(scoped_ptr<constraint>&& c, bool activate);
+        constraint_ref mk_eq(pdd const& p, unsigned dep);
+        constraint_ref mk_diseq(pdd const& p, unsigned dep);
+        constraint_ref mk_ule(pdd const& p, pdd const& q, unsigned dep);
+        constraint_ref mk_ult(pdd const& p, pdd const& q, unsigned dep);
+        constraint_ref mk_sle(pdd const& p, pdd const& q, unsigned dep);
+        constraint_ref mk_slt(pdd const& p, pdd const& q, unsigned dep);
+        void new_constraint(constraint_ref c, bool activate);
         static void insert_constraint(ptr_vector<constraint>& cs, constraint* c);
 
         bool invariant();
@@ -321,20 +322,20 @@ namespace polysat {
          * Create polynomial constraints (but do not activate them).
          * Each constraint is tracked by a dependency.
          */
-        void new_eq(pdd const& p, unsigned dep);
-        void new_diseq(pdd const& p, unsigned dep);
-        void new_ule(pdd const& p, pdd const& q, unsigned dep);
-        void new_ult(pdd const& p, pdd const& q, unsigned dep);
-        void new_sle(pdd const& p, pdd const& q, unsigned dep);
-        void new_slt(pdd const& p, pdd const& q, unsigned dep);
+        void new_eq(pdd const& p, unsigned dep)                { new_constraint(mk_eq(p, dep), false); }
+        void new_diseq(pdd const& p, unsigned dep)             { new_constraint(mk_diseq(p, dep), false); }
+        void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q, dep), false); }
+        void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q, dep), false); }
+        void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q, dep), false); }
+        void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q, dep), false); }
 
         /** Create and activate polynomial constraints. */
-        void add_eq(pdd const& p, unsigned dep = null_dependency);
-        void add_diseq(pdd const& p, unsigned dep = null_dependency);
-        void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency);
-        void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency);
-        void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency);
-        void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency);
+        void add_eq(pdd const& p, unsigned dep = null_dependency)                { new_constraint(mk_eq(p, dep), true); }
+        void add_diseq(pdd const& p, unsigned dep = null_dependency)             { new_constraint(mk_diseq(p, dep), true); }
+        void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q, dep), true); }
+        void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q, dep), true); }
+        void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q, dep), true); }
+        void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q, dep), true); }
         
         /**
          * Activate the constraint corresponding to the given boolean variable.
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index e5022fa04..c86fe496d 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -19,13 +19,13 @@ Author:
 namespace polysat {
 
     std::ostream& ule_constraint::display(std::ostream& out) const {
-        out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " @" << level();
+        out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " @" << level() << " b" << bvar();
         if (is_undef())
             out << " [inactive]";
         return out;
     }
 
-    scoped_ptr<constraint> ule_constraint::resolve(solver& s, pvar v) {
+    constraint_ref ule_constraint::resolve(solver& s, pvar v) {
         return nullptr;
     }
 
@@ -121,7 +121,7 @@ namespace polysat {
             return p.is_val() && q.is_val() && p.val() > q.val();
     }
 
-    bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr<constraint>& out_neg_cond)
+    bool ule_constraint::forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond)
     {
         SASSERT(!is_undef());
 
@@ -189,6 +189,11 @@ namespace polysat {
         // Concrete values of evaluable terms
         auto e1s = e1.subst_val(s.assignment());
         auto e2s = e2.subst_val(s.assignment());
+        // TODO: this is not always true! cjust[v]/conflict may contain unassigned variables (they're coming from a previous conflict, but together they lead to a conflict. need something else to handle that.)
+        if (!e1s.is_val())
+            return false;
+        if (!e2s.is_val())
+            return false;
         SASSERT(e1s.is_val());
         SASSERT(e2s.is_val());
 
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index 545421da4..e72ba1f4d 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -32,13 +32,13 @@ namespace polysat {
         pdd const& lhs() const { return m_lhs; }
         pdd const& rhs() const { return m_rhs; }
         std::ostream& display(std::ostream& out) const override;
-        scoped_ptr<constraint> resolve(solver& s, pvar v) override;
+        constraint_ref resolve(solver& s, pvar v) override;
         bool is_always_false(pdd const& lhs, pdd const& rhs);
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
         bool is_currently_true(solver& s) override;
         void narrow(solver& s) override;
-        bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, scoped_ptr<constraint>& out_neg_cond) override;
+        bool forbidden_interval(solver& s, pvar v, eval_interval& out_interval, constraint_ref& out_neg_cond) override;
     };
 
 }
diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp
index dd7b03c98..6f6b7d7c5 100644
--- a/src/math/polysat/var_constraint.cpp
+++ b/src/math/polysat/var_constraint.cpp
@@ -21,7 +21,7 @@ namespace polysat {
         return out << "v" << m_var << ": " << m_viable << "\n";
     }
 
-    scoped_ptr<constraint> var_constraint::resolve(solver& s, pvar v) {
+    constraint_ref var_constraint::resolve(solver& s, pvar v) {
         UNREACHABLE();
         return nullptr;
     }
diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h
index 7e07d82e4..44d8c25ce 100644
--- a/src/math/polysat/var_constraint.h
+++ b/src/math/polysat/var_constraint.h
@@ -33,7 +33,7 @@ namespace polysat {
             constraint(m, lvl, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
         ~var_constraint() override {}
         std::ostream& display(std::ostream& out) const override;
-        scoped_ptr<constraint> resolve(solver& s, pvar v) override;
+        constraint_ref resolve(solver& s, pvar v) override;
         void narrow(solver& s) override;
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index e74bf22e6..22f8b5e38 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -153,7 +153,7 @@ public:
     expr_ref_vector const &get_cube();
     void update_cube(pob_ref const &p, expr_ref_vector &cube);
 
-    bool has_pob() {return m_pob;}
+    bool has_pob() {return !!m_pob;}
     pob_ref &get_pob() {return m_pob;}
     unsigned weakness() {return m_weakness;}
 
diff --git a/src/util/ref.h b/src/util/ref.h
index 764eb416b..1f30aae82 100644
--- a/src/util/ref.h
+++ b/src/util/ref.h
@@ -66,10 +66,14 @@ public:
         return m_ptr;
     }
 
-    operator bool() const {
+    explicit operator bool() const {
         return m_ptr != nullptr;
     }
 
+    bool operator!() const {
+        return m_ptr == nullptr;
+    }
+
     const T & operator*() const {
         return *m_ptr;
     }
diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
index 9e502335e..406f7be61 100644
--- a/src/util/ref_vector.h
+++ b/src/util/ref_vector.h
@@ -20,6 +20,7 @@ Revision History:
 
 #include "util/vector.h"
 #include "util/obj_ref.h"
+#include "util/ref.h"
 
 /**
    \brief Vector of smart pointers.
@@ -113,6 +114,11 @@ public:
         return *this;
     }
 
+    ref_vector_core& push_back(ref<T>&& n) {
+        m_nodes.push_back(n.detach());
+        return *this;
+    }
+
     void pop_back() {
         SASSERT(!m_nodes.empty());
         T * n = m_nodes.back();