From 23963f274dcfbda495c528d78d5a812feebac42a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Sep 2021 04:58:00 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/solver.cpp | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 750f083d5..221dc3612 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -532,18 +532,13 @@ namespace polysat {
             case l_true:
                 return;
             case l_false:
-                continue;
-            default:                
-                
-                if (lit2cnstr(lit).is_currently_false(*this)) {
-                    num_choices++;
-                    continue;
-                }
+                break;
+            case l_undef:
+                num_choices++;                
+                if (!lit2cnstr(lit).is_currently_false(*this)) 
+                    choice = lit;
                 break;
             }
-            num_choices++;
-            if (choice == sat::null_literal)
-                choice = lit;
         }
         LOG_V("num_choices: " << num_choices);
         if (choice == sat::null_literal) {