summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2015-08-15 11:45:44 +0200
committerClifford Wolf <clifford@clifford.at>2015-08-15 11:45:44 +0200
commitb659ffb4571a07db7df7c102790f850f003c9066 (patch)
tree7642a797a8f6b4e077c6a9ca3e99cc319ea6aaf5 /backends/smt2
parent1e67b2991916077260fbaf8679608c07375a19ac (diff)
Fixed generation of smt2 concat statements
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smt2.cc8
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9b1972b1..1e00ac71 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -201,10 +201,12 @@ struct Smt2Worker
}
if (GetSize(subexpr) > 1) {
- std::string expr = "(concat";
- for (int i = GetSize(subexpr)-1; i >= 0; i--)
+ std::string expr = "", end_str = "";
+ for (int i = GetSize(subexpr)-1; i >= 0; i--) {
+ if (i > 0) expr += " (concat", end_str += ")";
expr += " " + subexpr[i];
- return expr + ")";
+ }
+ return expr.substr(1) + end_str;
} else {
log_assert(GetSize(subexpr) == 1);
return subexpr[0];