Dafny: Fixed a bug in the pretty printer.

1 files changed, 5 insertions, 1 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index cf8be27e..4290953b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -976,9 +976,13 @@ namespace Microsoft.Dafny {
           bool parensNeeded = opBindingStrength < contextBindingStrength ||

             (fragileContext && opBindingStrength == contextBindingStrength);

 

+          bool containsNestedNot = e.E is ParensExpression &&

+                                ((ParensExpression)e.E).E is UnaryExpr &&

+                                ((UnaryExpr)((ParensExpression)e.E).E).Op == UnaryExpr.Opcode.Not;

+

           if (parensNeeded) { wr.Write("("); }

           wr.Write(op);

-          PrintExpr(e.E, opBindingStrength, false, parensNeeded || isRightmost, -1);

+          PrintExpr(e.E, opBindingStrength, containsNestedNot, parensNeeded || isRightmost, -1);

           if (parensNeeded) { wr.Write(")"); }

         }