From dc023e723120369fa3964e9b702b83927dc39089 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 21 Jul 2024 21:06:26 -0700
Subject: [PATCH] Revert "new heap invariants (#7298)"

This reverts commit 80ac7b34387cddb88f2286b0716dd44ede982b78.
---
 src/test/heap.cpp | 24 +++++++++++-------------
 src/util/heap.h   | 13 -------------
 2 files changed, 11 insertions(+), 26 deletions(-)

diff --git a/src/test/heap.cpp b/src/test/heap.cpp
index f30f45c32cc..6a5bc7b9ffe 100644
--- a/src/test/heap.cpp
+++ b/src/test/heap.cpp
@@ -38,7 +38,7 @@ static void tst1() {
     for (int i = 0; i < N * 3; i++) {
         int val = heap_rand() % N;
         if (!h.contains(val)) {
-            VERIFY(!t.contains(val));
+            ENSURE(!t.contains(val));
             h.insert(val);
             t.insert(val);
         }
@@ -46,26 +46,26 @@ static void tst1() {
             if (!t.contains(val)) {
                 for (int v : t) std::cout << v << "\n";
             }
-            VERIFY(t.contains(val));
+            ENSURE(t.contains(val));
         }
     }
-    VERIFY(h.check_invariant());
+    ENSURE(h.check_invariant());
     for (int v : t) {
-        VERIFY(h.contains(v));
+        ENSURE(h.contains(v));
     }
     while (!h.empty()) {
         int m1 = h.min_value();
         int m2 = h.erase_min();
         (void)m1;
         (void)m2;
-        VERIFY(m1 == m2);
-        VERIFY(-1 < m2);
+        ENSURE(m1 == m2);
+        ENSURE(-1 < m2);
     }
 }
 
 int g_value[N];
 
-struct lt_proc2 { bool operator()(int v1, int v2) const { VERIFY(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } };
+struct lt_proc2 { bool operator()(int v1, int v2) const { ENSURE(v1 < N && v2 < N); return g_value[v1] < g_value[v2]; } };
 typedef heap<lt_proc2> int_heap2;
 
 static void init_values() {
@@ -98,7 +98,7 @@ static void tst2() {
                 TRACE("heap", tout << "inserting: " << val << "\n";);
                 h.insert(val);
                 TRACE("heap", dump_heap(h, tout););
-                VERIFY(h.contains(val));
+                ENSURE(h.contains(val));
             }
         }
         else if (cmd <= 6) {
@@ -107,7 +107,7 @@ static void tst2() {
                 TRACE("heap", tout << "removing: " << val << "\n";);
                 h.erase(val);
                 TRACE("heap", dump_heap(h, tout););
-                VERIFY(!h.contains(val));
+                ENSURE(!h.contains(val));
             }
         }
         else if (cmd <= 8) {
@@ -128,12 +128,10 @@ static void tst2() {
             }
         }
         else {
-            VERIFY(h.check_invariant());
+            ENSURE(h.check_invariant());
         }
     }
-    VERIFY(h.check_invariant());
-    h.reset();
-    VERIFY(h.check_invariant());
+    ENSURE(h.check_invariant());
 }
 
 void tst_heap() {
diff --git a/src/util/heap.h b/src/util/heap.h
index 3bee2fe9f67..c080c6ebde9 100644
--- a/src/util/heap.h
+++ b/src/util/heap.h
@@ -55,19 +55,6 @@ class heap : private LT {
     }
 
     bool check_invariant_core(int idx) const {
-        
-        // Check that m_values starts with a dummy value at index 0.
-        if (m_values.empty() || m_values[0] != -1) {
-            return false;
-        }
-
-        // All indices in m_value2indices that are not used in m_values should be 0
-        for (int val = 0; val < static_cast<int>(m_value2indices.size()); ++val) {
-            if (std::find(m_values.begin(), m_values.end(), val) == m_values.end() && m_value2indices[val] != 0) {
-                return false; // Unused indices should have a 0 value
-            }
-        }
-
         if (idx < static_cast<int>(m_values.size())) {
             SASSERT(m_value2indices[m_values[idx]] == idx);
             SASSERT(parent(idx) == 0 || !less_than(m_values[idx], m_values[parent(idx)]));