From d4abf16551d1076d06d06665ce1a10b0cb5d8f0d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 20 Sep 2021 17:38:42 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 2188cc48a..750f083d5 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -554,7 +554,7 @@ namespace polysat {
         }
 
         signed_constraint c = lit2cnstr(choice);
-        if (num_choices > 0)
+        if (num_choices > 1)
             push_level();        
         push_cjust(lemma.justified_var(), c);