diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index 835130380..34614476f 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -154,7 +154,22 @@ namespace polysat {
     lbool core::assign_variable() {
         if (m_var_queue.empty())
             return l_true;
-        m_var = m_var_queue.min_var();
+
+        for (auto v : m_var_queue) {
+            switch (assign_variable(v)) {
+            case l_false:
+                return l_false;
+            case l_true:
+                return l_true;
+            default:
+                break;
+            }
+        }
+        return l_undef;
+    }
+
+    lbool core::assign_variable(pvar v) {
+        m_var = v;
         CTRACE("bv", is_assigned(m_var), display(tout << "v" << m_var << " is assigned\n"););
         SASSERT(!is_assigned(m_var));
 
@@ -206,11 +221,11 @@ namespace polysat {
         case l_false:
             return sat::check_result::CR_CONTINUE;
         case l_undef:
-            verbose_stream() << "giveup assign\n";
-            return sat::check_result::CR_GIVEUP;
+            // verbose_stream() << "giveup assign\n";
+            // return sat::check_result::CR_GIVEUP;
             // or:
-            // r = l_undef;
-            // break;
+            r = l_undef;
+            break;
         }
 
         saturation saturate(*this);
diff --git a/src/sat/smt/polysat/core.h b/src/sat/smt/polysat/core.h
index 4fcb09f7f..2d2944741 100644
--- a/src/sat/smt/polysat/core.h
+++ b/src/sat/smt/polysat/core.h
@@ -92,6 +92,7 @@ namespace polysat {
         void add_watch(unsigned idx, unsigned var);
 
         lbool assign_variable();
+        lbool assign_variable(pvar v);
         
         void add_opdef(signed_constraint sc);
 
diff --git a/src/sat/smt/polysat/forbidden_intervals.cpp b/src/sat/smt/polysat/forbidden_intervals.cpp
index 009630236..11f082cec 100644
--- a/src/sat/smt/polysat/forbidden_intervals.cpp
+++ b/src/sat/smt/polysat/forbidden_intervals.cpp
@@ -118,7 +118,7 @@ namespace polysat {
                 rational A = div(bound, b2.val());
                 rational B = div(bound + A, A) - 1;
 
-                if (A >= 4 && B >= 4) {
+                if (!e2.is_val() && A >= 4 && B >= 4) {
                     _backtrack.released = false;
                     return false;
                 }
@@ -149,7 +149,7 @@ namespace polysat {
                 //       := div(2^N + A - 1, A)
                 rational A = div(bound, b2.val()) + 1;
                 rational B = div(bound + A, A);
-                if (A >= 4 && B >= 4) {
+                if (!e2.is_val() && A >= 4 && B >= 4) {
                     _backtrack.released = false;
                     return false;
                 }
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 7bf9dd526..4b9445e1c 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -28,9 +28,11 @@ namespace polysat {
             lbool eval_value = c.strong_eval(sc);
             if (eval_value == l_true)
                 continue;
-
+            has_conflict = true;
+            if (eval_value == l_undef)
+                continue;
+            
             TRACE("bv", sc.display(tout << "eval: ") << " evaluates to " << eval_value << "\n");
-            SASSERT(eval_value != l_undef);
 
             has_conflict = true;
             auto vars = c.find_conflict_variables(idx);
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 32509875f..c3c663d1d 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -148,7 +148,7 @@ namespace polysat {
             }
             return find_t::multiple;                        
         }
-
+        TRACE("bv", display(tout << "resource-out v" << v << "\n"));
         return find_t::resource_out;        
     }