Fixed generation of smt2 concat statements

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9b1972b14e7cd65c5be0e468ea30da76a4580e6a..1e00ac7185a24d2386ffbfb5c16047a22b5ea7d8 100644 (file)
--- 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];