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)
21372137 else if (quantifier_expr.id () == ID_exists)
21382138 out << " (exists " ;
21392139
2140- out << " ( " ;
2140+ out << ' (' ;
2141+ bool first = true ;
21412142 for (const auto &bound : quantifier_expr.variables ())
21422143 {
2143- out << " (" ;
2144+ if (first)
2145+ first = false ;
2146+ else
2147+ out << ' ' ;
2148+ out << ' (' ;
21442149 convert_expr (bound);
2145- out << " " ;
2150+ out << ' ' ;
21462151 convert_type (bound.type ());
2147- out << " ) " ;
2152+ out << ' ) ' ;
21482153 }
21492154 out << " ) " ;
21502155
21512156 convert_expr (quantifier_expr.where ());
21522157
2153- out << " ) " ;
2158+ out << ' ) ' ;
21542159 }
21552160 else if (expr.id ()==ID_vector)
21562161 {
@@ -2383,7 +2388,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
23832388 convert_expr (src);
23842389 out << " " ;
23852390 convert_expr (from_integer (0 , src_type));
2386- out << " )) " ; // not, =
2391+ out << " ))" ; // not, =
23872392 out << " (_ bv1 " << to_width << " )" ;
23882393 out << " (_ bv0 " << to_width << " )" ;
23892394 out << " )" ; // ite
You can’t perform that action at this time.
0 commit comments