diff options
author | Daniel Grumberg <dany.grumberg@gmail.com> | 2020-03-19 14:48:01 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-03-27 20:34:34 +0000 |
commit | 928fd62aed9d1f2b6e7617de8ba0604b415f62ab (patch) | |
tree | 98902cd974ea35b514748c4ed92932122ded0833 /lib/Solver/Z3Solver.cpp | |
parent | 4030052bbd3f8a4682590ca6fb3a9faf5aec483d (diff) | |
download | klee-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.cpp | 4 |
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); } } |