File tree Expand file tree Collapse file tree 1 file changed +11
-6
lines changed Expand file tree Collapse file tree 1 file changed +11
-6
lines changed Original file line number Diff line number Diff line change @@ -2137,20 +2137,25 @@ void smt2_convt::convert_expr(const exprt &expr)
2137
2137
else if (quantifier_expr.id () == ID_exists)
2138
2138
out << " (exists " ;
2139
2139
2140
- out << " ( " ;
2140
+ out << ' (' ;
2141
+ bool first = true ;
2141
2142
for (const auto &bound : quantifier_expr.variables ())
2142
2143
{
2143
- out << " (" ;
2144
+ if (first)
2145
+ first = false ;
2146
+ else
2147
+ out << ' ' ;
2148
+ out << ' (' ;
2144
2149
convert_expr (bound);
2145
- out << " " ;
2150
+ out << ' ' ;
2146
2151
convert_type (bound.type ());
2147
- out << " ) " ;
2152
+ out << ' ) ' ;
2148
2153
}
2149
2154
out << " ) " ;
2150
2155
2151
2156
convert_expr (quantifier_expr.where ());
2152
2157
2153
- out << " ) " ;
2158
+ out << ' ) ' ;
2154
2159
}
2155
2160
else if (expr.id ()==ID_vector)
2156
2161
{
@@ -2383,7 +2388,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
2383
2388
convert_expr (src);
2384
2389
out << " " ;
2385
2390
convert_expr (from_integer (0 , src_type));
2386
- out << " )) " ; // not, =
2391
+ out << " ))" ; // not, =
2387
2392
out << " (_ bv1 " << to_width << " )" ;
2388
2393
out << " (_ bv0 " << to_width << " )" ;
2389
2394
out << " )" ; // ite
You can’t perform that action at this time.
0 commit comments