diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 8c9da43e309..13d8c7e6e94 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -150,7 +150,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     for(std::size_t i = 0; i < array_list_expr.operands().size(); i += 2)
       out << "(store ";
 
-    out << "((as const " << smt2_format(expr.type()) << ")) "
+    out << "((as const " << smt2_format(expr.type()) << ") "
         << smt2_format(
              from_integer(0, to_array_type(expr.type()).element_type()))
         << ')';