From 58330f7c55052dcb0dbbc49333871f7eb95704d6 Mon Sep 17 00:00:00 2001
From: Golovin Pavel <gopavel0@gmail.com>
Date: Tue, 18 Jun 2024 00:16:08 +0200
Subject: [PATCH] [motoko-san] bugfix: add parenthesis around quantifiers

Problem: `Forall(func i => i == i) ==> B` is translated as
`forall i, i == i ==> B` that is wrong since involving `i` in the context of
`B`.
---
 src/viper/pretty.ml           | 4 ++--
 test/viper/ok/odd-even.vpr.ok | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
index 3535177c7e9..33521fee5ac 100644
--- a/src/viper/pretty.ml
+++ b/src/viper/pretty.ml
@@ -172,8 +172,8 @@ and pp_exp ppf exp =
     fprintf ppf "@[old(%a)@]" pp_exp e
   | PermE p -> pp_perm ppf p
   | AccE (fldacc, perm) -> fprintf ppf "@[acc(%a,%a)@]" pp_fldacc fldacc pp_exp perm
-  | ForallE (binders, exp) -> fprintf ppf "@[forall %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
-  | ExistsE (binders, exp) -> fprintf ppf "@[exists %a :: %a@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
+  | ForallE (binders, exp) -> fprintf ppf "@[(forall %a :: %a)@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
+  | ExistsE (binders, exp) -> fprintf ppf "@[(exists %a :: %a)@]" (pp_print_list ~pp_sep:comma pp_binder) binders pp_exp exp
   | _ -> fprintf ppf "@[// pretty printer not implemented for node at %s@]" (string_of_region exp.at)
 
 and pp_perm ppf perm =
diff --git a/test/viper/ok/odd-even.vpr.ok b/test/viper/ok/odd-even.vpr.ok
index 8ad16c4d127..033799a5e35 100644
--- a/test/viper/ok/odd-even.vpr.ok
+++ b/test/viper/ok/odd-even.vpr.ok
@@ -38,7 +38,7 @@ method odd($Self: Ref, n: Int)
     requires ((n % 2) == 1)
     ensures $Perm($Self)
     { 
-      assert exists k : Int :: (((2 * k) + 1) == n);
+      assert (exists k : Int :: (((2 * k) + 1) == n));
       $Res := n;
       goto $Ret;
       label $Ret; 
@@ -49,7 +49,7 @@ method even($Self: Ref, n: Int)
     requires ((n % 2) == 0)
     ensures $Perm($Self)
     { 
-      assert exists k : Int :: ((2 * k) == n);
+      assert (exists k : Int :: ((2 * k) == n));
       $Res := n;
       goto $Ret;
       label $Ret;