From bc636d7ee00b7ead1de4e9537930fce9d85a958d Mon Sep 17 00:00:00 2001
From: LiviaSun <33578456+ChuyueSun@users.noreply.github.com>
Date: Fri, 19 Jul 2024 14:01:42 -0700
Subject: [PATCH] new hashtable.h invariants (#7296)

* add copyright for dlist unit test

* new hashtable invariants

* add copyright
---
 src/test/dlist.cpp   | 17 +++++++++++++++++
 src/util/hashtable.h | 14 ++++++++++++++
 2 files changed, 31 insertions(+)

diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
index dfc1138b7b9..200a0a3296b 100644
--- a/src/test/dlist.cpp
+++ b/src/test/dlist.cpp
@@ -1,3 +1,20 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+    tst_dlist.cpp
+
+Abstract:
+
+    Test dlist module
+
+Author:
+
+    Chuyue Sun 2024-07-18.
+
+--*/
+
 #include <cassert>
 #include <iostream>
 #include "util/dlist.h"
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index b59a2e7d835..acbe2a81865 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -12,6 +12,7 @@ Module Name:
 Author:
 
     Leonardo de Moura (leonardo) 2006-09-11.
+    Chuyue Sun (liviasun) 2024-07-18.
 
 Revision History:
 
@@ -639,6 +640,19 @@ class core_hashtable : private HashProc, private EqProc {
 
 #ifdef Z3DEBUG
     bool check_invariant() {
+        // The capacity must always be a power of two.
+        if (!is_power_of_two(m_capacity))
+            return false;
+
+        // The number of deleted plus the size must not exceed the capacity.
+        if (m_num_deleted + m_size > m_capacity)
+            return false;
+
+        // Checking that m_num_deleted is less than or equal to m_size.
+        if (m_num_deleted > m_size) {
+            return false;
+        }
+
         entry * curr = m_table;
         entry * end  = m_table + m_capacity;
         unsigned num_deleted = 0;