diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index 1e8fdf44a..c440ebeb2 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -33,7 +33,7 @@ namespace polysat {
         friend class constraint_manager;
 
         unsigned m_ref_count = 0;  // TODO: remove refcount once we confirm it's not needed anymore
-        bool m_redundant = false;
+        bool m_redundant = true;
         sat::literal_vector m_literals;
 
 
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index 55a32a30f..dc2d223f7 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -27,7 +27,6 @@ namespace polysat {
      * \param[out] fi               "forbidden interval" record that captures values not allowed for v
      * \returns True iff a forbidden interval exists and the output parameters were set.
      */
-
     bool forbidden_intervals::get_interval(signed_constraint const& c, pvar v, fi_record& fi) {
         if (!c->is_ule())
             return false;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 11a90ae05..35af5aaa6 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -124,6 +124,18 @@ namespace polysat {
         m_free_pvars.del_var_eh(v);
     }
 
+    std::tuple<pdd, pdd> solver::quot_rem(pdd const& a, pdd const& b) {
+        auto& m = a.manager();
+        unsigned sz = m.power_of_2();
+        pdd quot = m.mk_var(add_var(sz));
+        pdd rem = m.mk_var(add_var(sz));
+        add_eq(b * quot + rem - a);
+        add_noovfl(b, quot);
+        add_clause(eq(b), ult(rem, b), false);
+        return std::tuple<pdd, pdd>(quot, rem);
+    }
+
+
     void solver::assign_eh(signed_constraint c, unsigned dep) {
         SASSERT(at_base_level());
         SASSERT(c);
@@ -545,7 +557,7 @@ namespace polysat {
     void solver::learn_lemma(clause& lemma) {
         LOG("Learning: "<< lemma);
         SASSERT(!lemma.empty());
-        add_lemma(lemma);
+        add_clause(lemma);
         if (!is_conflict())
             decide_bool(lemma);
     }
@@ -667,7 +679,7 @@ namespace polysat {
 
         backjump(m_bvars.level(var) - 1);
 
-        add_lemma(*reason);
+        add_clause(*reason);
 
         if (!is_conflict() && lemma)
             decide_bool(*lemma);
@@ -751,17 +763,28 @@ namespace polysat {
     }
 
     // Add lemma to storage
-    void solver::add_lemma(clause& lemma) {
-        LOG("Lemma: " << lemma);
-        for (sat::literal lit : lemma) {
+    void solver::add_clause(clause& clause) {
+        LOG("Lemma: " << clause);
+        for (sat::literal lit : clause) {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
             // SASSERT(m_bvars.value(lit) != l_true);
         }
-        SASSERT(!lemma.empty());
-        m_constraints.store(&lemma, *this);
+        SASSERT(!clause.empty());
+        m_constraints.store(&clause, *this);
         propagate();
     }
 
+    void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
+        clause_builder cb(*this);
+        if (!c1.is_always_false())
+            cb.push(c1);
+        if (!c2.is_always_false())
+            cb.push(c2);
+        clause_ref clause = cb.build();
+        clause->set_redundant(is_redundant);
+        add_clause(*clause);
+    }
+
     void solver::insert_constraint(signed_constraints& cs, signed_constraint c) {
         SASSERT(c);
         LOG_V("INSERTING: " << c);
@@ -780,6 +803,7 @@ namespace polysat {
         LOG("Pop " << num_scopes << " user scopes; lowest popped level = " << base_level << "; current level = " << m_level);
         pop_levels(m_level - base_level + 1);
         m_conflict.reset();   
+        m_base_levels.shrink(m_base_levels.size() - num_scopes);
     }
 
     bool solver::at_base_level() const {
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index d332495be..a3f4d7254 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -205,7 +205,8 @@ namespace polysat {
         void report_unsat();
         void learn_lemma(clause& lemma);
         void backjump(unsigned new_level);
-        void add_lemma(clause& lemma);
+        void add_clause(clause& lemma);
+        void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
 
 
         signed_constraint lit2cnstr(sat::literal lit) const { return m_constraints.lookup(lit); }
@@ -236,11 +237,9 @@ namespace polysat {
          * 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();
 
-
         /**
          * retrieve unsat core dependencies
          */
@@ -256,6 +255,18 @@ namespace polysat {
          */
         pdd var(pvar v) { return m_vars[v]; }
 
+        /**
+        * Create terms for unsigned quot-rem
+        * 
+        * Return tuple (quot, rem)
+        * 
+        * The following properties are enforced:
+        * b*quot + rem = a
+        * ~ovfl(b*quot)
+        * rem < b or b = 0
+        */
+        std::tuple<pdd, pdd> quot_rem(pdd const& a, pdd const& b);
+
         /**
          * Create polynomial constant.
          */