[fix] Clean _arr_hash as well

UnitTestBot · Nov 2, 2023 · ad1841e · ad1841e
1 parent bf66f57
commit ad1841e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
@@ -218,7 +218,10 @@ class Z3Builder {
       clearConstructCache();
     return res;
   }
-  void clearConstructCache() { constructed.clear(); }
+  void clearConstructCache() {
+    constructed.clear();
+    _arr_hash.clear();
+  }
   void clearSideConstraints() { sideConstraints.clear(); }
 };
 } // namespace klee

diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
@@ -551,8 +551,6 @@ bool Z3SolverImpl::internalRunSolver(
     }
 
     for (auto constant_array : constant_arrays_in_query.results) {
-      // assert(builder->constant_array_assertions.count(constant_array) == 1 &&
-      //        "Constant array found in query, but not handled by Z3Builder");
       if (all_constant_arrays_in_query.count(constant_array))
         continue;
       all_constant_arrays_in_query.insert(constant_array);