From 5003d41cdbc392eacea5d73d1065259ec9a0dadf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 19 Jul 2024 19:11:54 -0700
Subject: [PATCH] Revert "New invariant for dlist (#7294)" (#7301)

This reverts commit cf4d0e74a53428192d5c4cb8d5a033431828deb2.
---
 src/util/dlist.h | 26 +++++++++-----------------
 1 file changed, 9 insertions(+), 17 deletions(-)

diff --git a/src/util/dlist.h b/src/util/dlist.h
index 52cb25548d4..4c0e51e5898 100644
--- a/src/util/dlist.h
+++ b/src/util/dlist.h
@@ -155,23 +155,15 @@ class dll_base {
         elem->init(elem);
     }
 
-    bool invariant() const { 
-        auto* e = this; 
-        const T* slow = static_cast<const T*>(this); 
-        const T* fast = m_next; 
-        bool looped = false; 
-        // m_next of each node should point back to m_prev of the following node,
-        // and m_prev of each node should point forward to m_next of the preceding node.
-        while (slow != fast) { 
-            if (fast->m_prev->m_next != fast || fast->m_next->m_prev != fast) 
-                return false;             
-            fast = fast->m_next; 
-            looped = looped || (fast == static_cast<const T*>(this)); 
-            if (!looped && fast == m_next)  
-                // We should be able to traverse back to the starting node. 
-                return false;             
-        } 
-        return true; 
+    bool invariant() const {
+        auto* e = this;
+        do {
+            if (e->m_next->m_prev != e)
+                return false;
+            e = e->m_next;
+        }
+        while (e != this);
+        return true;
     }
 
     static bool contains(T const* list, T const* elem) {