From 6f183356045ec68fb94f2b299684a0f942881503 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 5 Jan 2023 16:43:23 +0100
Subject: [PATCH] need y0 value

---
 src/math/polysat/saturation.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index 62b802b7c..69d1f5c20 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1700,6 +1700,8 @@ namespace polysat {
         if (y1 == null_var && y2 == null_var)
             return false;
         y = (y1 == null_var) ? y2 : y1;
+        if (!s.is_assigned(y))
+            return false;
         rational y0 = s.get_value(y);
 
         vector<signed_constraint> bounds;