diff --git a/include/klee/ADT/ImmutableList.h b/include/klee/ADT/ImmutableList.h
index 425036979e..73ce89f448 100644
--- a/include/klee/ADT/ImmutableList.h
+++ b/include/klee/ADT/ImmutableList.h
@@ -47,16 +47,10 @@ template <typename T> class ImmutableList {
 
   struct iterator {
     const ImmutableListNode *rootNode;
-    std::unique_ptr<iterator> it;
     size_t get;
 
   public:
-    explicit iterator(const ImmutableListNode *p)
-        : rootNode(p), it(nullptr), get(0) {
-      if (rootNode && rootNode->prev.get()) {
-        it = std::make_unique<iterator>(rootNode->prev.get());
-      }
-    }
+    explicit iterator(const ImmutableListNode *p) : rootNode(p), get(0) {}
 
     bool operator==(const iterator &b) const {
       return rootNode == b.rootNode && get == b.get;
@@ -66,17 +60,16 @@ template <typename T> class ImmutableList {
 
     iterator &operator++() {
       ++get;
-      if (get < rootNode->prev_len) {
-        it->operator++();
-      }
       return *this;
     }
 
     const T &operator*() const {
-      if (get < rootNode->prev_len) {
-        return **it;
+      assert(get < rootNode->size() && "Out of bound");
+      const ImmutableListNode *curNode = rootNode;
+      while (get < curNode->prev_len) {
+        curNode = curNode->prev.get();
       }
-      return rootNode->values[get - rootNode->prev_len];
+      return curNode->values[get - curNode->prev_len];
     }
 
     const T &operator->() const { return **this; }