From 09b0c4bc9db7548674b65357f3bbb5939c1ec289 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Apr 2022 07:17:24 +0200
Subject: [PATCH] fix #5988

---
 src/util/max_cliques.h | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/util/max_cliques.h b/src/util/max_cliques.h
index 979a5b795..576408f51 100644
--- a/src/util/max_cliques.h
+++ b/src/util/max_cliques.h
@@ -181,7 +181,7 @@ public:
                     next.push_back(n);
             std::sort(next.begin(), next.end(), [&](unsigned a, unsigned b) { return conns[a].num_elems() < conns[b].num_elems(); });
             for (unsigned x : next) {
-                bool all = true;
+                bool all = heap.contains(x);
                 for (unsigned y : am1) {
                     if (!conns[x].contains(y)) {
                         all = false;
@@ -190,15 +190,18 @@ public:
                 }
                 if (all)
                     am1.insert(x);
-            }
+            }            
             am1.insert(v);
+
             for (unsigned x : am1) {
                 todo.remove(x);
                 for (unsigned y : conns[x]) {
                     conns[y].remove(x);
-                    heap.decreased(y);
+                    if (heap.contains(y))
+                        heap.decreased(y);
                 }
             }
+            
             for (unsigned x : am1) 
                 heap.erase(x);