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);