diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 90eb39877..35db88e10 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -29,16 +29,16 @@ namespace polysat {
         return *dynamic_cast<eq_constraint const*>(this); 
     }
 
-    constraint* constraint::eq(unsigned lvl, pdd const& p, p_dependency_ref& d) {
-        return alloc(eq_constraint, lvl, p, d);
+    constraint* constraint::eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d) {
+        return alloc(eq_constraint, lvl, bvar, sign, p, d);
     }
 
-    constraint* constraint::viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d) {
-        return alloc(var_constraint, lvl, v, b, d);
+    constraint* constraint::viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d) {
+        return alloc(var_constraint, lvl, bvar, sign, v, b, d);
     }
 
-    constraint* constraint::ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d) {
-        return alloc(ule_constraint, lvl, a, b, d);
+    constraint* constraint::ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d) {
+        return alloc(ule_constraint, lvl, bvar, sign, a, b, d);
     }
 
 }
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 5c57e4bdf..365a60a89 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -17,6 +17,7 @@ Author:
 namespace polysat {
 
     enum ckind_t { eq_t, ule_t, sle_t, bit_t };
+    enum csign_t : bool { neg_t = false, pos_t = true };
 
     class eq_constraint;
     class var_constraint;
@@ -30,12 +31,15 @@ namespace polysat {
         ckind_t          m_kind;
         p_dependency_ref m_dep;
         unsigned_vector  m_vars;
-        constraint(unsigned lvl, p_dependency_ref& dep, ckind_t k): 
-            m_level(lvl), m_kind(k), m_dep(dep) {}
+        bool_var         m_bool_var;
+        csign_t          m_sign;  ///< sign/polarity
+        lbool            m_status = l_undef;  ///< current constraint status, computed from value of m_bool_var and m_sign
+        constraint(unsigned lvl, bool_var bvar, csign_t sign, p_dependency_ref& dep, ckind_t k):
+            m_level(lvl), m_kind(k), m_dep(dep), m_bool_var(bvar), m_sign(sign) {}
     public:
-        static constraint* eq(unsigned lvl, pdd const& p, p_dependency_ref& d);
-        static constraint* viable(unsigned lvl, pvar v, bdd const& b, p_dependency_ref& d);
-        static constraint* ule(unsigned lvl, pdd const& a, pdd const& b, p_dependency_ref& d);
+        static constraint* eq(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& d);
+        static constraint* viable(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const& b, p_dependency_ref& d);
+        static constraint* ule(unsigned lvl, bool_var bvar, csign_t sign, pdd const& a, pdd const& b, p_dependency_ref& d);
         virtual ~constraint() {}
         bool is_eq() const { return m_kind == ckind_t::eq_t; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
@@ -46,12 +50,18 @@ namespace polysat {
         virtual 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;
         virtual void narrow(solver& s) = 0;
         eq_constraint& to_eq();
         eq_constraint const& to_eq() const;
         p_dependency* dep() const { return m_dep; }
         unsigned_vector& vars() { return m_vars; }
         unsigned level() const { return m_level; }
+        bool_var bvar() const { return m_bool_var; }
+        bool sign() const { return m_sign; }
+        void assign_eh(bool is_true) { m_status = (is_true ^ !m_sign) ? l_true : l_false; }
+        bool is_positive() const { return m_status == l_true; }
+        bool is_negative() const { return m_status == l_false; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp
index 969b42e8c..d5b57f1a8 100644
--- a/src/math/polysat/eq_constraint.cpp
+++ b/src/math/polysat/eq_constraint.cpp
@@ -19,7 +19,7 @@ Author:
 namespace polysat {
 
     std::ostream& eq_constraint::display(std::ostream& out) const {
-        return out << p() << " == 0";
+        return out << p() << (sign() == pos_t ? " == 0" : " != 0") << " [" << m_status << "]";
     }
 
     bool eq_constraint::propagate(solver& s, pvar v) {
@@ -43,9 +43,56 @@ namespace polysat {
     }
 
     constraint* eq_constraint::resolve(solver& s, pvar v) {
+        if (is_positive())
+            return eq_resolve(s, v);
+        if (is_negative())
+            return diseq_resolve(s, v);
+        UNREACHABLE();
+    }
+
+    void eq_constraint::narrow(solver& s) {
+        if (is_positive())
+            eq_narrow(s);
+        if (is_negative())
+            diseq_narrow(s);
+    }
+
+    bool eq_constraint::is_always_false() {
+        if (is_positive())
+            return p().is_never_zero();
+        if (is_negative())
+            return p().is_zero();
+        UNREACHABLE();
+    }
+
+    bool eq_constraint::is_currently_false(solver& s) {
+        pdd r = p().subst_val(s.m_search);
+        if (is_positive())
+            return r.is_never_zero();
+        if (is_negative())
+            return r.is_zero();
+        UNREACHABLE();
+    }
+
+    bool eq_constraint::is_currently_true(solver& s) {
+        pdd r = p().subst_val(s.m_search);
+        if (is_positive())
+            return r.is_zero();
+        if (is_negative())
+            return r.is_never_zero();
+        UNREACHABLE();
+    }
+
+    /**
+     * Equality constraints
+     */
+
+    constraint* eq_constraint::eq_resolve(solver& s, pvar v) {
+        SASSERT(is_currently_true(s));
         if (s.m_conflict.size() != 1)
             return nullptr;
         constraint* c = s.m_conflict[0];
+        SASSERT(c->is_currently_false(s));
         if (c->is_eq()) {
             pdd a = c->to_eq().p();
             pdd b = p();
@@ -54,12 +101,14 @@ namespace polysat {
                 return nullptr;
             p_dependency_ref d(s.m_dm.mk_join(c->dep(), dep()), s.m_dm);
             unsigned lvl = std::max(c->level(), level());
-            return constraint::eq(lvl, r, d);             
+            constraint* lemma = constraint::eq(lvl, s.m_next_bvar++, pos_t, r, d);
+            lemma->assign_eh(true);
+            return lemma;
         }
         return nullptr;
     }
 
-    void eq_constraint::narrow(solver& s) {
+    void eq_constraint::eq_narrow(solver& s) {
         LOG("Assignment: " << s.m_search);
         auto q = p().subst_val(s.m_search);
         LOG("Substituted: " << p() << " := " << q);
@@ -92,13 +141,17 @@ namespace polysat {
         // TODO: what other constraints can be extracted cheaply?
     }
 
-    bool eq_constraint::is_always_false() {
-        return p().is_never_zero();
+
+    /**
+     * Disequality constraints
+     */
+
+    constraint* eq_constraint::diseq_resolve(solver& s, pvar v) {
+        NOT_IMPLEMENTED_YET();
     }
 
-    bool eq_constraint::is_currently_false(solver& s) {
-        pdd r = p().subst_val(s.m_search);
-        return r.is_never_zero();
+    void eq_constraint::diseq_narrow(solver& s) {
+        NOT_IMPLEMENTED_YET();
     }
 
 }
diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h
index 40c764391..c20f0e35b 100644
--- a/src/math/polysat/eq_constraint.h
+++ b/src/math/polysat/eq_constraint.h
@@ -20,8 +20,8 @@ namespace polysat {
     class eq_constraint : public constraint {
         pdd m_poly;
     public:
-        eq_constraint(unsigned lvl, pdd const& p, p_dependency_ref& dep):
-            constraint(lvl, dep, ckind_t::eq_t), m_poly(p) {
+        eq_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& p, p_dependency_ref& dep):
+            constraint(lvl, bvar, sign, dep, ckind_t::eq_t), m_poly(p) {
             m_vars.append(p.free_vars());
         }
         ~eq_constraint() override {}
@@ -31,7 +31,14 @@ namespace polysat {
         constraint* 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;
+
+    private:
+        constraint* eq_resolve(solver& s, pvar v);
+        void eq_narrow(solver& s);
+        constraint* diseq_resolve(solver& s, pvar v);
+        void diseq_narrow(solver& s);
     };
 
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 4d445e143..1dc55eeae 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -148,58 +148,76 @@ namespace polysat {
         m_free_vars.del_var_eh(v);
     }
 
-    void solver::add_constraint(constraint* c) {
+    void solver::new_constraint(constraint* c) {
         SASSERT(c);
-        LOG("Adding constraint: " << *c);
+        LOG("New constraint: " << *c);
         m_constraints.push_back(c);
-        c->narrow(*this);
+        SASSERT(!get_bv2c(c->bvar()));
+        insert_bv2c(c->bvar(), c);
     }
 
-    void solver::add_eq(pdd const& p, unsigned dep) {
+    bool_var solver::new_eq(pdd const& p, unsigned dep) {
         p_dependency_ref d(mk_dep(dep), m_dm);
-        constraint* c = constraint::eq(m_level, p, d);
-        add_watch(*c);
-        add_constraint(c);
+        constraint* c = constraint::eq(m_level, m_next_bvar++, pos_t, p, d);
+        new_constraint(c);
+        return c->bvar();
     }
 
-    void solver::add_diseq(pdd const& p, unsigned dep) {
-        if (p.is_val()) {
-            if (!p.is_zero()) 
-                return;
-            // set conflict.
-            NOT_IMPLEMENTED_YET();
-            return;
-        }
+    bool_var solver::new_diseq(pdd const& p, unsigned dep) {
+        // if (p.is_val()) {
+        //     if (!p.is_zero())
+        //         return;
+        //     // set conflict.
+        //     NOT_IMPLEMENTED_YET();   // TODO: not here, only when activated
+        //     return;
+        // }
         unsigned sz = size(p.var());
         auto slack = add_var(sz);
         auto q = p + var(slack);
         add_eq(q, dep);
         auto non_zero = sz2bits(sz).non_zero();
         p_dependency_ref d(mk_dep(dep), m_dm);        
-        constraint* c = constraint::viable(m_level, slack, non_zero, d);
-        add_constraint(c);
+        constraint* c = constraint::viable(m_level, m_next_bvar++, pos_t, slack, non_zero, d);
+        new_constraint(c);
+        return c->bvar();
     }
 
-    void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) {
+    bool_var solver::new_ule(pdd const& p, pdd const& q, unsigned dep, csign_t sign) {
         p_dependency_ref d(mk_dep(dep), m_dm);
-        constraint* c = constraint::ule(m_level, p, q, d);
+        constraint* c = constraint::ule(m_level, m_next_bvar++, sign, p, q, d);
+        new_constraint(c);
+        return c->bvar();
+    }
+
+    bool_var solver::new_sle(pdd const& p, pdd const& q, unsigned dep, csign_t sign) {
+        auto shift = rational::power_of_two(p.power_of_2() - 1);
+        return new_ule(p + shift, q + shift, dep, sign);
+    }
+
+    bool_var solver::new_ult(pdd const& p, pdd const& q, unsigned dep) {
+        return new_ule(q, p, dep, neg_t);
+    }
+
+    bool_var solver::new_slt(pdd const& p, pdd const& q, unsigned dep) {
+        return new_sle(q, p, dep, neg_t);
+    }
+
+    void solver::add_eq(pdd const& p, unsigned dep) { assign_eh(new_eq(p, dep), true); }
+    void solver::add_diseq(pdd const& p, unsigned dep) { assign_eh(new_diseq(p, dep), true); }
+    void solver::add_ule(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ule(p, q, dep), true); }
+    void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_ult(p, q, dep), true); }
+    void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_sle(p, q, dep), true); }
+    void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) { assign_eh(new_slt(p, q, dep), true); }
+
+    void solver::assign_eh(bool_var v, bool is_true) {
+        constraint* c = get_bv2c(v);
+        if (!c) {
+            LOG("WARN: there is no constraint for bool_var " << v);
+            return;
+        }
+        c->assign_eh(is_true);
         add_watch(*c);
-        add_constraint(c);
-    }
-
-    void solver::add_sle(pdd const& p, pdd const& q, unsigned dep) {
-        // save for later
-        NOT_IMPLEMENTED_YET();
-    }
-
-    void solver::add_ult(pdd const& p, pdd const& q, unsigned dep) {
-        // save for later
-        NOT_IMPLEMENTED_YET();
-    }
-
-    void solver::add_slt(pdd const& p, pdd const& q, unsigned dep) {
-        // save for later
-        NOT_IMPLEMENTED_YET();
+        c->narrow(*this);
     }
 
 
@@ -566,6 +584,8 @@ namespace polysat {
         if (!c)
             return;
         LOG("Lemma: " << *c);
+        SASSERT(!get_bv2c(c->bvar()));
+        insert_bv2c(c->bvar(), c);
         add_watch(*c);
         m_redundant.push_back(c);
         for (unsigned i = m_redundant.size() - 1; i-- > 0; ) {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index bc87f7066..0e5a1f200 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -65,6 +65,13 @@ namespace polysat {
         scoped_ptr_vector<constraint>   m_constraints;
         scoped_ptr_vector<constraint>   m_redundant;
 
+        // Map boolean variables to constraints
+        bool_var                 m_next_bvar = 2;  // TODO: later, bool vars come from external supply
+        ptr_vector<constraint>   m_bv2constraint;
+        void insert_bv2c(bool_var bv, constraint* c) { m_bv2constraint.setx(bv, c, nullptr); }
+        void erase_bv2c(bool_var bv) { m_bv2constraint[bv] = nullptr; }
+        constraint* get_bv2c(bool_var bv) const { return m_bv2constraint.get(bv, nullptr); }
+
         // Per variable information
         vector<bdd>              m_viable;   // set of viable values.
         vector<rational>         m_value;    // assigned value
@@ -204,7 +211,7 @@ namespace polysat {
         void backjump(unsigned new_level);
         void add_lemma(constraint* c);
 
-        void add_constraint(constraint* c);
+        void new_constraint(constraint* c);
 
         bool invariant();
         bool invariant(scoped_ptr_vector<constraint> const& cs);
@@ -222,9 +229,20 @@ namespace polysat {
 
         /**
          * End-game satisfiability checker.
+         *
+         * Returns l_undef if the search cannot proceed.
+         * Possible reasons:
+         * - Resource limits are exhausted.
+         * - A disjunctive lemma should be learned. The disjunction needs to be handled externally.
          */
         lbool check_sat();
 
+        /**
+         * Returns the disjunctive lemma that should be learned,
+         * or an empty vector if check_sat() terminated for a different reason.
+         */
+        bool_var_vector get_lemma() { NOT_IMPLEMENTED_YET(); return {}; };
+
         /**
          * retrieve unsat core dependencies
          */
@@ -241,10 +259,17 @@ namespace polysat {
         pdd var(pvar v) { return m_vars[v]; }
 
         /**
-         * Add polynomial constraints
+         * Create polynomial constraints (but do not activate them).
          * Each constraint is tracked by a dependency.
-         * assign sets the 'index'th bit of var.
          */
+        bool_var new_eq(pdd const& p, unsigned dep = null_dependency);
+        bool_var new_diseq(pdd const& p, unsigned dep = null_dependency);
+        bool_var new_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t);
+        bool_var new_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency);
+        bool_var new_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency, csign_t sign = pos_t);
+        bool_var new_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency);
+
+        /** 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);
@@ -252,6 +277,11 @@ namespace polysat {
         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);
         
+        /**
+         * Activate the constraint corresponding to the given boolean variable.
+         * Note: to deactivate, use push/pop.
+         */
+        void assign_eh(bool_var v, bool is_true);
 
         /**
          * main state transitions.
@@ -264,7 +294,7 @@ namespace polysat {
          * Adds so-called user-scope.
          */
         void push();
-        void pop(unsigned num_scopes);
+        void pop(unsigned num_scopes = 1);
        
         std::ostream& display(std::ostream& out) const;
 
diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h
index f799ff70c..392490964 100644
--- a/src/math/polysat/types.h
+++ b/src/math/polysat/types.h
@@ -51,4 +51,7 @@ namespace polysat {
     typedef obj_ref<p_dependency, poly_dep_manager> p_dependency_ref; 
     typedef ref_vector<p_dependency, poly_dep_manager> p_dependency_refv;
 
+    typedef int bool_var;  // see smt_types.h
+    typedef svector<bool_var> bool_var_vector;  // see smt_types.h
+
 }
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 5e9572549..6707fb4c7 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -19,7 +19,7 @@ Author:
 namespace polysat {
 
     std::ostream& ule_constraint::display(std::ostream& out) const {
-        return out << m_lhs << " <=u " << m_rhs;
+        return out << m_lhs << (sign() == pos_t ? " <=u " : " >u ") << m_rhs << " [" << m_status << "]";
     }
 
     bool ule_constraint::propagate(solver& s, pvar v) {
@@ -57,7 +57,8 @@ namespace polysat {
             return;
         }
         if (p.is_val() && q.is_val()) {
-            SASSERT(p.val() <= q.val());
+            SASSERT(!is_positive() || p.val() <= q.val());
+            SASSERT(!is_negative() || p.val() > q.val());
             return;
         }
 
@@ -89,7 +90,9 @@ namespace polysat {
         }
         if (v != null_var) {
             bddv const& x = s.var2bits(v).var();
-            bdd xs = (a * x + b <= c * x + d);
+            bddv l = a * x + b;
+            bddv r = c * x + d;
+            bdd xs = is_positive() ? (l <= r) : (l > r);
             s.push_cjust(v, this);
             s.intersect_viable(v, xs);
 
@@ -106,7 +109,11 @@ namespace polysat {
 
     bool ule_constraint::is_always_false(pdd const& lhs, pdd const& rhs) {
         // TODO: other conditions (e.g. when forbidden interval would be full)
-        return lhs.is_val() && rhs.is_val() && !(lhs.val() <= rhs.val());
+        if (is_positive())
+            return lhs.is_val() && rhs.is_val() && !(lhs.val() <= rhs.val());
+        if (is_negative())
+            return lhs.is_val() && rhs.is_val() && !(lhs.val() > rhs.val());
+        UNREACHABLE();
     }
 
     bool ule_constraint::is_always_false() {
@@ -119,4 +126,14 @@ namespace polysat {
         return is_always_false(p, q);
     }
 
+    bool ule_constraint::is_currently_true(solver& s) {
+        auto p = lhs().subst_val(s.m_search);
+        auto q = rhs().subst_val(s.m_search);
+        if (is_positive())
+            return p.is_val() && q.is_val() && p.val() <= q.val();
+        if (is_negative())
+            return p.is_val() && q.is_val() && p.val() > q.val();
+        UNREACHABLE();
+    }
+
 }
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index c2339b258..cc7cdd45c 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -21,8 +21,8 @@ namespace polysat {
         pdd m_lhs;
         pdd m_rhs;
     public:
-        ule_constraint(unsigned lvl, pdd const& l, pdd const& r, p_dependency_ref& dep):
-            constraint(lvl, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
+        ule_constraint(unsigned lvl, bool_var bvar, csign_t sign, pdd const& l, pdd const& r, p_dependency_ref& dep):
+            constraint(lvl, bvar, sign, dep, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
             m_vars.append(l.free_vars());
             for (auto v : r.free_vars())
                 if (!m_vars.contains(v))
@@ -34,9 +34,10 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool propagate(solver& s, pvar v) override;
         constraint* resolve(solver& s, pvar v) override;
-        static bool is_always_false(pdd const& lhs, pdd const& rhs);
+        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;
     };
 
diff --git a/src/math/polysat/var_constraint.cpp b/src/math/polysat/var_constraint.cpp
index 5e5308b0d..aae02f408 100644
--- a/src/math/polysat/var_constraint.cpp
+++ b/src/math/polysat/var_constraint.cpp
@@ -39,6 +39,10 @@ namespace polysat {
         return s.m_viable[m_var].is_false();
     }
 
+    bool var_constraint::is_currently_true(solver& s) {
+        return !s.m_viable[m_var].is_false();
+    }
+
     void var_constraint::narrow(solver& s) {
         s.intersect_viable(m_var, m_viable);
     }
diff --git a/src/math/polysat/var_constraint.h b/src/math/polysat/var_constraint.h
index 57e5610f0..9490fdd1f 100644
--- a/src/math/polysat/var_constraint.h
+++ b/src/math/polysat/var_constraint.h
@@ -29,8 +29,8 @@ namespace polysat {
         pvar        m_var;
         bdd         m_viable;
     public:
-        var_constraint(unsigned lvl, pvar v, bdd const & b, p_dependency_ref& dep):
-            constraint(lvl, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
+        var_constraint(unsigned lvl, bool_var bvar, csign_t sign, pvar v, bdd const & b, p_dependency_ref& dep):
+            constraint(lvl, bvar, sign, dep, ckind_t::bit_t), m_var(v), m_viable(b) {}
         ~var_constraint() override {}
         std::ostream& display(std::ostream& out) const override;
         bool propagate(solver& s, pvar v) override;
@@ -38,5 +38,6 @@ namespace polysat {
         void narrow(solver& s) override;
         bool is_always_false() override;
         bool is_currently_false(solver& s) override;
+        bool is_currently_true(solver& s) override;
     };
 }
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 63fc99e88..d271f1dcf 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -12,8 +12,33 @@ namespace polysat {
     struct scoped_solver : public solver_scope, public solver {
         scoped_solver(): solver(lim) {}
 
+        lbool check_rec() {
+            lbool result = check_sat();
+            if (result != l_undef)
+                return result;
+            auto const& new_lemma = get_lemma();
+            // Empty lemma => check_sat() terminated for another reason, e.g., resource limits
+            if (new_lemma.empty())
+                return l_undef;
+            for (auto lit : new_lemma) {
+                push();
+                assign_eh(lit, true);
+                result = check_rec();
+                pop();
+                // Found a model => done
+                if (result == l_true)
+                    return l_true;
+                if (result == l_undef)
+                    return l_undef;
+                // Unsat => try next literal
+                SASSERT(result == l_false);
+            }
+            // No literal worked? unsat
+            return l_false;
+        }
+
         void check() {
-            std::cout << check_sat() << "\n";
+            std::cout << check_rec() << "\n";
             statistics st;
             collect_statistics(st);
             std::cout << st << "\n";
@@ -113,9 +138,9 @@ namespace polysat {
         auto v = s.var(s.add_var(5));
         auto q = s.var(s.add_var(5));
         auto r = s.var(s.add_var(5));
-        s.add_eq(u - (v*q) - r, 0);
-        s.add_ult(r, u, 0);
-        s.add_ult(u, v*q, 0);
+        s.add_eq(u - (v*q) - r);
+        s.add_ult(r, u);
+        s.add_ult(u, v*q);
         s.check();
     }