From adf41c5d020246d43d94eb4025ad9c31fef6aefd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 24 Nov 2021 13:37:15 +0100
Subject: [PATCH] another bug fix

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/viable.cpp | 12 ++++++------
 src/test/polysat.cpp        |  1 +
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index f9ed09f28..a8c5fc42e 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -141,7 +141,7 @@ namespace polysat {
         SASSERT(well_formed(m_viable[v]));
     }
 
-    bool viable::has_viable(pvar v) { 
+    bool viable::has_viable(pvar v) {         
         auto* e = m_viable[v];
         if (!e)
             return true;
@@ -150,17 +150,16 @@ namespace polysat {
 
         // quick check: last interval doesn't wrap around, so hi_val
         // has not been covered
-        if (last->interval.lo_val() < last->interval.hi_val())
-            return true;
-
-        auto const& max_value = s.var2pdd(v).max_value();
+        if (last->interval.lo_val() < last->interval.hi_val()) 
+            return true;        
+        
         do {
             if (e->interval.is_full())
                 return false;
             entry* n = e->next();
             if (n == e)
                 return true;
-            if (e->interval.hi_val() < n->interval.lo_val())
+            if (!n->interval.currently_contains(e->interval.hi_val()))
                 return true;
             if (n == first)
                 return e->interval.lo_val() <= e->interval.hi_val();
@@ -276,6 +275,7 @@ namespace polysat {
     }
 
     bool viable::resolve(pvar v, conflict& core) {
+        std::cout << "resolve " << v << "\n";
         if (has_viable(v))
             return false;
         auto* e = m_viable[v];
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index 1f6f70fc5..02a29d46a 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1068,6 +1068,7 @@ namespace polysat {
 void tst_polysat() {
 
 
+    polysat::test_ineq_basic6();
             
     // polysat::test_monot_bounds(8);