Fix forall precedences (thanks @v-gb !)

GillianPlatform · Jan 7, 2025 · 8111475 · 8111475
1 parent 3834539
commit 8111475
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/Gillian-C/lib/MonadicSVal.ml b/Gillian-C/lib/MonadicSVal.ml
@@ -237,8 +237,10 @@ module SVArray = struct
             fmt "Undefined pf: not as concrete: %a" Expr.pp size);
         let i = LVar.alloc () in
         let i_e = Expr.LVar i in
-        forall [ (i, Some IntType) ] zero <= i_e
-        && i_e < size ==> (Expr.list_nth_e arr_exp i_e == Lit Undefined)
+        forall
+          [ (i, Some IntType) ]
+          ((zero <= i_e && i_e < size)
+          ==> (Expr.list_nth_e arr_exp i_e == Lit Undefined))
 
   let zeros_pf ?size arr_exp =
     let size =
@@ -259,12 +261,12 @@ module SVArray = struct
     | _ ->
         Logging.verbose (fun fmt ->
             fmt "Zeros pf: not as concrete: %a" Expr.pp size);
-        let is_zero e = e == Expr.int 0 in
         let i = LVar.alloc () in
         let i_e = Expr.LVar i in
         let zero = Expr.int 0 in
-        forall [ (i, Some IntType) ] zero <= i_e
-        && i_e < size ==> is_zero (Expr.list_nth_e arr_exp i_e)
+        forall
+          [ (i, Some IntType) ]
+          ((zero <= i_e && i_e < size) ==> (Expr.list_nth_e arr_exp i_e == zero))
 
   let to_arr_with_size arr s =
     let open Expr.Infix in

diff --git a/Gillian-C2/lib/memory_model/SVal.ml b/Gillian-C2/lib/memory_model/SVal.ml
@@ -290,15 +290,16 @@ module SVArray = struct
             fmt "Zeros pf: not as concrete: %a" Expr.pp size);
         let values_var = LVar.alloc () in
         let values = Expr.LVar values_var in
-        let is_zero e = e == Expr.int 0 in
         let i = LVar.alloc () in
         let i_e = Expr.LVar i in
         let zero = Expr.zero_i in
         let learned_types = [ (values_var, Type.ListType) ] in
         let correct_length = Expr.list_length values == size in
         let all_zero =
-          forall [ (i, Some IntType) ] zero <= i_e
-          && i_e < size ==> is_zero (Expr.list_nth_e values i_e)
+          forall
+            [ (i, Some IntType) ]
+            ((zero <= i_e && i_e < size)
+            ==> (Expr.list_nth_e values i_e == zero))
         in
         return ~learned:[ correct_length; all_zero ] ~learned_types values