[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`.
serokell · Jun 21, 2024 · 58330f7 · 58330f7
1 parent ac73455
commit 58330f7
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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;