From 928fd62aed9d1f2b6e7617de8ba0604b415f62ab Mon Sep 17 00:00:00 2001 From: Daniel Grumberg Date: Thu, 19 Mar 2020 14:48:01 +0000 Subject: Ensure that temp_builder is used when adding constant array value assertion constraints --- lib/Solver/Z3Solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib/Solver') 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); } } -- cgit 1.4.1