diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 3c6d60f352..c705e8eb93 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -164,7 +164,10 @@ struct print_expr_fn { bool first = true; for (auto l : ls) { if (first) first = false; else out() << " "; - out() << l; + if (is_max(l) || is_imax(l)) + out() << "(" << l << ")"; + else + out() << l; } out() << "}"; }