From 134f677ec3c04c9d84944a10328c7a8e26562edd Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 22 Dec 2023 13:25:45 +0100
Subject: [PATCH] skip empty layers

---
 src/math/polysat/viable.cpp | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index c9873e2d3..42227debc 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1518,9 +1518,9 @@ namespace polysat {
                 LOG("    v" << x << " = v" << v << "[" << hi << ":" << lo << "]");
             else
                 LOG("    v" << x << " not extracted from v" << v << "; size " << s.size(x));
-            for (layer const& l : m_units[x].get_layers()) {
-                widths_set.insert(l.bit_width);
-            }
+            for (layer const& l : m_units[x].get_layers())
+                if (l.entries)
+                    widths_set.insert(l.bit_width);
         }
 
         unsigned_vector widths;
@@ -1857,6 +1857,8 @@ namespace polysat {
         LOG("Assignment: " << assignments_pp(s));
         for (pvar x : overlaps) {
             for (layer const& l : m_units[x].get_layers()) {
+                if (!l.entries)
+                    continue;
                 entry const* first = l.entries;
                 entry const* e = first;
                 do {