diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h
index 0f210e121..68aa34ee6 100644
--- a/src/math/polysat/boolean.h
+++ b/src/math/polysat/boolean.h
@@ -100,10 +100,11 @@ namespace polysat {
 
         friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
             switch (k) {
-            case kind_t::unassigned: return out << "unassigned"; 
-            case kind_t::bool_propagation: return out << "bool propagation"; 
-            case kind_t::value_propagation: return out << "value propagation"; 
-            case kind_t::decision: return out << "decision"; 
+            case kind_t::unassigned: return out << "unassigned";
+            case kind_t::bool_propagation: return out << "bool propagation";
+            case kind_t::value_propagation: return out << "value propagation";
+            case kind_t::decision: return out << "decision";
+            case kind_t::assumption: return out << "assumption";
             default: UNREACHABLE(); return out;
             }
          }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 9d3ef404f..cce6eb318 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -513,15 +513,18 @@ namespace polysat {
         m_search.pop();
         m_justification[v] = justification::unassigned();
         if (!is_valid) {
+            LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
             // Try to find a valid replacement value
             switch (m_viable_fallback.find_viable(v, val)) {
             case dd::find_t::singleton:
             case dd::find_t::multiple:
+                LOG("Fallback solver: " << assignment_pp(*this, v, val));
                 // NOTE: I don't think this can happen if viable::find_viable returned a singleton. since all values excluded by viable are true negatives.
                 SASSERT(!j.is_propagation());
                 j = justification::decision(m_level + 1);
                 break;
             case dd::find_t::empty:
+                LOG("Fallback solver: unsat");
                 m_free_pvars.unassign_var_eh(v);
                 auto core = m_viable_fallback.unsat_core(v);  // TODO: add constraints from unsat_core to conflict
                 set_conflict(v);
diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index fe46c50af..7851e208c 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -29,17 +29,19 @@ namespace polysat {
 
     class univariate_bitblast_solver : public univariate_solver {
         // TODO: does it make sense to share m and bv between different solver instances?
+        // TODO: consider pooling solvers to save setup overhead, see if solver/solver_pool.h can be used
         ast_manager m;
         scoped_ptr<bv_util> bv;
         scoped_ptr<solver> s;
         unsigned bit_width;
-        func_decl* x_decl;
-        expr* x;
+        func_decl_ref x_decl;
+        expr_ref x;
 
     public:
         univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
-            bit_width(bit_width)
-        {
+            bit_width(bit_width),
+            x_decl(m),
+            x(m) {
             // m.register_plugin(symbol("bv"), alloc(bv_decl_plugin));  // this alone doesn't work
             reg_decl_plugins(m);
             bv = alloc(bv_util, m);