diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc index 2fc1c821c29..c79401ad1fe 100644 --- a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc +++ b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc @@ -3,7 +3,7 @@ Test.class --function Test.main --no-simplify --unwind 10 --show-vcc ^EXIT=0$ ^SIGNAL=0$ -"java::Impl1" = cast\(\{ \{ "java::Impl1"\}, 0\}, struct \{ struct \{ string @class_identifier \} @java.lang.Object \}\)\.@java.lang.Object\.@class_identifier +"java::Impl1" = cast\(\{ \{ "java::Impl1" \}, 0 \}, struct \{ struct \{ string @class_identifier \} @java.lang.Object \}\)\.@java.lang.Object\.@class_identifier -- ^warning: ignoring -- diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index d9ec271b34f..35c9e828749 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -294,7 +294,7 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr) os << format(op); } - return os << '}'; + return os << " }"; } else if(id == ID_if) { diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index 3f361a10fb3..54cbfe2a264 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -60,7 +60,7 @@ std::ostream &format_rec(std::ostream &os, const typet &type) const auto &id = type.id(); if(id == ID_pointer) - return os << '*' << format(to_pointer_type(type).subtype()); + return os << format(to_pointer_type(type).subtype()) << '*'; else if(id == ID_array) { const auto &t = to_array_type(type);