From ee208efdc55c5bdae685bdefe4491212a377ca64 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 19 Aug 2022 16:18:13 +0200
Subject: [PATCH] fix

---
 src/math/polysat/solver.cpp | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 96deda234..b1c34a21b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1245,11 +1245,14 @@ namespace polysat {
         }
 
         if (all_unit) {
+            SASSERT(!intersection.is_currently_empty());
             // Unit intervals from all constraints
             // => build constraint from intersection of forbidden intervals
             //    z \not\in [l;u[  <=>  z - l >= u - l
-            auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
-            out_lits.push_back(c_new.blit());
+            if (intersection.is_proper()) {
+                auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
+                out_lits.push_back(c_new.blit());
+            }
             return;
         } else {
             out_lits.shrink(out_lits_original_size);