diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index d118a55ef32..71d3a3a86b7 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -5726,7 +5726,7 @@ void smt2_convt::find_symbols(const exprt &expr)
       const auto &floatbv_type = to_floatbv_type(tc.op().type());
       out << "(assert (= ";
       out << "((_ to_fp " << floatbv_type.get_e() << " "
-          << floatbv_type.get_f() + 1 << ") " << id << ')';
+          << floatbv_type.get_f() + 1 << ") " << id << ") ";
       convert_expr(tc.op());
       out << ')'; // =
       out << ')' << '\n';