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, 3 insertions, 1 deletions

diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
index e1937158..0e51967e 100644
--- a/lib/Solver/Z3Builder.cpp
+++ b/lib/Solver/Z3Builder.cpp
@@ -394,7 +394,9 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
     // Unique arrays by name, so we make sure the name is unique by
     // using the size of the array hash as a counter.
     std::string unique_id = llvm::utostr(_arr_hash._array_hash.size());
-    std::string unique_name = root->name + unique_id;
+    // Prefix unique ID with '_' to avoid name collision if name ends with
+    // number
+    std::string unique_name = root->name + "_" + unique_id;
 
     array_expr = buildArray(unique_name.c_str(), root->getDomain(),
                             root->getRange());