From 827374952bf0b56c5f17138fca71ec902a497dfc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Mar 2023 10:47:05 -0800
Subject: [PATCH] fix test for non-val node

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

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index c3f38d5ba..9e3c8d44f 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1591,7 +1591,7 @@ namespace polysat {
         if (y == null_var) {
             // choose the top variable
             y = q.var();
-            if (q.hi().is_var() && q.hi().var() == y)
+            if (!q.hi().is_val() && q.hi().var() == y)
                 return false;
             if (!eval_round(M, q.hi(), a))
                 return false;