New invariant for dlist (#7294)

* unit tests for dlist.h

* new invariant for dlist: should be circular. avoid infinite loop

* remove dlist test commit

* format

* format

* Update dlist.h

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/util/dlist.h

@@ -155,15 +155,23 @@ class dll_base {
         elem->init(elem);
     }
 
-    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;
+    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; 
     }
 
     static bool contains(T const* list, T const* elem) {