diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 96c9cdc93..eb764698c 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -567,6 +567,11 @@ namespace smt {
                 << (m_nielsen.sat_node() ? "set" : "null") << "\n";);
             // Nielsen found a consistent assignment for positive constraints.
             SASSERT(has_eq_or_mem); // we should have axiomatized them
+            #if 0
+            // TODO: add this pending review
+            if (!add_nielsen_assumptions())
+                return FC_CONTINUE;
+            #endif
             if (!has_unhandled_preds())
                 return FC_DONE;
         }
@@ -575,6 +580,38 @@ namespace smt {
         return FC_GIVEUP;
     }
 
+
+    bool theory_nseq::add_nielsen_assumptions() {
+        bool has_undef = false;
+        bool has_false = false;
+        for (auto const& c : m_nielsen.sat_node()->constraints()) {
+            auto lit = mk_literal(c.fml);
+            switch (ctx.get_assignment(lit)) { 
+            case l_true: break;
+            case l_undef: 
+                has_undef = true; 
+                ctx.force_phase(lit);                
+                IF_VERBOSE(2, verbose_stream() << 
+                    "nseq final_check: adding nielsen assumption " << c.fml << "\n";);
+                break;
+            case l_false: 
+                // do we really expect this to happen?
+                has_false = true; 
+                IF_VERBOSE(1, verbose_stream()
+                                  << "nseq final_check: nielsen assumption " << c.fml << " is false\n";);
+                ctx.force_phase(lit);
+                break;
+            }
+        }
+        if (has_undef)
+            return false;
+        if (has_false) {
+            // fishy case.
+            return false;
+        }
+        return true;
+    }
+
     // -----------------------------------------------------------------------
     // Conflict explanation
     // -----------------------------------------------------------------------
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index e624dceb0..cdfcd8698 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -114,6 +114,7 @@ namespace smt {
         void populate_nielsen_graph();
         void explain_nielsen_conflict();
         void set_conflict(enode_pair_vector const& eqs, literal_vector const& lits);
+        bool add_nielsen_assumptions();
         euf::snode* get_snode(expr* e);
 
         // propagation dispatch helpers