about summary refs log tree commit diff homepage
path: root/lib/Solver/Z3Solver.cpp
diff options
context:
space:
mode:
authorDaniel Grumberg <dany.grumberg@gmail.com>2020-03-19 14:48:01 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-03-27 20:34:34 +0000
commit928fd62aed9d1f2b6e7617de8ba0604b415f62ab (patch)
tree98902cd974ea35b514748c4ed92932122ded0833 /lib/Solver/Z3Solver.cpp
parent4030052bbd3f8a4682590ca6fb3a9faf5aec483d (diff)
downloadklee-928fd62aed9d1f2b6e7617de8ba0604b415f62ab.tar.gz
Ensure that temp_builder is used when adding constant array value assertion constraints
Diffstat (limited to 'lib/Solver/Z3Solver.cpp')
-rw-r--r--lib/Solver/Z3Solver.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 00777a78..e95ad7f4 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -172,10 +172,10 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) {
   constant_arrays_in_query.visit(query.expr);
 
   for (auto const &constant_array : constant_arrays_in_query.results) {
-    assert(builder->constant_array_assertions.count(constant_array) == 1 &&
+    assert(temp_builder.constant_array_assertions.count(constant_array) == 1 &&
            "Constant array found in query, but not handled by Z3Builder");
     for (auto const &arrayIndexValueExpr :
-         builder->constant_array_assertions[constant_array]) {
+         temp_builder.constant_array_assertions[constant_array]) {
       assumptions.push_back(arrayIndexValueExpr);
     }
   }