From 450ed26440ce87b8b550dd05fb5a63c956e65ac4 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Tue, 12 Mar 2024 16:23:23 +0100
Subject: [PATCH] implement 'is_full' case

---
 src/sat/smt/polysat/viable.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 29738315e..b4dff4454 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -892,8 +892,9 @@ namespace polysat {
         });
 
         if (ivl.is_full()) {
-            // TODO: set conflict
-            NOT_IMPLEMENTED_YET();
+            pdd zero = c.var2pdd(m_var).zero();
+            auto sc = cs.ult(zero, zero);  // false
+            return c.propagate(sc, deps, "propagate from containing slice (conflict)");
         }
         else {
             // proper interval