diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 0f210f331..20d745523 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -165,7 +165,11 @@ namespace dd {
         return true;
     }
 
-    pdd pdd_manager::subst_val(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {
+    pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
+        return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
+    }
+
+    pdd pdd_manager::subst_val0(pdd const& p, vector<std::pair<unsigned, rational>> const& _s) {
         typedef std::pair<unsigned, rational> pr;
         vector<pr> s(_s);        
         std::function<bool (pr const&, pr const&)> compare_level = 
@@ -173,10 +177,16 @@ namespace dd {
         std::sort(s.begin(), s.end(), compare_level);
         pdd r(one());
         for (auto const& q : s) 
-            r = (r * mk_var(q.first)) + q.second;            
-        return pdd(apply(p.root, r.root, pdd_subst_val_op), this);
+            r = (r * mk_var(q.first)) + q.second;
+        return subst_val(p, r);
     }
 
+    pdd pdd_manager::subst_add(pdd const& s, unsigned v, rational const& val) {
+        pdd v_val = mk_var(v) + val;
+        return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
+    }
+    
+
     pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
         bool first = true;
         SASSERT(well_formed());
@@ -247,6 +257,14 @@ namespace dd {
             }
             if (is_val(p) || is_val(q)) return p;            
             break;
+        case pdd_subst_add_op:
+            if (is_one(p)) return q;
+            SASSERT(!is_val(p));
+            SASSERT(!is_val(q));
+            if (level(p) < level(q))
+                // p*hi(q) + lo(q)
+                return make_node(level(q), lo(q), p);
+            break;
         default:
             UNREACHABLE();
             break;
@@ -404,6 +422,14 @@ namespace dd {
                 npop = 3;
             }
             break;
+        case pdd_subst_add_op:
+            SASSERT(!is_val(p));
+            SASSERT(!is_val(q));
+            SASSERT(level_p > level_q);
+            push(apply_rec(hi(p), q, pdd_subst_add_op));           // hi := add_subst(hi(p), q)
+            r = make_node(level_p, lo(p), read(1));                // r := hi*var(p) + lo(p)
+            npop = 1;
+            break;
         default:
             r = null_pdd;
             UNREACHABLE();
@@ -415,6 +441,7 @@ namespace dd {
         return r;
     }
 
+
     pdd pdd_manager::minus(pdd const& a) {
         if (m_semantics == mod2_e) {
             return a;
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 0b73be6e5..b81d5c915 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -68,8 +68,9 @@ namespace dd {
             pdd_mul_op = 5,
             pdd_reduce_op = 6,
             pdd_subst_val_op = 7,
-            pdd_div_const_op = 8,
-            pdd_no_op = 9
+            pdd_subst_add_op = 8,
+            pdd_div_const_op = 9,
+            pdd_no_op = 10
         };
 
         struct node {
@@ -338,8 +339,10 @@ namespace dd {
         pdd mk_xor(pdd const& p, unsigned q);
         pdd mk_not(pdd const& p);
         pdd reduce(pdd const& a, pdd const& b);
-        pdd subst_val(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
+        pdd subst_val0(pdd const& a, vector<std::pair<unsigned, rational>> const& s);
         pdd subst_val(pdd const& a, unsigned v, rational const& val);
+        pdd subst_val(pdd const& a, pdd const& s);
+        pdd subst_add(pdd const& s, unsigned v, rational const& val);
         bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
         pdd reduce(unsigned v, pdd const& a, pdd const& b);
         void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
@@ -436,8 +439,10 @@ namespace dd {
         bool resolve(unsigned v, pdd const& other, pdd& result) { return m.resolve(v, *this, other, result); }
         pdd reduce(unsigned v, pdd const& other) const { return m.reduce(v, *this, other); }
 
-        pdd subst_val(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val(*this, s); }
+        pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
+        pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
         pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
+        pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
 
         std::ostream& display(std::ostream& out) const { return m.display(out, *this); }
         bool operator==(pdd const& other) const { return root == other.root; }
diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index a0a8b8bf6..7cb7de457 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -90,10 +90,10 @@ namespace polysat {
 
         friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
             switch (k) {
-            case kind_t::unassigned: return out << "unassigned"; break;
-            case kind_t::propagation: return out << "propagation"; break;
-            case kind_t::decision: return out << "decision"; break;
-            default: UNREACHABLE();
+            case kind_t::unassigned: return out << "unassigned"; 
+            case kind_t::propagation: return out << "propagation"; 
+            case kind_t::decision: return out << "decision"; 
+            default: UNREACHABLE(); return out;
             }
          }
     };
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 70cd1703b..3a02d76ce 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -281,6 +281,11 @@ namespace polysat {
             return;
         if (!c.is_currently_false(s))
             return;
+
+        return;
+#if 0
+        
+        TODO - fix for new subst
         assignment_t a;
         for (auto v : m_vars)
             a.push_back(std::make_pair(v, s.get_value(v)));
@@ -302,6 +307,7 @@ namespace polysat {
         for (auto const& [v, val] : a)
             m_vars.insert(v);
         LOG("reduced " << m_vars);
+#endif
     }
 
 
diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 62996793a..c7657a443 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -137,14 +137,6 @@ namespace polysat {
         return {lookup(lit.var()), lit};
     }
 
-    bool signed_constraint::is_currently_false(solver& s) const { 
-        return is_currently_false(s.assignment());
-    }
-
-    bool signed_constraint::is_currently_true(solver& s) const { 
-        return is_currently_true(s.assignment());
-    }
-
     /** Look up constraint among stored constraints. */
     constraint* constraint_manager::dedup(constraint* c1) {
         constraint* c2 = nullptr;
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 3f8e9d73d..753a9054f 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -174,8 +174,8 @@ namespace polysat {
         bool propagate(solver& s, bool is_positive, pvar v);
         virtual void propagate_core(solver& s, bool is_positive, pvar v, pvar other_v);
         virtual bool is_always_false(bool is_positive) const = 0;
-        virtual bool is_currently_false(assignment_t const& a, bool is_positive) const = 0;
-        virtual bool is_currently_true(assignment_t const& a, bool is_positive) const = 0;
+        virtual bool is_currently_false(solver& s, bool is_positive) const = 0;
+        virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
         virtual void narrow(solver& s, bool is_positive) = 0;
         virtual inequality as_inequality(bool is_positive) const = 0;
 
@@ -241,10 +241,8 @@ namespace polysat {
         void propagate_core(solver& s, pvar v, pvar other_v) { get()->propagate_core(s, is_positive(), v, other_v); }
         bool is_always_false() const { return get()->is_always_false(is_positive()); }
         bool is_always_true() const { return get()->is_always_false(is_negative()); }        
-        bool is_currently_false(solver& s) const;
-        bool is_currently_true(solver& s) const;
-        bool is_currently_false(assignment_t const& a) const { return get()->is_currently_false(a, is_positive()); }
-        bool is_currently_true(assignment_t const& a) const { return get()->is_currently_true(a, is_positive()); }
+        bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
+        bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); }
         lbool bvalue(solver& s) const;
         unsigned level(solver& s) const { return get()->level(s); }
         void narrow(solver& s) { get()->narrow(s, is_positive()); }
diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index 1960079e0..57e766069 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -111,13 +111,13 @@ namespace polysat {
         // r := eval(q)
         // Add side constraint q = r.
         if (!q.is_val()) {
-            pdd r = q.subst_val(s.assignment());
+            pdd r = s.subst(q);
             if (!r.is_val())
                 return std::tuple(false, rational(0), q, e);
             out_side_cond.push_back(s.eq(q, r));
             q = r;
         }
-        auto b = e.subst_val(s.assignment());
+        auto b = s.subst(e); 
         return std::tuple(b.is_val(), q.val(), e, b);
     };
 
diff --git a/src/math/polysat/mul_ovfl_constraint.cpp b/src/math/polysat/mul_ovfl_constraint.cpp
index 33b2b1113..b07f1efa6 100644
--- a/src/math/polysat/mul_ovfl_constraint.cpp
+++ b/src/math/polysat/mul_ovfl_constraint.cpp
@@ -81,18 +81,19 @@ namespace polysat {
         return is_always_false(is_positive, m_p, m_q);
     }
 
-    bool mul_ovfl_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
-        return is_always_false(is_positive, p().subst_val(a), q().subst_val(a));
+
+    bool mul_ovfl_constraint::is_currently_false(solver& s, bool is_positive) const {
+        return is_always_false(is_positive, s.subst(p()), s.subst(q()));
     }
 
-    bool mul_ovfl_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
-        return is_always_true(is_positive, p().subst_val(a), q().subst_val(a));
+    bool mul_ovfl_constraint::is_currently_true(solver& s, bool is_positive) const {
+        return is_always_true(is_positive, s.subst(p()), s.subst(q()));
     }
 
     void mul_ovfl_constraint::narrow(solver& s, bool is_positive) {    
-        auto p1 = p().subst_val(s.assignment());
-        auto q1 = q().subst_val(s.assignment());
-
+        auto p1 = s.subst(p());
+        auto q1 = s.subst(q());
+        
         if (is_always_false(is_positive, p1, q1)) {
             s.set_conflict({ this, is_positive });
             return;
diff --git a/src/math/polysat/mul_ovfl_constraint.h b/src/math/polysat/mul_ovfl_constraint.h
index d4484cd95..827fa6b3a 100644
--- a/src/math/polysat/mul_ovfl_constraint.h
+++ b/src/math/polysat/mul_ovfl_constraint.h
@@ -15,6 +15,8 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     class mul_ovfl_constraint final : public constraint {
         friend class constraint_manager;
 
@@ -27,7 +29,7 @@ namespace polysat {
         bool is_always_true(bool is_positive, pdd const& p, pdd const& q) const;
         bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
         lbool eval(pdd const& p, pdd const& q) const;
-
+        
     public:
         ~mul_ovfl_constraint() override {}
         pdd const& p() const { return m_p; }
@@ -35,9 +37,10 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(assignment_t const& a, bool is_positive) const override;
-        bool is_currently_true(assignment_t const& a, bool is_positive) const override;
         void narrow(solver& s, bool is_positive) override;
+        bool is_currently_false(solver & s, bool is_positive) const;
+        bool is_currently_true(solver& s, bool is_positive) const;
+
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
         bool operator==(constraint const& other) const override;
diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 98d6aa85c..71fd9c684 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -78,12 +78,12 @@ namespace polysat {
         return is_always_false(is_positive, p(), q(), r());
     }
 
-    bool op_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
-        return is_always_false(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    bool op_constraint::is_currently_false(solver& s, bool is_positive) const {
+        return is_always_false(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));        
     }
 
-    bool op_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
-        return is_always_true(is_positive, p().subst_val(a), q().subst_val(a), r().subst_val(a));
+    bool op_constraint::is_currently_true(solver& s, bool is_positive) const {
+        return is_always_true(is_positive, s.subst(p()), s.subst(q()), s.subst(r()));        
     }
 
     std::ostream& op_constraint::display(std::ostream& out, lbool status) const {
@@ -130,7 +130,7 @@ namespace polysat {
     void op_constraint::narrow(solver& s, bool is_positive) {
         SASSERT(is_positive);
 
-        if (is_currently_true(s.assignment(), is_positive))
+        if (is_currently_true(s, is_positive))
             return;
 
         switch (m_op) {
@@ -144,7 +144,7 @@ namespace polysat {
             NOT_IMPLEMENTED_YET();
             break;
         }
-        if (!s.is_conflict() && is_currently_false(s.assignment(), is_positive))
+        if (!s.is_conflict() && is_currently_false(s, is_positive))
             s.set_conflict(signed_constraint(this, is_positive));
     }
 
@@ -180,9 +180,9 @@ namespace polysat {
      * when r, q are variables.
      */
     void op_constraint::narrow_lshr(solver& s) {
-        auto pv = p().subst_val(s.assignment());
-        auto qv = q().subst_val(s.assignment());
-        auto rv = r().subst_val(s.assignment());
+        auto pv = s.subst(p());
+        auto qv = s.subst(q());
+        auto rv = s.subst(r());
         unsigned K = p().manager().power_of_2();
 
         signed_constraint lshr(this, true);
@@ -253,10 +253,10 @@ namespace polysat {
     * q = max_value => p = r
     */
     void op_constraint::narrow_and(solver& s) {
-        auto pv = p().subst_val(s.assignment());
-        auto qv = q().subst_val(s.assignment());
-        auto rv = r().subst_val(s.assignment());
-
+        auto pv = s.subst(p());
+        auto qv = s.subst(q());
+        auto rv = s.subst(r());
+        
         signed_constraint andc(this, true);
         if (pv.is_val() && rv.is_val() && rv.val() > pv.val())
             s.add_clause(~andc, s.ule(r(), p()), true);
diff --git a/src/math/polysat/op_constraint.h b/src/math/polysat/op_constraint.h
index 45e73e9c7..c80d47933 100644
--- a/src/math/polysat/op_constraint.h
+++ b/src/math/polysat/op_constraint.h
@@ -23,6 +23,8 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     class op_constraint final : public constraint {
     public:
         enum class code { lshr_op, ashr_op, shl_op, and_op, or_op, xor_op, not_op };
@@ -54,8 +56,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(assignment_t const& a, bool is_positive) const override;
-        bool is_currently_true(assignment_t const& a, bool is_positive) const override;
+        bool is_currently_false(solver& s, bool is_positive) const override;
+        bool is_currently_true(solver& s, bool is_positive) const override;
         void narrow(solver& s, bool is_positive) override;
         inequality as_inequality(bool is_positive) const override { throw default_exception("is not an inequality"); }
         unsigned hash() const override;
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index a87ce9f47..3d884d0e3 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -13,6 +13,7 @@ Author:
 --*/
 
 #include "math/polysat/search_state.h"
+#include "math/polysat/solver.h"
 
 namespace polysat {
 
@@ -44,15 +45,33 @@ namespace polysat {
                 return true;
             }
         return false;
-    }   
+    }
 
     void search_state::push_assignment(pvar p, rational const& r) {
         m_items.push_back(search_item::assignment(p));
         m_assignment.push_back({p, r});
+        auto& m = s.var2pdd(p);
+        unsigned sz = s.size(p);
+        pdd& s = assignment(sz);
+        m_subst_trail.push_back(s);
+        s = s.subst_add(p, r);
+        SASSERT(s == *m_subst[sz]);
+    }
+
+    pdd& search_state::assignment(unsigned sz) const {
+        m_subst.reserve(sz + 1);
+        if (!m_subst[sz])
+            m_subst.set(sz, alloc(pdd, s.sz2pdd(sz).one()));
+        return *m_subst[sz];
     }
 
     void search_state::pop_assignment() {
         m_assignment.pop_back();
+        pdd& s = m_subst_trail.back();
+        auto& m = s.manager();
+        unsigned sz = m.power_of_2();
+        *m_subst[sz] = s;
+        m_subst_trail.pop_back();
     }
 
     void search_state::push_boolean(sat::literal lit) {
@@ -62,7 +81,7 @@ namespace polysat {
     void search_state::pop() {
         auto const& item = m_items.back();
         if (item.is_assignment() && !m_assignment.empty() && item.var() == m_assignment.back().first) 
-            m_assignment.pop_back();        
+            pop_assignment();
         m_items.pop_back();
     }
 
diff --git a/src/math/polysat/search_state.h b/src/math/polysat/search_state.h
index bb66bb8f2..0d704d922 100644
--- a/src/math/polysat/search_state.h
+++ b/src/math/polysat/search_state.h
@@ -20,6 +20,8 @@ namespace polysat {
     typedef std::pair<pvar, rational> assignment_item_t;
     typedef vector<assignment_item_t> assignment_t;
 
+    class solver;
+
     enum class search_item_k
     {
         assignment,
@@ -49,18 +51,23 @@ namespace polysat {
     };
 
     class search_state {
+        solver&             s;
 
         vector<search_item> m_items;
         assignment_t        m_assignment;  // First-order part of the search state
-        
+        mutable scoped_ptr_vector<pdd>         m_subst;
+        vector<pdd>         m_subst_trail;
+
         bool value(pvar v, rational& r) const;
 
     public:
+        search_state(solver& s): s(s) {}
         unsigned size() const { return m_items.size(); }
         search_item const& back() const { return m_items.back(); }
         search_item const& operator[](unsigned i) const { return m_items[i]; }
 
         assignment_t const& assignment() const { return m_assignment; }
+        pdd& assignment(unsigned sz) const;        
 
         void push_assignment(pvar p, rational const& r);
         void push_boolean(sat::literal lit);
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index cf66b3c48..e44699a3f 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -38,7 +38,8 @@ namespace polysat {
         m_forbidden_intervals(*this),
         m_bvars(),
         m_free_pvars(m_activity),
-        m_constraints(m_bvars) {
+        m_constraints(m_bvars),
+        m_search(*this) {
     }
 
     solver::~solver() {
@@ -82,7 +83,7 @@ namespace polysat {
         return l_undef;
     }
 
-    dd::pdd_manager& solver::sz2pdd(unsigned sz) {
+    dd::pdd_manager& solver::sz2pdd(unsigned sz) const {
         m_pdd.reserve(sz + 1);
         if (!m_pdd[sz])
             m_pdd.set(sz, alloc(dd::pdd_manager, 1000, dd::pdd_manager::semantics::mod2N_e, sz));
@@ -901,7 +902,7 @@ namespace polysat {
     }
 
     bool solver::try_eval(pdd const& p, rational& out_value) const {
-        pdd r = p.subst_val(assignment());
+        pdd r = subst(p);
         if (r.is_val())
             out_value = r.val();
         return r.is_val();
@@ -1010,6 +1011,13 @@ namespace polysat {
         return true;
     }
 
+    pdd solver::subst(pdd const& p) const {
+        unsigned sz = p.manager().power_of_2();
+        pdd const& s = m_search.assignment(sz);
+        return p.subst_val(s);
+    }
+
+
     /** Check that boolean assignment and constraint evaluation are consistent */
     bool solver::assignment_invariant() {
         if (is_conflict())
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 0681ea4c1..1d676ca22 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -69,20 +69,20 @@ namespace polysat {
         friend class forbidden_intervals;
         friend class linear_solver;
         friend class viable;
-        friend class viable2;
+        friend class search_state;
         friend class assignment_pp;
         friend class assignments_pp;
         friend class ex_polynomial_superposition;
-        friend class inf_saturate;
+        friend class inf_saturate;        
         friend class constraint_manager;
-        friend class scoped_solverv;
+        friend class scoped_solverv;        
         friend class test_polysat;
         friend class test_fi;
 
         reslimit&                m_lim;
         params_ref               m_params;
 
-        scoped_ptr_vector<dd::pdd_manager> m_pdd;
+        mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
         viable                   m_viable;   // viable sets per variable
         linear_solver            m_linear_solver;
         conflict                 m_conflict; 
@@ -115,6 +115,7 @@ namespace polysat {
 
         search_state             m_search;
         assignment_t const& assignment() const { return m_search.assignment(); }
+        pdd subst(pdd const& p) const; 
 
         unsigned                 m_qhead = 0; // next item to propagate (index into m_search)
         unsigned                 m_level = 0;
@@ -145,7 +146,7 @@ namespace polysat {
 
         void del_var();
 
-        dd::pdd_manager& sz2pdd(unsigned sz);
+        dd::pdd_manager& sz2pdd(unsigned sz) const;
         dd::pdd_manager& var2pdd(pvar v);
 
         void push_level();
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 4e7510aff..ba69cd734 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -122,9 +122,9 @@ namespace polysat {
     }
 
     void ule_constraint::narrow(solver& s, bool is_positive) {
-        auto p = lhs().subst_val(s.assignment());
-        auto q = rhs().subst_val(s.assignment());
-
+        auto p = s.subst(lhs());
+        auto q = s.subst(rhs());
+        
         signed_constraint sc(this, is_positive);
 
         LOG_H3("Narrowing " << sc);
@@ -190,15 +190,15 @@ namespace polysat {
         return is_always_false(is_positive, lhs(), rhs());
     }
 
-    bool ule_constraint::is_currently_false(assignment_t const& a, bool is_positive) const {
-        auto p = lhs().subst_val(a);
-        auto q = rhs().subst_val(a);
+    bool ule_constraint::is_currently_false(solver& s, bool is_positive) const {
+        auto p = s.subst(lhs());
+        auto q = s.subst(rhs());
         return is_always_false(is_positive, p, q);
     }
 
-    bool ule_constraint::is_currently_true(assignment_t const& a, bool is_positive) const {
-        auto p = lhs().subst_val(a);
-        auto q = rhs().subst_val(a);
+    bool ule_constraint::is_currently_true(solver& s, bool is_positive) const {
+        auto p = s.subst(lhs());
+        auto q = s.subst(rhs());
         if (is_positive) {
             if (p.is_zero())
                 return true;
@@ -208,6 +208,7 @@ namespace polysat {
             return p.is_val() && q.is_val() && p.val() > q.val();
     }
 
+
     inequality ule_constraint::as_inequality(bool is_positive) const {
         if (is_positive)
             return inequality(lhs(), rhs(), false, this);
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index 69af886e8..ca2492152 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -17,6 +17,8 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     class ule_constraint final : public constraint {
         friend class constraint_manager;
 
@@ -34,8 +36,8 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const override;
         bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const;
         bool is_always_false(bool is_positive) const override;
-        bool is_currently_false(assignment_t const& a, bool is_positive) const override;
-        bool is_currently_true(assignment_t const& a, bool is_positive) const override;
+        bool is_currently_false(solver& s, bool is_positive) const override;
+        bool is_currently_true(solver& s, bool is_positive) const override;
         void narrow(solver& s, bool is_positive) override;
         inequality as_inequality(bool is_positive) const override;
         unsigned hash() const override;
diff --git a/src/test/pdd.cpp b/src/test/pdd.cpp
index bc5ecbd5f..0a5126807 100644
--- a/src/test/pdd.cpp
+++ b/src/test/pdd.cpp
@@ -309,10 +309,10 @@ public :
         sub1.push_back(std::make_pair(va, rational(1)));
         sub2.push_back(std::make_pair(va, rational(2)));
         sub3.push_back(std::make_pair(va, rational(3)));
-        std::cout << "sub 0 " << p.subst_val(sub0) << "\n";
-        std::cout << "sub 1 " << p.subst_val(sub1) << "\n";
-        std::cout << "sub 2 " << p.subst_val(sub2) << "\n";
-        std::cout << "sub 3 " << p.subst_val(sub3) << "\n";
+        std::cout << "sub 0 " << p.subst_val0(sub0) << "\n";
+        std::cout << "sub 1 " << p.subst_val0(sub1) << "\n";
+        std::cout << "sub 2 " << p.subst_val0(sub2) << "\n";
+        std::cout << "sub 3 " << p.subst_val0(sub3) << "\n";
 
         std::cout << "expect 1 " << (2*a + 1).is_never_zero() << "\n";
         std::cout << "expect 1 " << (2*a*b + 2*b + 1).is_never_zero() << "\n";
@@ -538,7 +538,7 @@ public :
             pdd const p = 2*a + b + 1;
             SASSERT(p.subst_val(va, rational(0)) == b + 1);
         }
-
+        
         {
             pdd const p = a + 2*b;
             SASSERT(p.subst_val(va, rational(0)) == 2*b);
@@ -555,7 +555,7 @@ public :
             vector<std::pair<unsigned, rational>> sub;
             sub.push_back({vb, rational(2)});
             sub.push_back({vc, rational(3)});
-            SASSERT(p.subst_val(sub) == a + d + 1);
+            SASSERT(p.subst_val0(sub) == a + d + 1);
         }
 
         {
@@ -563,10 +563,10 @@ public :
             vector<std::pair<unsigned, rational>> sub;
             sub.push_back({vb, rational(2)});
             sub.push_back({vc, rational(3)});
-            SASSERT(p.subst_val(sub) == (a + 2) * (d + 3));
+            SASSERT(p.subst_val0(sub) == (a + 2) * (d + 3));
             sub.push_back({va, rational(3)});
             sub.push_back({vd, rational(2)});
-            SASSERT(p.subst_val(sub) == m.one());
+            SASSERT(p.subst_val0(sub) == m.one());
         }
     }
 
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index aae954cf7..33edc45fd 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -85,8 +85,8 @@ namespace polysat {
             LOG(m_name << ": " << m_last_result << "\n");
             statistics st;
             collect_statistics(st);
-            // LOG(st << "\n" << *this << "\n");
-            std::cout << st << "\n" << *this << "\n";
+            LOG(st << "\n" << *this << "\n");
+            std::cout << st << "\n";
         }
 
         void expect_unsat() {
@@ -1321,17 +1321,16 @@ public:
 void tst_polysat() {
     using namespace polysat;
 
-    test_fi::exhaustive();
-    test_fi::randomized();
-    return;
+    test_polysat::test_l2();
 
+#if 0
     // looks like a fishy conflict lemma?
     test_polysat::test_monot_bounds();
-    return;
+     return;
 
     test_polysat::test_quot_rem_incomplete();
     test_polysat::test_quot_rem_fixed();
-    return;
+    //return;
 
     test_polysat::test_band();
     return;
@@ -1347,6 +1346,8 @@ void tst_polysat() {
     test_polysat::test_ineq_axiom6();
     return;
 
+#endif
+
     test_polysat::test_ineq_basic4();
     //return;
 
@@ -1390,6 +1391,11 @@ void tst_polysat() {
     test_polysat::test_ineq_axiom4();
     test_polysat::test_ineq_axiom5();
     test_polysat::test_ineq_axiom6();
+
+    test_fi::exhaustive();
+    test_fi::randomized();
+    return;
+
 #if 0
     test_polysat::test_ineq_non_axiom4(32, 5);
 #endif