diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index 7b407c6e3da..28b0025398c 100644 --- 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 index a485ebe83ed..a4d74cbf5c0 100644 --- 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);