diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/STPBuilder.cpp | 8 | ||||
| -rw-r--r-- | lib/Solver/Z3Builder.cpp | 8 |
2 files changed, 4 insertions, 12 deletions
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 9fd9dc8e..13a42513 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -436,12 +436,8 @@ ExprHandle STPBuilder::constructSDivByConstant(ExprHandle expr_n, unsigned width if (!hashed) { // STP uniques 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::itostr(_arr_hash._array_hash.size()); - unsigned const uid_length = unique_id.length(); - unsigned const space = (root->name.length() > 32 - uid_length) - ? (32 - uid_length) - : root->name.length(); - std::string unique_name = root->name.substr(0, space) + unique_id; + std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); + std::string unique_name = root->name + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index ce584175..950bd879 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -392,12 +392,8 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { if (!hashed) { // 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::itostr(_arr_hash._array_hash.size()); - unsigned const uid_length = unique_id.length(); - unsigned const space = (root->name.length() > 32 - uid_length) - ? (32 - uid_length) - : root->name.length(); - std::string unique_name = root->name.substr(0, space) + unique_id; + std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); + std::string unique_name = root->name + unique_id; array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); |