From f813c88c8cb868fc9c0be78fbf92a94d72ac02b0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Mon, 20 Nov 2023 22:41:19 +0000 Subject: Avoid generating array names in solver builders that could accidently collide If an array name ended with a number, adding a number-only suffix could generate the same name used as part of the solvers. In the specific testcase `val_1` became solver array `val_111` which collided with array `val_11` that became `val_111` as well. Using an `_` as prefix for the suffix, solves that problem in general, i.e. `val_1` becomes `val_1_11` and `val_11` becomes `val_11_1`. Fixes #1668 --- unittests/Solver/Z3SolverTest.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'unittests/Solver') diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index e81ff19e..0eba3d0e 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -64,7 +64,7 @@ TEST_F(Z3SolverTest, GetConstraintLog) { // Ensure this is not buggy as fixed in https://github.com/klee/klee/pull/1235 // If the bug is still present this fail due to an internal assertion char *ConstraintsString = Z3Solver_->getConstraintLog(TheQuery); - const char *ExpectedArraySelection = "(= (select const_array0"; + const char *ExpectedArraySelection = "(= (select const_array_0"; const char *Occurence = std::strstr(ConstraintsString, ExpectedArraySelection); ASSERT_STRNE(Occurence, nullptr); free(ConstraintsString); -- cgit 1.4.1