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

1 files changed, 1 insertions, 1 deletions

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);