diff --git a/Gillian-C/lib/Constr.ml b/Gillian-C/lib/Constr.ml
index e630e942..979a04b6 100644
--- a/Gillian-C/lib/Constr.ml
+++ b/Gillian-C/lib/Constr.ml
@@ -3,7 +3,7 @@ open Gil_syntax
 module Core = struct
   let pred ga ins outs =
     let ga_name = LActions.str_ga ga in
-    Asrt.GA (ga_name, ins, outs)
+    Asrt.CorePred (ga_name, ins, outs)
 
   let single ~loc ~ofs ~chunk ~sval ~perm =
     let chunk = Expr.Lit (String (ValueTranslation.string_of_chunk chunk)) in
diff --git a/Gillian-C/lib/MonadicSMemory.ml b/Gillian-C/lib/MonadicSMemory.ml
index 8cbb2d1a..4a665c2f 100644
--- a/Gillian-C/lib/MonadicSMemory.ml
+++ b/Gillian-C/lib/MonadicSMemory.ml
@@ -256,7 +256,7 @@ module Mem = struct
 
   let prod_bounds map loc bounds =
     let open DR.Syntax in
-    let** loc_name = resolve_loc_result loc in
+    let* loc_name = resolve_or_create_loc_name loc in
     let* tree = get_or_create_tree map loc_name in
     let++ tree_set =
       SHeapTree.prod_bounds tree bounds |> DR.of_result |> map_lift_err loc_name
@@ -525,7 +525,7 @@ let execute_prod_single heap params =
   ] ->
       let perm = ValueTranslation.permission_of_string perm_string in
       let chunk = ValueTranslation.chunk_of_string chunk_string in
-      let* sval = SVal.of_gil_expr_exn sval_e in
+      let* sval = SVal.of_gil_expr_vanish sval_e in
       let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
       { heap with mem }
   | _ -> fail_ungracefully "set_single" params
diff --git a/Gillian-C/lib/MonadicSVal.ml b/Gillian-C/lib/MonadicSVal.ml
index 32d3bcf1..b38b73f0 100644
--- a/Gillian-C/lib/MonadicSVal.ml
+++ b/Gillian-C/lib/MonadicSVal.ml
@@ -119,6 +119,12 @@ let of_gil_expr_exn sval_e =
       if !Gillian.Utils.Config.under_approximation then Delayed.vanish ()
       else raise (NotACompCertValue sval_e)
 
+let of_gil_expr_vanish sval_e =
+  let* value_opt = of_gil_expr sval_e in
+  match value_opt with
+  | Some value -> Delayed.return value
+  | None -> Delayed.vanish ()
+
 let to_gil_expr_undelayed = to_gil_expr
 
 let to_gil_expr sval =
diff --git a/Gillian-C/lib/SHeapTree.mli b/Gillian-C/lib/SHeapTree.mli
index 2936bfb9..230f1a5a 100644
--- a/Gillian-C/lib/SHeapTree.mli
+++ b/Gillian-C/lib/SHeapTree.mli
@@ -85,7 +85,7 @@ val allocated_function : t
     [dst_tree] after modification *)
 val move : t -> Expr.t -> t -> Expr.t -> Expr.t -> t d_or_error
 
-val assertions : loc:string -> t -> Asrt.t list
+val assertions : loc:string -> t -> Asrt.t
 
 val substitution :
   le_subst:(Expr.t -> Expr.t) ->
diff --git a/Gillian-C/lib/gil_logic_gen.ml b/Gillian-C/lib/gil_logic_gen.ml
index 0ba80016..e50a5cfd 100644
--- a/Gillian-C/lib/gil_logic_gen.ml
+++ b/Gillian-C/lib/gil_logic_gen.ml
@@ -5,7 +5,6 @@ open CLogic
 open Compcert
 open CompileState
 module Str_set = Gillian.Utils.Containers.SS
-open Asrt.Infix
 open Formula.Infix
 module CoreP = Constr.Core
 
@@ -31,7 +30,7 @@ let rec split3_expr_comp = function
   | [] -> ([], [], [])
   | (x, y, z) :: l ->
       let rx, ry, rz = split3_expr_comp l in
-      (x :: rx, y @ ry, z :: rz)
+      (x @ rx, y @ ry, z :: rz)
 
 let ( ++ ) = Expr.Infix.( + )
 
@@ -135,83 +134,65 @@ let assert_of_member cenv members id typ =
         Fmt.failwith "Invalid member offset : %a@?" Driveraux.print_error e
   in
   (* The following bit of code should be refactored to be made cleaner ... *)
-  if
-    match typ with
-    | Tstruct _ -> true
-    | _ -> false
-  then
-    let struct_name, struct_id =
-      match typ with
-      | Tstruct (id, _) -> (true_name id, id)
-      | _ -> failwith "impossible"
-    in
-    let pred_name = pred_name_of_struct struct_name in
-    let arg_number =
-      List.length (Option.get (Maps.PTree.get struct_id cenv)).co_members
-    in
-    let args_without_ins =
-      List.init arg_number (fun k ->
-          Expr.LVar ("#i__" ^ field_name ^ "_" ^ string_of_int k))
-    in
-    let list_is_components =
-      let open Formula.Infix in
-      Asrt.Pure pvmember #== (Expr.list args_without_ins)
-    in
-    let ofs =
-      let open Expr.Infix in
-      pvofs + fo
-    in
-    let args = pvloc :: ofs :: args_without_ins in
-    let pred_call = Asrt.Pred (pred_name, args) in
-    list_is_components ** pred_call
-  else if
-    match typ with
-    | Tarray _ -> true
-    | _ -> false
-  then
-    let ty, n =
-      match typ with
-      | Tarray (ty, n, _) -> (ty, n)
-      | _ -> failwith "impossible"
-    in
-    let n = ValueTranslation.int_of_z n in
-    let n_e = Expr.int_z n in
-    let chunk =
-      match access_mode_by_value ty with
-      | Some chunk -> chunk
-      | _ -> failwith "Array in a structure containing complicated types"
-    in
-    Constr.Core.array ~loc:pvloc ~ofs:(pvofs ++ fo) ~chunk ~size:n_e
-      ~sval_arr:pvmember ~perm:(Some Freeable)
-  else
-    let mk t v = Expr.list [ Expr.string t; v ] in
-    let field_val_name = "#i__" ^ field_name ^ "_v" in
-    let lvval = Expr.LVar field_val_name in
-    let e_to_use, getter_or_type_pred =
-      let open Internal_Predicates in
-      let open VTypes in
-      match typ with
-      | Tint _ -> (mk int_type lvval, Asrt.Pred (int_get, [ pvmember; lvval ]))
-      | Tlong _ ->
-          (mk long_type lvval, Asrt.Pred (long_get, [ pvmember; lvval ]))
-      | Tfloat _ ->
-          (mk float_type lvval, Asrt.Pred (float_get, [ pvmember; lvval ]))
-      | Tpointer _ -> (pvmember, Asrt.Pred (is_ptr_opt, [ pvmember ]))
-      | _ ->
-          failwith
-            (Printf.sprintf "unhandled struct field type for now : %s"
-               (PrintCsyntax.name_cdecl field_name typ))
-    in
-    let chunk =
-      match access_mode_by_value typ with
-      | Some chunk -> chunk
-      | _ -> failwith "Invalid access mode for some type"
-    in
-    let ga_asrt =
-      CoreP.single ~loc:pvloc ~ofs:(pvofs ++ fo) ~chunk ~sval:e_to_use
-        ~perm:(Some Freeable)
-    in
-    getter_or_type_pred ** ga_asrt
+  match typ with
+  | Tstruct (struct_id, _) ->
+      let struct_name = true_name struct_id in
+      let pred_name = pred_name_of_struct struct_name in
+      let arg_number =
+        List.length (Option.get (Maps.PTree.get struct_id cenv)).co_members
+      in
+      let args_without_ins =
+        List.init arg_number (fun k ->
+            Expr.LVar ("#i__" ^ field_name ^ "_" ^ string_of_int k))
+      in
+      let list_is_components =
+        Formula.Infix.(Asrt.Pure pvmember #== (Expr.list args_without_ins))
+      in
+      let ofs = Expr.Infix.(pvofs + fo) in
+      let args = pvloc :: ofs :: args_without_ins in
+      let pred_call = Asrt.Pred (pred_name, args) in
+      [ list_is_components; pred_call ]
+  | Tarray (ty, n, _) ->
+      let n = ValueTranslation.int_of_z n in
+      let n_e = Expr.int_z n in
+      let chunk =
+        match access_mode_by_value ty with
+        | Some chunk -> chunk
+        | _ -> failwith "Array in a structure containing complicated types"
+      in
+      [
+        Constr.Core.array ~loc:pvloc ~ofs:(pvofs ++ fo) ~chunk ~size:n_e
+          ~sval_arr:pvmember ~perm:(Some Freeable);
+      ]
+  | _ ->
+      let mk t v = Expr.list [ Expr.string t; v ] in
+      let field_val_name = "#i__" ^ field_name ^ "_v" in
+      let lvval = Expr.LVar field_val_name in
+      let e_to_use, getter_or_type_pred =
+        let open Internal_Predicates in
+        let open VTypes in
+        match typ with
+        | Tint _ -> (mk int_type lvval, Asrt.Pred (int_get, [ pvmember; lvval ]))
+        | Tlong _ ->
+            (mk long_type lvval, Asrt.Pred (long_get, [ pvmember; lvval ]))
+        | Tfloat _ ->
+            (mk float_type lvval, Asrt.Pred (float_get, [ pvmember; lvval ]))
+        | Tpointer _ -> (pvmember, Asrt.Pred (is_ptr_opt, [ pvmember ]))
+        | _ ->
+            failwith
+              (Printf.sprintf "unhandled struct field type for now : %s"
+                 (PrintCsyntax.name_cdecl field_name typ))
+      in
+      let chunk =
+        match access_mode_by_value typ with
+        | Some chunk -> chunk
+        | _ -> failwith "Invalid access mode for some type"
+      in
+      let ga_asrt =
+        CoreP.single ~loc:pvloc ~ofs:(pvofs ++ fo) ~chunk ~sval:e_to_use
+          ~perm:(Some Freeable)
+      in
+      [ getter_or_type_pred; ga_asrt ]
 
 let assert_of_hole (low, high) =
   let pvloc = Expr.PVar loc_param_name in
@@ -244,22 +225,18 @@ let gen_pred_of_struct cenv ann struct_name =
     ]
   in
   let struct_params =
-    List.map
-      (function
-        | Member_plain (i, _) -> (true_name i, Some Type.ListType)
-        | Member_bitfield _ -> failwith "Unsupported bitfield members")
-      comp.co_members
+    comp.co_members
+    |> List.map @@ function
+       | Member_plain (i, _) -> (true_name i, Some Type.ListType)
+       | Member_bitfield _ -> failwith "Unsupported bitfield members"
   in
   let pred_params = first_params @ struct_params in
   let pred_num_params = List.length pred_params in
   let def_without_holes =
-    List.fold_left
-      (fun asrt member ->
-        match member with
-        | Member_plain (id, typ) ->
-            asrt ** assert_of_member cenv comp.co_members id typ
-        | Member_bitfield _ -> failwith "Unsupported bitfield members")
-      Asrt.Emp comp.co_members
+    comp.co_members
+    |> List.concat_map @@ function
+       | Member_plain (id, typ) -> assert_of_member cenv comp.co_members id typ
+       | Member_bitfield _ -> failwith "Unsupported bitfield members"
   in
   let fo idp =
     match field_offset cenv idp comp.co_members with
@@ -284,7 +261,7 @@ let gen_pred_of_struct cenv ann struct_name =
 
   let holes = get_holes comp.co_members in
   let holes_asserts = List.map assert_of_hole holes in
-  let def = Asrt.star holes_asserts ** def_without_holes in
+  let def = holes_asserts @ def_without_holes in
   (* TODO (Alexis): How to handle changes in structs? *)
   let n_pred =
     Pred.
@@ -354,112 +331,109 @@ let trans_sval (sv : CSVal.t) : Asrt.t * Var.t list * Expr.t =
   match sv with
   | CSVal.Sint se ->
       let eg = tse se in
-      (tint eg, [], mk int_type (tse se))
+      ([ tint eg ], [], mk int_type (tse se))
   | Slong se ->
       let eg = tse se in
-      (tint eg, [], mk long_type (tse se))
+      ([ tint eg ], [], mk long_type (tse se))
   | Ssingle se ->
       let eg = tse se in
-      (tnum eg, [], mk single_type (tse se))
+      ([ tnum eg ], [], mk single_type (tse se))
   | Sfloat se ->
       let eg = tse se in
-      (tnum eg, [], mk float_type (tse se))
+      ([ tnum eg ], [], mk float_type (tse se))
   | Sptr (se1, se2) ->
       let eg1, eg2 = (tse se1, tse se2) in
-      (tloc eg1 ** tint eg2, [], Expr.EList [ tse se1; tse se2 ])
+      ([ tloc eg1; tint eg2 ], [], Expr.EList [ tse se1; tse se2 ])
   | Sfunptr symb ->
       let loc = Global_env.location_of_symbol symb in
       let ptr = Expr.EList [ Lit (Loc loc); Expr.zero_i ] in
-      (Asrt.Emp, [], ptr)
+      ([], [], ptr)
 
 (** Returns assertions that are necessary to define the expression,
       the created variable for binding when necessary, and the used expression *)
 let rec trans_expr (e : CExpr.t) : Asrt.t * Var.t list * Expr.t =
   match e with
-  | CExpr.SExpr se -> (Asrt.Emp, [], trans_simpl_expr se)
+  | CExpr.SExpr se -> ([], [], trans_simpl_expr se)
   | SVal sv -> trans_sval sv
   | EList el ->
-      let asrts, vars, elp = split3_expr_comp (List.map trans_expr el) in
-      let asrt = Asrt.star asrts in
+      let asrt, vars, elp = split3_expr_comp (List.map trans_expr el) in
       (asrt, vars, Expr.EList elp)
   | ESet es ->
-      let asrts, vars, elp = split3_expr_comp (List.map trans_expr es) in
-      let asrt = Asrt.star asrts in
+      let asrt, vars, elp = split3_expr_comp (List.map trans_expr es) in
       (asrt, vars, Expr.ESet elp)
   | BinOp (e1, LstCat, e2) ->
       let a1, v1, eg1 = trans_expr e1 in
       let a2, v2, eg2 = trans_expr e2 in
-      (a1 ** a2, v1 @ v2, Expr.list_cat eg1 eg2)
+      (a1 @ a2, v1 @ v2, Expr.list_cat eg1 eg2)
   | BinOp (e1, LstCons, e2) ->
       let a1, v1, eg1 = trans_expr e1 in
       let a2, v2, eg2 = trans_expr e2 in
-      (a1 ** a2, v1 @ v2, Expr.list_cat (EList [ eg1 ]) eg2)
+      (a1 @ a2, v1 @ v2, Expr.list_cat (EList [ eg1 ]) eg2)
   | BinOp (e1, PtrPlus, e2) -> (
       let a1, v1, ptr = trans_expr e1 in
       let a2, v2, to_add = trans_expr e2 in
       match ptr with
       | Expr.EList [ loc; ofs ] ->
-          (a1 ** a2, v1 @ v2, Expr.EList [ loc; Expr.Infix.( + ) ofs to_add ])
+          (a1 @ a2, v1 @ v2, Expr.EList [ loc; Expr.Infix.( + ) ofs to_add ])
       | ptr ->
           let res_lvar = fresh_lvar () in
           let res = Expr.LVar res_lvar in
-          ( a1 ** a2 ** Constr.Others.ptr_add ~ptr ~to_add ~res,
+          ( a1 @ a2 @ [ Constr.Others.ptr_add ~ptr ~to_add ~res ],
             res_lvar :: (v1 @ v2),
             res ))
   | BinOp (e1, b, e2) ->
       let a1, v1, eg1 = trans_expr e1 in
       let a2, v2, eg2 = trans_expr e2 in
-      (a1 ** a2, v1 @ v2, BinOp (eg1, trans_binop b, eg2))
+      (a1 @ a2, v1 @ v2, BinOp (eg1, trans_binop b, eg2))
   | UnOp (u, e) ->
       let a, v, eg = trans_expr e in
       (a, v, UnOp (trans_unop u, eg))
   | NOp (nop, el) ->
-      let asrts, vs, elp = split3_expr_comp (List.map trans_expr el) in
-      let asrt = Asrt.star asrts in
+      let asrt, vs, elp = split3_expr_comp (List.map trans_expr el) in
       let gnop = trans_nop nop in
       (asrt, vs, Expr.NOp (gnop, elp))
   | LstSub (lst, start, len) ->
       let a1, v1, lst = trans_expr lst in
       let a2, v2, start = trans_expr start in
       let a3, v3, len = trans_expr len in
-      (a1 ** a2 ** a3, v1 @ v2 @ v3, Expr.list_sub ~lst ~start ~size:len)
+      (a1 @ a2 @ a3, v1 @ v2 @ v3, Expr.list_sub ~lst ~start ~size:len)
 
 let rec trans_form (f : CFormula.t) : Asrt.t * Var.t list * Formula.t =
   let open Formula.Infix in
   match f with
-  | CFormula.True -> (Emp, [], Formula.True)
-  | False -> (Emp, [], False)
+  | CFormula.True -> ([], [], Formula.True)
+  | False -> ([], [], False)
   | Eq (ce1, ce2) ->
       let f1, v1, eg1 = trans_expr ce1 in
       let f2, v2, eg2 = trans_expr ce2 in
-      (f1 ** f2, v1 @ v2, eg1 #== eg2)
+      (f1 @ f2, v1 @ v2, eg1 #== eg2)
   | LessEq (ce1, ce2) ->
       let f1, v1, eg1 = trans_expr ce1 in
       let f2, v2, eg2 = trans_expr ce2 in
-      (f1 ** f2, v1 @ v2, eg1 #<= eg2)
+      (f1 @ f2, v1 @ v2, eg1 #<= eg2)
   | Less (ce1, ce2) ->
       let f1, v1, eg1 = trans_expr ce1 in
       let f2, v2, eg2 = trans_expr ce2 in
-      (f1 ** f2, v1 @ v2, eg1 #< eg2)
+      (f1 @ f2, v1 @ v2, eg1 #< eg2)
   | SetMem (ce1, ce2) ->
       let f1, v1, eg1 = trans_expr ce1 in
       let f2, v2, eg2 = trans_expr ce2 in
-      (f1 ** f2, v1 @ v2, SetMem (eg1, eg2))
+      (f1 @ f2, v1 @ v2, SetMem (eg1, eg2))
   | Not fp ->
       let a, v, fpp = trans_form fp in
       (a, v, fnot fpp)
   | Or (f1, f2) ->
       let a1, v1, fp1 = trans_form f1 in
       let a2, v2, fp2 = trans_form f2 in
-      (a1 ** a2, v1 @ v2, fp1 #|| fp2)
+      (a1 @ a2, v1 @ v2, fp1 #|| fp2)
   | And (f1, f2) ->
       let a1, v1, fp1 = trans_form f1 in
       let a2, v2, fp2 = trans_form f2 in
-      (a1 ** a2, v1 @ v2, fp1 #&& fp2)
+      (a1 @ a2, v1 @ v2, fp1 #&& fp2)
   | Implies (f1, f2) ->
       let a1, v1, fp1 = trans_form f1 in
       let a2, v2, fp2 = trans_form f2 in
-      (a1 ** a2, v1 @ v2, fp1 #=> fp2)
+      (a1 @ a2, v1 @ v2, fp1 #=> fp2)
   | ForAll (lvts, f) ->
       let a, v, fp = trans_form f in
       (a, v, ForAll (lvts, fp))
@@ -511,13 +485,13 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
         let loc = Global_env.location_of_symbol symb in
         let loc = Expr.Lit (Loc loc) in
         let ofsv = Expr.int 0 in
-        (Asrt.Emp, loc, ofsv)
+        ([], loc, ofsv)
     | _ ->
         let a_s, _, s_e = trans_expr s in
         let locv = gen_loc_var () in
         let ofsv = gen_ofs_var () in
         let pc = ptr_call s_e locv ofsv in
-        (pc ** a_s, locv, ofsv)
+        (pc :: a_s, locv, ofsv)
   in
   let to_assert, locv, ofsv = interpret_s ~typ s in
   let malloc_chunk siz =
@@ -526,52 +500,35 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
   let mk str v = Expr.list [ Expr.string str; v ] in
   let mk_ptr l o = Expr.list [ l; o ] in
   match c with
-  | CConstructor.ConsExpr (SVal (Sint se)) ->
-      let e = cse se in
-      let chunk = Chunk.Mint32 in
-      let sv = mk int_type e in
-      let siz = sz (Sint se) in
-      let ga =
-        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:sv ~perm:(Some Freeable)
-      in
-      ga ** to_assert ** tint e ** malloc_chunk siz
-  | ConsExpr (SVal (Sfloat se)) ->
-      let e = cse se in
-      let chunk = Chunk.Mfloat32 in
-      let siz = sz (Sfloat se) in
-      let sv = mk float_type e in
-      let ga =
-        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:sv ~perm:(Some Freeable)
+  | CConstructor.ConsExpr (SVal (Sint v as se))
+  | ConsExpr (SVal (Sfloat v as se))
+  | ConsExpr (SVal (Ssingle v as se))
+  | ConsExpr (SVal (Slong v as se)) ->
+      let chunk, typ, asrtfn =
+        match se with
+        | Sint _ -> (Chunk.Mint32, int_type, tint)
+        | Sfloat _ -> (Chunk.Mfloat32, float_type, tnum)
+        | Ssingle _ -> (Chunk.Mfloat32, single_type, tnum)
+        | Slong _ -> (Chunk.Mint64, long_type, tint)
+        | _ -> failwith "Impossible"
       in
-      ga ** to_assert ** tnum e ** malloc_chunk siz
-  | ConsExpr (SVal (Ssingle se)) ->
-      let e = cse se in
-      let chunk = Chunk.Mfloat32 in
-      let siz = sz (Ssingle se) in
-      let sv = mk single_type e in
+      let e = cse v in
+      let sval = mk typ e in
+      let siz = sz se in
       let ga =
-        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:sv ~perm:(Some Freeable)
+        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval ~perm:(Some Freeable)
       in
-      ga ** to_assert ** tnum e ** malloc_chunk siz
-  | ConsExpr (SVal (Slong se)) ->
-      let e = cse se in
-      let chunk = Chunk.Mint64 in
-      let siz = sz (Slong se) in
-      let sv = mk long_type e in
-      let ga =
-        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:sv ~perm:(Some Freeable)
-      in
-      ga ** to_assert ** tint e ** malloc_chunk siz
+      [ ga; asrtfn e; malloc_chunk siz ] @ to_assert
   | ConsExpr (SVal (Sptr (sl, so))) ->
       let l = cse sl in
       let o = cse so in
       let chunk = Chunk.ptr in
       let siz = sz (Sptr (sl, so)) in
-      let sv = mk_ptr l o in
+      let sval = mk_ptr l o in
       let ga =
-        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:sv ~perm:(Some Freeable)
+        CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval ~perm:(Some Freeable)
       in
-      ga ** to_assert ** tloc l ** tint o ** malloc_chunk siz
+      [ ga; tloc l; tint o; malloc_chunk siz ] @ to_assert
   | ConsExpr (SVal (Sfunptr fname)) ->
       let l = Global_env.location_of_symbol fname in
       let ptr = Expr.EList [ Expr.Lit (Loc l); Expr.zero_i ] in
@@ -580,7 +537,7 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
       let ga_single =
         CoreP.single ~loc:locv ~ofs:ofsv ~chunk ~sval:ptr ~perm:(Some Freeable)
       in
-      ga_single ** to_assert ** malloc_chunk siz
+      [ ga_single; malloc_chunk siz ] @ to_assert
   | ConsExpr _ ->
       Fmt.failwith "Constructor %a is not handled yet" CConstructor.pp c
   | ConsStruct (sname, el) ->
@@ -597,72 +554,73 @@ let trans_constr ?fname:_ ~(typ : CAssert.points_to_type) ann s c =
         split3_expr_comp (List.map trans_expr el)
       in
       let pr =
-        Asrt.Pred (struct_pred, [ locv; ofsv ] @ params_fields)
-        ** Asrt.star more_asrt
+        Asrt.Pred (struct_pred, [ locv; ofsv ] @ params_fields) :: more_asrt
       in
-      pr ** to_assert ** malloc_chunk siz
+      pr @ to_assert @ [ malloc_chunk siz ]
 
 let rec trans_asrt ~fname ~ann asrt =
-  match asrt with
-  | CAssert.Star (a1, a2) ->
-      trans_asrt ~fname ~ann a1 ** trans_asrt ~fname ~ann a2
-  | Array { ptr; chunk; size; content; malloced } ->
-      let a1, _, ptr = trans_expr ptr in
-      let a2, _, size = trans_expr size in
-      let a3, _, content = trans_expr content in
-      let malloc_p =
-        if malloced then
-          let open Expr.Infix in
-          let csize = Expr.int (Chunk.size chunk) in
-          let total_size = size * csize in
-          Constr.Others.malloced_abst ~ptr ~total_size
-        else Asrt.Emp
-      in
-      a1 ** a2 ** a3
-      ** Constr.Others.array_ptr ~ptr ~chunk ~size ~content
-      ** malloc_p
-  | Malloced (e1, e2) ->
-      let a1, _, ce1 = trans_expr e1 in
-      let a2, _, ce2 = trans_expr e2 in
-      a1 ** a2 ** Constr.Others.malloced_abst ~ptr:ce1 ~total_size:ce2
-  | Zeros (e1, e2) ->
-      let a1, _, ce1 = trans_expr e1 in
-      let a2, _, ce2 = trans_expr e2 in
-      a1 ** a2 ** Constr.Others.zeros_ptr_size ~ptr:ce1 ~size:ce2
-  | Undefs (e1, e2) ->
-      let a1, _, ce1 = trans_expr e1 in
-      let a2, _, ce2 = trans_expr e2 in
-      a1 ** a2 ** Constr.Others.undefs_ptr_size ~ptr:ce1 ~size:ce2
-  | Pure f ->
-      let ma, _, fp = trans_form f in
-      ma ** Pure fp
-  | Pred (p, cel) ->
-      let ap, _, gel = split3_expr_comp (List.map trans_expr cel) in
-      Asrt.star ap ** Pred (p, gel)
-  | Emp -> Emp
-  | PointsTo { ptr = s; constr = c; typ } -> trans_constr ~fname ~typ ann s c
+  let a =
+    match asrt with
+    | CAssert.Star (a1, a2) ->
+        trans_asrt ~fname ~ann a1 @ trans_asrt ~fname ~ann a2
+    | Array { ptr; chunk; size; content; malloced } ->
+        let a1, _, ptr = trans_expr ptr in
+        let a2, _, size = trans_expr size in
+        let a3, _, content = trans_expr content in
+        let malloc_p =
+          if malloced then
+            let open Expr.Infix in
+            let csize = Expr.int (Chunk.size chunk) in
+            let total_size = size * csize in
+            [ Constr.Others.malloced_abst ~ptr ~total_size ]
+          else []
+        in
+        a1 @ a2 @ a3
+        @ [ Constr.Others.array_ptr ~ptr ~chunk ~size ~content ]
+        @ malloc_p
+    | Malloced (e1, e2) ->
+        let a1, _, ce1 = trans_expr e1 in
+        let a2, _, ce2 = trans_expr e2 in
+        a1 @ a2 @ [ Constr.Others.malloced_abst ~ptr:ce1 ~total_size:ce2 ]
+    | Zeros (e1, e2) ->
+        let a1, _, ce1 = trans_expr e1 in
+        let a2, _, ce2 = trans_expr e2 in
+        a1 @ a2 @ [ Constr.Others.zeros_ptr_size ~ptr:ce1 ~size:ce2 ]
+    | Undefs (e1, e2) ->
+        let a1, _, ce1 = trans_expr e1 in
+        let a2, _, ce2 = trans_expr e2 in
+        a1 @ a2 @ [ Constr.Others.undefs_ptr_size ~ptr:ce1 ~size:ce2 ]
+    | Pure f ->
+        let ma, _, fp = trans_form f in
+        Pure fp :: ma
+    | Pred (p, cel) ->
+        let ap, _, gel = split3_expr_comp (List.map trans_expr cel) in
+        Pred (p, gel) :: ap
+    | Emp -> [ Asrt.Emp ]
+    | PointsTo { ptr = s; constr = c; typ } -> trans_constr ~fname ~typ ann s c
+  in
+  match List.filter (fun x -> x <> Asrt.Emp) a with
+  | [] -> [ Asrt.Emp ]
+  | a -> a
 
 let rec trans_lcmd ~fname ~ann lcmd =
   let trans_lcmd = trans_lcmd ~fname ~ann in
   let trans_asrt = trans_asrt ~fname ~ann in
   let make_assert ~bindings = function
-    | Asrt.Emp -> []
+    | [] | [ Asrt.Emp ] -> []
     | a -> [ LCmd.SL (SepAssert (a, bindings)) ]
   in
   match lcmd with
   | CLCmd.Apply (pn, el) ->
       let aps, bindings, gel = split3_expr_comp (List.map trans_expr el) in
-      let to_assert = Asrt.star aps in
-      `Normal (make_assert ~bindings to_assert @ [ SL (ApplyLem (pn, gel, [])) ])
+      `Normal (make_assert ~bindings aps @ [ SL (ApplyLem (pn, gel, [])) ])
   | CLCmd.Fold (pn, el) ->
       let aps, bindings, gel = split3_expr_comp (List.map trans_expr el) in
-      let to_assert = Asrt.star aps in
-      `Normal (make_assert ~bindings to_assert @ [ SL (Fold (pn, gel, None)) ])
+      `Normal (make_assert ~bindings aps @ [ SL (Fold (pn, gel, None)) ])
   | Unfold { pred; params; bindings; recursive } ->
       let ap, vs, gel = split3_expr_comp (List.map trans_expr params) in
-      let to_assert = Asrt.star ap in
       `Normal
-        (make_assert ~bindings:vs to_assert
+        (make_assert ~bindings:vs ap
         @ [ SL (Unfold (pred, gel, bindings, recursive)) ])
   | Unfold_all pred_name -> `Normal [ SL (GUnfold pred_name) ]
   | Assert (a, ex) -> `Normal [ SL (SepAssert (trans_asrt a, ex)) ]
@@ -688,16 +646,14 @@ let rec trans_lcmd ~fname ~ann lcmd =
 let trans_asrt_annot da =
   let { label; existentials } = da in
   let exs, typsb =
-    List.split
-      (List.map
-         (fun (ex, topt) ->
-           match topt with
-           | None -> (ex, Asrt.Emp)
-           | Some t -> (ex, types t (Expr.LVar ex)))
-         existentials)
+    existentials
+    |> ( List.map @@ fun (ex, topt) ->
+         match topt with
+         | None -> (ex, Asrt.Emp)
+         | Some t -> (ex, types t (Expr.LVar ex)) )
+    |> List.split
   in
-  let a = Asrt.star typsb in
-  (a, (label, exs))
+  (typsb, (label, exs))
 
 let trans_abs_pred ~filepath cl_pred =
   let CAbsPred.
@@ -747,7 +703,7 @@ let trans_pred ~ann ~filepath cl_pred =
         | None -> (None, trans_asrt ~fname:pred_name ~ann a)
         | Some da ->
             let ada, gda = trans_asrt_annot da in
-            (Some gda, ada ** trans_asrt ~fname:pred_name ~ann a))
+            (Some gda, ada @ trans_asrt ~fname:pred_name ~ann a))
       definitions
   in
   Pred.
@@ -778,7 +734,7 @@ let trans_sspec ~ann fname sspecs =
   let CSpec.{ pre; posts; spec_annot } = sspecs in
   let tap, spa =
     match spec_annot with
-    | None -> (Asrt.Emp, None)
+    | None -> ([], None)
     | Some spa ->
         let a, (label, exs) = trans_asrt_annot spa in
         (a, Some (label, exs))
@@ -787,7 +743,7 @@ let trans_sspec ~ann fname sspecs =
   let make_post p = if !Config.allocated_functions then ta p else ta p in
   Spec.
     {
-      ss_pre = tap ** ta pre;
+      ss_pre = tap @ ta pre;
       ss_posts = List.map make_post posts;
       (* FIXME: bring in variant *)
       ss_variant = None;
@@ -965,16 +921,15 @@ let generate_bispec clight_prog fname ident f =
   let mk_lvar x = Expr.LVar ("#" ^ x) in
   let lvars = List.map mk_lvar true_params in
   let equalities =
-    Asrt.star
-      (List.map
-         (fun x -> Asrt.Pure (Formula.Eq (Expr.PVar x, mk_lvar x)))
-         true_params)
+    List.map
+      (fun x -> Asrt.Pure (Formula.Eq (Expr.PVar x, mk_lvar x)))
+      true_params
   in
   (* Right now, triples are : (param_name, csharpminor type, c type)
      The C type will be used to discriminate long/int from pointers *)
   let triples = combine lvars sig_args cligh_params in
   let pred_list = List.map predicate_from_triple triples in
-  let pre = equalities ** Asrt.star pred_list in
+  let pre = equalities @ pred_list in
   BiSpec.
     {
       bispec_name = fname;
diff --git a/Gillian-JS/lib/Compiler/JSIL2GIL.ml b/Gillian-JS/lib/Compiler/JSIL2GIL.ml
index 24c82b45..0e7bbe44 100644
--- a/Gillian-JS/lib/Compiler/JSIL2GIL.ml
+++ b/Gillian-JS/lib/Compiler/JSIL2GIL.ml
@@ -98,15 +98,16 @@ let rec jsil2gil_asrt (a : Asrt.t) : GAsrt.t =
   let f = jsil2gil_asrt in
   let fe = jsil2gil_expr in
   match a with
-  | Emp -> Emp
-  | Star (a1, a2) -> Star (f a1, f a2)
+  | Emp -> [ Emp ]
+  | Star (a1, a2) -> f a1 @ f a2
   | PointsTo (e1, e2, e3) ->
-      Asrt_utils.points_to ~loc:(fe e1) ~field:(fe e2) ~value:(fe e3)
-  | MetaData (e1, e2) -> Asrt_utils.metadata ~loc:(fe e1) ~metadata:(fe e2)
-  | EmptyFields (e1, e2) -> Asrt_utils.empty_fields ~loc:(fe e1) ~domain:(fe e2)
-  | Pred (pn, es) -> Pred (pn, List.map fe es)
-  | Pure f -> Pure (jsil2gil_formula f)
-  | Types vts -> Types (List.map (fun (v, t) -> (fe v, t)) vts)
+      [ Asrt_utils.points_to ~loc:(fe e1) ~field:(fe e2) ~value:(fe e3) ]
+  | MetaData (e1, e2) -> [ Asrt_utils.metadata ~loc:(fe e1) ~metadata:(fe e2) ]
+  | EmptyFields (e1, e2) ->
+      [ Asrt_utils.empty_fields ~loc:(fe e1) ~domain:(fe e2) ]
+  | Pred (pn, es) -> [ Pred (pn, List.map fe es) ]
+  | Pure f -> [ Pure (jsil2gil_formula f) ]
+  | Types vts -> [ Types (List.map (fun (v, t) -> (fe v, t)) vts) ]
 
 let jsil2gil_slcmd (slcmd : SLCmd.t) : GSLCmd.t =
   match slcmd with
diff --git a/Gillian-JS/lib/Compiler/JSIL_PostParser.ml b/Gillian-JS/lib/Compiler/JSIL_PostParser.ml
index 5a2e3e57..0fbcca3a 100644
--- a/Gillian-JS/lib/Compiler/JSIL_PostParser.ml
+++ b/Gillian-JS/lib/Compiler/JSIL_PostParser.ml
@@ -199,8 +199,8 @@ let scope_info_to_assertion
 
   let this_asrt = make_this_assertion () in
 
-  let init_heap_asrt : Asrt.t = Pred (heap_asrt_name, []) in
   if fid <> JS2JSIL_Helpers.main_fid then
+    let init_heap_asrt : Asrt.t = Pred (heap_asrt_name, []) in
     Asrt.star
       (glob_constraints @ (this_asrt :: init_heap_asrt :: a_schain :: a_vars))
   else Asrt.star (glob_constraints @ (this_asrt :: a_schain :: a_vars))
diff --git a/Gillian-JS/lib/Semantics/JSILSMemory.ml b/Gillian-JS/lib/Semantics/JSILSMemory.ml
index 9cf0a69e..b2929db3 100644
--- a/Gillian-JS/lib/Semantics/JSILSMemory.ml
+++ b/Gillian-JS/lib/Semantics/JSILSMemory.ml
@@ -90,7 +90,7 @@ module M = struct
     in
     Recovery_tactic.try_unfold values
 
-  let assertions ?to_keep:_ (heap : t) : GAsrt.t list = SHeap.assertions heap
+  let assertions ?to_keep:_ (heap : t) : GAsrt.t = SHeap.assertions heap
   let lvars (heap : t) : Containers.SS.t = SHeap.lvars heap
   let alocs (heap : t) : Containers.SS.t = SHeap.alocs heap
 
@@ -597,9 +597,7 @@ module M = struct
   let prop_abduce_none_in_js = [ "@call" ]
   let prop_abduce_both_in_js = [ "hasOwnProperty" ]
 
-  type fix_result = Asrt.t list
-
-  let complete_fix_js (i_fix : i_fix_t) : fix_result list =
+  let complete_fix_js (i_fix : i_fix_t) : Asrt.t list =
     match i_fix with
     | FLoc v ->
         (* Get a fresh location *)
@@ -610,7 +608,7 @@ module M = struct
         [ [ Asrt.Pure (Eq (ALoc al, v)) ] ]
     | FCell (l, p) -> (
         let none_fix () =
-          [ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ]
+          [ Asrt.CorePred (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ]
         in
 
         let some_fix () =
@@ -632,7 +630,7 @@ module M = struct
               ]
           in
           [
-            Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]);
+            Asrt.CorePred (JSILNames.aCell, [ l; p ], [ descriptor ]);
             Asrt.Pure asrt_empty;
             Asrt.Pure asrt_none;
             Asrt.Pure asrt_list;
@@ -651,17 +649,17 @@ module M = struct
         [
           [
             Asrt.Pure (Eq (ALoc al, l));
-            Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]);
-            Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]);
-            Asrt.GA
+            Asrt.CorePred (JSILNames.aMetadata, [ l ], [ mloc ]);
+            Asrt.CorePred (JSILNames.aMetadata, [ mloc ], [ Lit Null ]);
+            Asrt.CorePred
               ( JSILNames.aCell,
                 [ mloc; Lit (String "@class") ],
                 [ Lit (String "Object") ] );
-            Asrt.GA
+            Asrt.CorePred
               ( JSILNames.aCell,
                 [ mloc; Lit (String "@extensible") ],
                 [ Lit (Bool true) ] );
-            Asrt.GA
+            Asrt.CorePred
               ( JSILNames.aCell,
                 [ mloc; Lit (String "@proto") ],
                 [ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] );
@@ -670,7 +668,7 @@ module M = struct
     | FPure f -> [ [ Asrt.Pure f ] ]
 
   (* Fix completion: simple *)
-  let complete_fix_jsil (i_fix : i_fix_t) : fix_result list =
+  let complete_fix_jsil (i_fix : i_fix_t) : Asrt.t list =
     match i_fix with
     | FLoc v ->
         (* Get a fresh location *)
@@ -682,20 +680,29 @@ module M = struct
         let v : vt = LVar vvar in
         (* Value is not none - we always bi-abduce presence *)
         let not_none : Formula.t = Not (Eq (v, Lit Nono)) in
-        [ [ Asrt.GA (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none ] ]
+        [
+          [
+            Asrt.CorePred (JSILNames.aCell, [ l; p ], [ v ]); Asrt.Pure not_none;
+          ];
+        ]
     | FMetadata l ->
         (* Fresh variable to denote the property value *)
         let vvar = LVar.alloc () in
         let v : vt = LVar vvar in
         let not_none : Formula.t = Not (Eq (v, Lit Nono)) in
-        [ [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ] ]
+        [
+          [
+            Asrt.CorePred (JSILNames.aMetadata, [ l ], [ v ]);
+            Asrt.Pure not_none;
+          ];
+        ]
     | FPure f -> [ [ Asrt.Pure f ] ]
 
   (* An error can have multiple fixes *)
-  let get_fixes (err : err_t) : fix_result list =
-    let pp_fix_result ft res =
+  let get_fixes (err : err_t) : Asrt.t list =
+    let pp_fix ft res =
       let open Fmt in
-      pf ft "@[<v 2>@[<h>[[ %a ]]@]@\n@]" (list ~sep:comma Asrt.pp) res
+      pf ft "@[<v 2>@[<h>[[ %a ]]@]@\n@]" Asrt.pp res
     in
     let _, fixes, _ = err in
     L.verbose (fun m ->
@@ -709,10 +716,10 @@ module M = struct
       if !Js_config.js then complete_fix_js else complete_fix_jsil
     in
 
-    let complete_ifixes (ifixes : i_fix_t list) : fix_result list =
+    let complete_ifixes (ifixes : i_fix_t list) : Asrt.t list =
       let completed_ifixes = List.map complete ifixes in
       let completed_ifixes = List_utils.list_product completed_ifixes in
-      let completed_ifixes : fix_result list =
+      let completed_ifixes : Asrt.t list =
         List.map
           (fun fixes -> List.fold_right List.append fixes [])
           completed_ifixes
@@ -721,16 +728,14 @@ module M = struct
       L.verbose (fun m ->
           m "@[<v 2>Memory: i-fixes completed: %d@\n%a"
             (List.length completed_ifixes)
-            Fmt.(list ~sep:(any "@\n") pp_fix_result)
+            Fmt.(list ~sep:(any "@\n") pp_fix)
             completed_ifixes);
 
       completed_ifixes
     in
 
     (* Fixes hold lists of lists of i_fixes, *)
-    let completed_fixes = List.concat (List.map complete_ifixes fixes) in
-
-    completed_fixes
+    List.concat_map complete_ifixes fixes
 
   let can_fix _ = true
 
diff --git a/Gillian-JS/lib/Semantics/SFVL.ml b/Gillian-JS/lib/Semantics/SFVL.ml
index 610d9949..9231e48d 100644
--- a/Gillian-JS/lib/Semantics/SFVL.ml
+++ b/Gillian-JS/lib/Semantics/SFVL.ml
@@ -75,10 +75,10 @@ let alocs (sfvl : t) : SS.t =
       SS.union ac (SS.union (Expr.alocs e_field) (Expr.alocs e_val)))
     sfvl SS.empty
 
-let assertions (loc : Expr.t) (sfvl : t) : Asrt.t list =
+let assertions (loc : Expr.t) (sfvl : t) : Asrt.t =
   List.rev
     (Expr.Map.fold
-       (fun field value (ac : Asrt.t list) ->
+       (fun field value (ac : Asrt.t) ->
          Asrt_utils.points_to ~loc ~field ~value :: ac)
        sfvl [])
 
diff --git a/Gillian-JS/lib/Semantics/SFVL.mli b/Gillian-JS/lib/Semantics/SFVL.mli
index 2a4cdee4..3427ed05 100644
--- a/Gillian-JS/lib/Semantics/SFVL.mli
+++ b/Gillian-JS/lib/Semantics/SFVL.mli
@@ -23,7 +23,7 @@ val pp : Format.formatter -> t -> unit
 val union : t -> t -> t
 val lvars : t -> Containers.SS.t
 val alocs : t -> Containers.SS.t
-val assertions : Expr.t -> t -> Asrt.t list
+val assertions : Expr.t -> t -> Asrt.t
 val substitution : Subst.t -> bool -> t -> t
 val selective_substitution : Subst.t -> bool -> t -> t
 val is_well_formed : t -> bool
diff --git a/Gillian-JS/lib/Semantics/SHeap.ml b/Gillian-JS/lib/Semantics/SHeap.ml
index d0c7e1fc..34edc0fb 100644
--- a/Gillian-JS/lib/Semantics/SHeap.ml
+++ b/Gillian-JS/lib/Semantics/SHeap.ml
@@ -338,7 +338,7 @@ let to_list (heap : t) : (string * s_object) list =
   SS.fold (fun loc ac -> (loc, Option.get (get heap loc)) :: ac) domain []
 
 (** converts a symbolic heap to a list of assertions *)
-let assertions (heap : t) : Asrt.t list =
+let assertions (heap : t) : Asrt.t =
   let make_loc_lexpr loc =
     if Names.is_aloc_name loc then Expr.ALoc loc else Expr.Lit (Loc loc)
   in
@@ -359,8 +359,7 @@ let assertions (heap : t) : Asrt.t list =
     fv_assertions @ domain @ metadata
   in
 
-  List.sort Asrt.compare
-    (List.concat (List.map assertions_of_object (to_list heap)))
+  List.sort Asrt.compare (List.concat_map assertions_of_object (to_list heap))
 
 let wf_assertions_of_obj (heap : t) (loc : string) : Formula.t list =
   let cfvl =
diff --git a/Gillian-JS/lib/utils/asrt_utils.ml b/Gillian-JS/lib/utils/asrt_utils.ml
index 4513c7f7..a90cf487 100644
--- a/Gillian-JS/lib/utils/asrt_utils.ml
+++ b/Gillian-JS/lib/utils/asrt_utils.ml
@@ -1,6 +1,6 @@
 open JSILNames
 open Gillian.Gil_syntax.Asrt
 
-let points_to ~loc ~field ~value = GA (aCell, [ loc; field ], [ value ])
-let metadata ~loc ~metadata = GA (aMetadata, [ loc ], [ metadata ])
-let empty_fields ~loc ~domain = GA (aProps, [ loc; domain ], [])
+let points_to ~loc ~field ~value = CorePred (aCell, [ loc; field ], [ value ])
+let metadata ~loc ~metadata = CorePred (aMetadata, [ loc ], [ metadata ])
+let empty_fields ~loc ~domain = CorePred (aProps, [ loc; domain ], [])
diff --git a/GillianCore/GIL_Syntax/Asrt.ml b/GillianCore/GIL_Syntax/Asrt.ml
index e47e70a1..c8dc67f7 100644
--- a/GillianCore/GIL_Syntax/Asrt.ml
+++ b/GillianCore/GIL_Syntax/Asrt.ml
@@ -1,15 +1,19 @@
 (** {b GIL logic assertions}. *)
-type t = TypeDef__.assertion =
+type simple = TypeDef__.assertion_simple =
   | Emp  (** Empty heap             *)
-  | Star of t * t  (** Separating conjunction *)
   | Pred of string * Expr.t list  (** Predicates             *)
   | Pure of Formula.t  (** Pure formula           *)
   | Types of (Expr.t * Type.t) list  (** Typing assertion       *)
-  | GA of string * Expr.t list * Expr.t list  (** Core assertion         *)
+  | CorePred of string * Expr.t list * Expr.t list
+      (** Core assertion         *)
   | Wand of { lhs : string * Expr.t list; rhs : string * Expr.t list }
       (** Magic wand of the form [P(...) -* Q(...)] *)
 [@@deriving eq]
 
+type t = TypeDef__.assertion [@@deriving eq]
+
+let simple_to_yojson = TypeDef__.assertion_simple_to_yojson
+let simple_of_yojson = TypeDef__.assertion_simple_of_yojson
 let to_yojson = TypeDef__.assertion_to_yojson
 let of_yojson = TypeDef__.assertion_of_yojson
 
@@ -27,7 +31,7 @@ let compare x y =
   | _, Types _ -> 1
   | _, _ -> cmp x y
 
-let prioritise (a1 : t) (a2 : t) =
+let prioritise (a1 : simple) (a2 : simple) =
   let lloc_aloc_pvar_lvar e1 e2 =
     match ((e1 : Expr.t), (e2 : Expr.t)) with
     | Lit (Loc _), Lit (Loc _) -> 0
@@ -65,65 +69,43 @@ end
 module Set = Set.Make (MyAssertion)
 
 (** Deprecated, use {!Visitors.endo} instead. *)
-let rec map
-    (f_a_before : (t -> t * bool) option)
-    (f_a_after : (t -> t) option)
-    (f_e : (Expr.t -> Expr.t) option)
-    (f_p : (Formula.t -> Formula.t) option)
-    (a : t) : t =
-  (* Map recursively to assertions and expressions *)
-  let map_a = map f_a_before f_a_after f_e f_p in
-  let map_e = Option.value ~default:(fun x -> x) f_e in
-  let map_p = Option.value ~default:(Formula.map None None (Some map_e)) f_p in
-  let f_a_before = Option.value ~default:(fun x -> (x, true)) f_a_before in
-  let f_a_after = Option.value ~default:(fun x -> x) f_a_after in
-  let a', recurse = f_a_before a in
-
-  if not recurse then a'
-  else
-    let a'' =
-      match a' with
-      | Star (a1, a2) -> Star (map_a a1, map_a a2)
-      | Emp -> Emp
-      | Pred (s, le) -> Pred (s, List.map map_e le)
-      | Pure form -> Pure (map_p form)
-      | Types lt -> Types (List.map (fun (exp, typ) -> (map_e exp, typ)) lt)
-      | GA (x, es1, es2) -> GA (x, List.map map_e es1, List.map map_e es2)
-      | Wand { lhs = lhs_pred, lhs_args; rhs = rhs_pred, rhs_args } ->
-          Wand
-            {
-              lhs = (lhs_pred, List.map map_e lhs_args);
-              rhs = (rhs_pred, List.map map_e rhs_args);
-            }
-    in
-    f_a_after a''
+let map (f_e : Expr.t -> Expr.t) (f_p : Formula.t -> Formula.t) : t -> t =
+  List.map (function
+    | Emp -> Emp
+    | Pred (s, le) -> Pred (s, List.map f_e le)
+    | Pure form -> Pure (f_p form)
+    | Types lt -> Types (List.map (fun (exp, typ) -> (f_e exp, typ)) lt)
+    | CorePred (x, es1, es2) -> CorePred (x, List.map f_e es1, List.map f_e es2)
+    | Wand { lhs = lhs_pred, lhs_args; rhs = rhs_pred, rhs_args } ->
+        Wand
+          {
+            lhs = (lhs_pred, List.map f_e lhs_args);
+            rhs = (rhs_pred, List.map f_e rhs_args);
+          })
 
 (* Get all the logical expressions of --a-- that denote a list
    and are not logical variables *)
-let list_lexprs (a : t) : Expr.Set.t =
-  Formula.list_lexprs_collector#visit_assertion () a
+let list_lexprs : t -> Expr.Set.t =
+  Formula.list_lexprs_collector#visit_assertion ()
 
 (* Get all the logical variables in --a-- *)
-let lvars (a : t) : SS.t =
-  Visitors.Collectors.lvar_collector#visit_assertion SS.empty a
+let lvars : t -> SS.t =
+  Visitors.Collectors.lvar_collector#visit_assertion SS.empty
 
 (* Get all the program variables in --a-- *)
-let pvars (a : t) : SS.t =
-  Visitors.Collectors.pvar_collector#visit_assertion () a
+let pvars : t -> SS.t = Visitors.Collectors.pvar_collector#visit_assertion ()
 
 (* Get all the abstract locations in --a-- *)
-let alocs (a : t) : SS.t =
-  Visitors.Collectors.aloc_collector#visit_assertion () a
+let alocs : t -> SS.t = Visitors.Collectors.aloc_collector#visit_assertion ()
 
 (* Get all the concrete locations in [a] *)
-let clocs (a : t) : SS.t =
-  Visitors.Collectors.cloc_collector#visit_assertion () a
+let clocs : t -> SS.t = Visitors.Collectors.cloc_collector#visit_assertion ()
 
 (* Get all the concrete locations in [a] *)
-let locs (a : t) : SS.t = Visitors.Collectors.loc_collector#visit_assertion () a
+let locs : t -> SS.t = Visitors.Collectors.loc_collector#visit_assertion ()
 
 (* Returns a list with the names of the predicates that occur in --a-- *)
-let pred_names (a : t) : string list =
+let pred_names : t -> string list =
   let collector =
     object
       inherit [_] Visitors.reduce
@@ -131,10 +113,10 @@ let pred_names (a : t) : string list =
       method! visit_Pred () name _ = [ name ]
     end
   in
-  collector#visit_assertion () a
+  collector#visit_assertion ()
 
 (* Returns a list with the pure assertions that occur in --a-- *)
-let pure_asrts (a : t) : Formula.t list =
+let pure_asrts : t -> Formula.t list =
   let collector =
     object
       inherit [_] Visitors.reduce
@@ -142,122 +124,62 @@ let pure_asrts (a : t) : Formula.t list =
       method! visit_Pure () f = [ f ]
     end
   in
-  collector#visit_assertion () a
-
-(* Returns a list with the simple assertions that occur in --a-- *)
-let rec simple_asrts (a : t) : t list =
-  match a with
-  | Emp -> []
-  | Star (a1, a2) -> simple_asrts a1 @ simple_asrts a2
-  | _ -> [ a ]
+  collector#visit_assertion ()
 
 (* Check if --a-- is a pure assertion *)
-let rec is_pure_asrt (a : t) : bool =
-  match a with
-  | Pred _ | GA _ -> false
-  | Star (a1, a2) -> is_pure_asrt a1 && is_pure_asrt a2
+let is_pure_asrt : simple -> bool = function
+  | Pred _ | CorePred _ | Wand _ -> false
   | _ -> true
 
-(* Check if --a-- is a pure assertion & non-recursive assertion.
-   It assumes that only pure assertions are universally quantified *)
-let is_pure_non_rec_asrt (a : t) : bool =
-  match a with
-  | Pure _ | Types _ | Emp -> true
-  | _ -> false
-
 (* Eliminate LStar and LTypes assertions.
    LTypes disappears. LStar is replaced by LAnd.
    This function expects its argument to be a PURE assertion. *)
 let make_pure (a : t) : Formula.t =
-  let s_asrts = simple_asrts a in
-  let all_pure = List.for_all is_pure_non_rec_asrt s_asrts in
-  if all_pure then
-    let fs =
-      List.map
-        (fun a ->
-          match a with
-          | Pure f -> f
-          | _ -> raise (Failure "DEATH. make_pure"))
-        s_asrts
-    in
-    Formula.conjunct fs
-  else raise (Failure "DEATH. make_pure")
-
-let rec full_pp fmt a =
-  match a with
-  | Star (a1, a2) -> Fmt.pf fmt "%a *@ %a" full_pp a1 full_pp a2
-  | Emp -> Fmt.string fmt "emp"
-  | Pred (name, params) ->
-      let name = Pp_utils.maybe_quote_ident name in
-      Fmt.pf fmt "@[<h>%s(%a)@]" name
-        (Fmt.list ~sep:Fmt.comma Expr.full_pp)
-        params
-  | Types tls ->
-      let pp_tl f (e, t) = Fmt.pf f "%a : %s" Expr.full_pp e (Type.str t) in
-      Fmt.pf fmt "types(@[%a@])" (Fmt.list ~sep:Fmt.comma pp_tl) tls
-  | Pure f -> Formula.full_pp fmt f
-  | GA (a, ins, outs) ->
-      let pp_e_l = Fmt.list ~sep:Fmt.comma Expr.full_pp in
-      Fmt.pf fmt "@[<h><%s>(%a; %a)@]" a pp_e_l ins pp_e_l outs
-  | Wand { lhs = lname, largs; rhs = rname, rargs } ->
-      let lname = Pp_utils.maybe_quote_ident lname in
-      let rname = Pp_utils.maybe_quote_ident rname in
-      Fmt.pf fmt "(%s(%a) -* %s(%a))" lname
-        (Fmt.list ~sep:Fmt.comma Expr.full_pp)
-        largs rname
-        (Fmt.list ~sep:Fmt.comma Expr.full_pp)
-        rargs
+  a
+  |> List.filter_map (function
+       | Pure f -> Some f
+       | Emp -> None
+       | _ -> raise (Failure "DEATH. make_pure received unpure assertion"))
+  |> Formula.conjunct
 
 (** GIL logic assertions *)
-let rec pp fmt a =
-  match a with
-  | Star (a1, a2) -> Fmt.pf fmt "%a *@ %a" pp a1 pp a2
+let _pp_simple ?(e_pp : Format.formatter -> Expr.t -> unit = Expr.pp) fmt =
+  function
   | Emp -> Fmt.string fmt "emp"
   | Pred (name, params) ->
       let name = Pp_utils.maybe_quote_ident name in
-      Fmt.pf fmt "@[<h>%s(%a)@]" name (Fmt.list ~sep:Fmt.comma Expr.pp) params
+      Fmt.pf fmt "@[<h>%s(%a)@]" name (Fmt.list ~sep:Fmt.comma e_pp) params
   | Types tls ->
-      let pp_tl f (e, t) = Fmt.pf f "%a : %s" Expr.pp e (Type.str t) in
+      let pp_tl f (e, t) = Fmt.pf f "%a : %s" e_pp e (Type.str t) in
       Fmt.pf fmt "types(@[%a@])" (Fmt.list ~sep:Fmt.comma pp_tl) tls
   | Pure f -> Formula.pp fmt f
-  | GA (a, ins, outs) ->
-      let pp_e_l = Fmt.list ~sep:Fmt.comma Expr.pp in
+  | CorePred (a, ins, outs) ->
+      let pp_e_l = Fmt.list ~sep:Fmt.comma e_pp in
       Fmt.pf fmt "@[<h><%s>(%a; %a)@]" a pp_e_l ins pp_e_l outs
   | Wand { lhs = lname, largs; rhs = rname, rargs } ->
       let lname = Pp_utils.maybe_quote_ident lname in
       let rname = Pp_utils.maybe_quote_ident rname in
       Fmt.pf fmt "(%s(%a) -* %s(%a))" lname
-        (Fmt.list ~sep:Fmt.comma Expr.pp)
+        (Fmt.list ~sep:Fmt.comma e_pp)
         largs rname
-        (Fmt.list ~sep:Fmt.comma Expr.pp)
+        (Fmt.list ~sep:Fmt.comma e_pp)
         rargs
 
-let subst_clocs (subst : string -> Expr.t) (a : t) : t =
-  map None None
-    (Some (Expr.subst_clocs subst))
-    (Some (Formula.subst_clocs subst))
-    a
+let _pp ~(e_pp : Format.formatter -> Expr.t -> unit) (fmt : Format.formatter) :
+    t -> unit =
+  Fmt.list ~sep:(Fmt.any " *@ ") (_pp_simple ~e_pp) fmt
 
-let subst_expr_for_expr ~(to_subst : Expr.t) ~(subst_with : Expr.t) (a : t) : t
-    =
-  map None None
-    (Some (Expr.subst_expr_for_expr ~to_subst ~subst_with))
-    (Some (Formula.subst_expr_for_expr ~to_subst ~subst_with))
-    a
+let pp_simple = _pp_simple ~e_pp:Expr.pp
+let pp_simple_full = _pp_simple ~e_pp:Expr.full_pp
+let pp = _pp ~e_pp:Expr.pp
+let full_pp = _pp ~e_pp:Expr.full_pp
 
-module Infix = struct
-  let ( ** ) a b =
-    match (a, b) with
-    | Pure True, x | x, Pure True | Emp, x | x, Emp -> x
-    | (Pure False as fl), _ | _, (Pure False as fl) -> fl
-    | _ -> Star (a, b)
-
-  let ( --* ) lhs rhs = Wand { lhs; rhs }
-end
+let subst_clocs (subst : string -> Expr.t) : t -> t =
+  map (Expr.subst_clocs subst) (Formula.subst_clocs subst)
 
-let star (asrts : t list) : t = List.fold_left Infix.( ** ) Emp asrts
+let subst_expr_for_expr ~(to_subst : Expr.t) ~(subst_with : Expr.t) : t -> t =
+  map
+    (Expr.subst_expr_for_expr ~to_subst ~subst_with)
+    (Formula.subst_expr_for_expr ~to_subst ~subst_with)
 
-let pvars_to_lvars (a : t) : t =
-  let ff = Formula.pvars_to_lvars in
-  let fe = Expr.pvars_to_lvars in
-  map None None (Some fe) (Some ff) a
+let pvars_to_lvars : t -> t = map Expr.pvars_to_lvars Formula.pvars_to_lvars
diff --git a/GillianCore/GIL_Syntax/Gil_syntax.mli b/GillianCore/GIL_Syntax/Gil_syntax.mli
index 9bdd4d22..4dbb6b89 100644
--- a/GillianCore/GIL_Syntax/Gil_syntax.mli
+++ b/GillianCore/GIL_Syntax/Gil_syntax.mli
@@ -563,34 +563,29 @@ end
 module Asrt : sig
   (** GIL Assertions *)
 
-  type t =
+  type simple =
     | Emp  (** Empty heap *)
-    | Star of t * t  (** Separating conjunction *)
     | Pred of string * Expr.t list  (** Predicates *)
     | Pure of Formula.t  (** Pure formula *)
     | Types of (Expr.t * Type.t) list  (** Typing assertion *)
-    | GA of string * Expr.t list * Expr.t list  (** Core assertion *)
+    | CorePred of string * Expr.t list * Expr.t list  (** Core assertion *)
     | Wand of { lhs : string * Expr.t list; rhs : string * Expr.t list }
         (** Magic wand of the form [P(...) -* Q(...)] *)
   [@@deriving yojson, eq]
 
+  type t = simple list [@@deriving yojson, eq]
+
   (** Comparison of assertions *)
-  val compare : t -> t -> int
+  val compare : simple -> simple -> int
 
   (** Sorting of assertions *)
-  val prioritise : t -> t -> int
+  val prioritise : simple -> simple -> int
 
   (** Sets of assertions *)
   module Set : Set.S with type elt := t
 
   (** @deprecated Use {!Visitors.endo} instead *)
-  val map :
-    (t -> t * bool) option ->
-    (t -> t) option ->
-    (Expr.t -> Expr.t) option ->
-    (Formula.t -> Formula.t) option ->
-    t ->
-    t
+  val map : (Expr.t -> Expr.t) -> (Formula.t -> Formula.t) -> t -> t
 
   (** Get all the logical expressions of [a] that denote a list
    and are not logical variables *)
@@ -617,15 +612,8 @@ module Asrt : sig
   (** Returns a list with the pure assertions that occur in [a] *)
   val pure_asrts : t -> Formula.t list
 
-  (** Returns a list with the pure assertions that occur in [a] *)
-  val simple_asrts : t -> t list
-
   (** Check if [a] is a pure assertion *)
-  val is_pure_asrt : t -> bool
-
-  (** Check if [a] is a pure assertion & non-recursive assertion.
-   It assumes that only pure assertions are universally quantified *)
-  val is_pure_non_rec_asrt : t -> bool
+  val is_pure_asrt : simple -> bool
 
   (** Eliminate LStar and LTypes assertions.
    LTypes disappears. LStar is replaced by LAnd.
@@ -635,11 +623,12 @@ module Asrt : sig
   (** Pretty-printer *)
   val pp : Format.formatter -> t -> unit
 
+  val pp_simple : Format.formatter -> simple -> unit
+
   (** Full pretty-printer *)
   val full_pp : Format.formatter -> t -> unit
 
-  (** [star \[a1; a2; ...; an\] will return \[a1 * a2 * ... * an\]] *)
-  val star : t list -> t
+  val pp_simple_full : Format.formatter -> simple -> unit
 
   (** [subst_clocs subst a] Substitutes expressions of the form [Lit (Loc l)] with [subst l] in [a] *)
   val subst_clocs : (string -> Expr.t) -> t -> t
@@ -649,11 +638,6 @@ module Asrt : sig
 
   (** Move pvars to lvars *)
   val pvars_to_lvars : t -> t
-
-  module Infix : sig
-    (** Star constructor *)
-    val ( ** ) : t -> t -> t
-  end
 end
 
 (** @canonical Gillian.Gil_syntax.SLCmd *)
@@ -676,12 +660,7 @@ module SLCmd : sig
     | SymbExec
 
   (** @deprecated Use {!Visitors.endo} instead *)
-  val map :
-    (t -> t) option ->
-    (Asrt.t -> Asrt.t) option ->
-    (Expr.t -> Expr.t) option ->
-    t ->
-    t
+  val map : (Asrt.t -> Asrt.t) -> (Expr.t -> Expr.t) -> t -> t
 
   (** Pretty-printer of folding info *)
   val pp_folding_info : (string * (string * Expr.t) list) option Fmt.t
@@ -708,10 +687,9 @@ module LCmd : sig
 
   (** @deprecated Use {!Visitors.endo} instead *)
   val map :
-    (t -> t) option ->
-    (Expr.t -> Expr.t) option ->
-    (Formula.t -> Formula.t) option ->
-    (SLCmd.t -> SLCmd.t) option ->
+    (Expr.t -> Expr.t) ->
+    (Formula.t -> Formula.t) ->
+    (SLCmd.t -> SLCmd.t) ->
     t ->
     t
 
@@ -845,7 +823,7 @@ module Pred : sig
 
   (** Given a guarded predicate, return a "call" to its close token.
       The arguments given are PVars with the same name as the ins of the predicate. *)
-  val close_token_call : t -> Asrt.t
+  val close_token_call : t -> Asrt.simple
 
   (** Given a name, if it's a close_token name, returns the name of the corresponding predicate,
    otherwise return None. *)
@@ -1322,7 +1300,7 @@ module Visitors : sig
              'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
          ; visit_EForall :
              'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
-         ; visit_Emp : 'c -> Asrt.t -> Asrt.t
+         ; visit_Emp : 'c -> Asrt.simple -> Asrt.simple
          ; visit_Empty : 'c -> Literal.t -> Literal.t
          ; visit_EmptyType : 'c -> Type.t -> Type.t
          ; visit_Epsilon : 'c -> Constant.t -> Constant.t
@@ -1352,14 +1330,19 @@ module Visitors : sig
              (string * Type.t option) list ->
              Formula.t ->
              Formula.t
-         ; visit_GA :
-             'c -> Asrt.t -> string -> Expr.t list -> Expr.t list -> Asrt.t
+         ; visit_CorePred :
+             'c ->
+             Asrt.simple ->
+             string ->
+             Expr.t list ->
+             Expr.t list ->
+             Asrt.simple
          ; visit_Wand :
              'c ->
-             Asrt.t ->
+             Asrt.simple ->
              string * Expr.t list ->
              string * Expr.t list ->
-             Asrt.t
+             Asrt.simple
          ; visit_GUnfold : 'c -> SLCmd.t -> string -> SLCmd.t
          ; visit_Goto : 'c -> 'f Cmd.t -> 'f -> 'f Cmd.t
          ; visit_GuardedGoto : 'c -> 'f Cmd.t -> Expr.t -> 'f -> 'f -> 'f Cmd.t
@@ -1437,8 +1420,9 @@ module Visitors : sig
          ; visit_PhiAssignment :
              'c -> 'f Cmd.t -> (string * Expr.t list) list -> 'f Cmd.t
          ; visit_Pi : 'c -> Constant.t -> Constant.t
-         ; visit_Pred : 'c -> Asrt.t -> string -> Expr.t list -> Asrt.t
-         ; visit_Pure : 'c -> Asrt.t -> Formula.t -> Asrt.t
+         ; visit_Pred :
+             'c -> Asrt.simple -> string -> Expr.t list -> Asrt.simple
+         ; visit_Pure : 'c -> Asrt.simple -> Formula.t -> Asrt.simple
          ; visit_Random : 'c -> Constant.t -> Constant.t
          ; visit_ReturnError : 'c -> 'f Cmd.t -> 'f Cmd.t
          ; visit_ReturnNormal : 'c -> 'f Cmd.t -> 'f Cmd.t
@@ -1457,7 +1441,6 @@ module Visitors : sig
          ; visit_SignedRightShiftF : 'c -> BinOp.t -> BinOp.t
          ; visit_Skip : 'c -> 'f Cmd.t -> 'f Cmd.t
          ; visit_FreshSVar : 'c -> LCmd.t -> string -> LCmd.t
-         ; visit_Star : 'c -> Asrt.t -> Asrt.t -> Asrt.t -> Asrt.t
          ; visit_StrCat : 'c -> BinOp.t -> BinOp.t
          ; visit_StrLen : 'c -> UnOp.t -> UnOp.t
          ; visit_NumToInt : 'c -> UnOp.t -> UnOp.t
@@ -1477,7 +1460,8 @@ module Visitors : sig
          ; visit_Type : 'c -> Literal.t -> Type.t -> Literal.t
          ; visit_TypeOf : 'c -> UnOp.t -> UnOp.t
          ; visit_TypeType : 'c -> Type.t -> Type.t
-         ; visit_Types : 'c -> Asrt.t -> (Expr.t * Type.t) list -> Asrt.t
+         ; visit_Types :
+             'c -> Asrt.simple -> (Expr.t * Type.t) list -> Asrt.simple
          ; visit_UNot : 'c -> UnOp.t -> UnOp.t
          ; visit_UTCTime : 'c -> Constant.t -> Constant.t
          ; visit_UnOp : 'c -> Expr.t -> UnOp.t -> Expr.t -> Expr.t
@@ -1500,6 +1484,7 @@ module Visitors : sig
          ; visit_UnsignedRightShift : 'c -> BinOp.t -> BinOp.t
          ; visit_UnsignedRightShiftL : 'c -> BinOp.t -> BinOp.t
          ; visit_UnsignedRightShiftF : 'c -> BinOp.t -> BinOp.t
+         ; visit_assertion_simple : 'c -> Asrt.simple -> Asrt.simple
          ; visit_assertion : 'c -> Asrt.t -> Asrt.t
          ; visit_bindings :
              'c ->
@@ -1591,7 +1576,7 @@ module Visitors : sig
     method visit_EForall :
       'c -> Expr.t -> (string * Type.t option) list -> Expr.t -> Expr.t
 
-    method visit_Emp : 'c -> Asrt.t -> Asrt.t
+    method visit_Emp : 'c -> Asrt.simple -> Asrt.simple
     method visit_Empty : 'c -> Literal.t -> Literal.t
     method visit_EmptyType : 'c -> Type.t -> Type.t
     method visit_Epsilon : 'c -> Constant.t -> Constant.t
@@ -1620,11 +1605,15 @@ module Visitors : sig
     method visit_ForAll :
       'c -> Formula.t -> (string * Type.t option) list -> Formula.t -> Formula.t
 
-    method visit_GA :
-      'c -> Asrt.t -> string -> Expr.t list -> Expr.t list -> Asrt.t
+    method visit_CorePred :
+      'c -> Asrt.simple -> string -> Expr.t list -> Expr.t list -> Asrt.simple
 
     method visit_Wand :
-      'c -> Asrt.t -> string * Expr.t list -> string * Expr.t list -> Asrt.t
+      'c ->
+      Asrt.simple ->
+      string * Expr.t list ->
+      string * Expr.t list ->
+      Asrt.simple
 
     method visit_GUnfold : 'c -> SLCmd.t -> string -> SLCmd.t
     method visit_Goto : 'c -> 'f Cmd.t -> 'f -> 'f Cmd.t
@@ -1709,8 +1698,11 @@ module Visitors : sig
       'c -> 'f Cmd.t -> (string * Expr.t list) list -> 'f Cmd.t
 
     method visit_Pi : 'c -> Constant.t -> Constant.t
-    method visit_Pred : 'c -> Asrt.t -> string -> Expr.t list -> Asrt.t
-    method visit_Pure : 'c -> Asrt.t -> Formula.t -> Asrt.t
+
+    method visit_Pred :
+      'c -> Asrt.simple -> string -> Expr.t list -> Asrt.simple
+
+    method visit_Pure : 'c -> Asrt.simple -> Formula.t -> Asrt.simple
     method visit_Random : 'c -> Constant.t -> Constant.t
     method visit_ReturnError : 'c -> 'f Cmd.t -> 'f Cmd.t
     method visit_ReturnNormal : 'c -> 'f Cmd.t -> 'f Cmd.t
@@ -1729,7 +1721,6 @@ module Visitors : sig
     method visit_SignedRightShiftF : 'c -> BinOp.t -> BinOp.t
     method visit_Skip : 'c -> 'f Cmd.t -> 'f Cmd.t
     method visit_FreshSVar : 'c -> LCmd.t -> string -> LCmd.t
-    method visit_Star : 'c -> Asrt.t -> Asrt.t -> Asrt.t -> Asrt.t
     method visit_StrCat : 'c -> BinOp.t -> BinOp.t
     method visit_StrLen : 'c -> UnOp.t -> UnOp.t
     method visit_IntToNum : 'c -> UnOp.t -> UnOp.t
@@ -1749,7 +1740,10 @@ module Visitors : sig
     method visit_Type : 'c -> Literal.t -> Type.t -> Literal.t
     method visit_TypeOf : 'c -> UnOp.t -> UnOp.t
     method visit_TypeType : 'c -> Type.t -> Type.t
-    method visit_Types : 'c -> Asrt.t -> (Expr.t * Type.t) list -> Asrt.t
+
+    method visit_Types :
+      'c -> Asrt.simple -> (Expr.t * Type.t) list -> Asrt.simple
+
     method visit_UNot : 'c -> UnOp.t -> UnOp.t
     method visit_UTCTime : 'c -> Constant.t -> Constant.t
     method visit_UnOp : 'c -> Expr.t -> UnOp.t -> Expr.t -> Expr.t
@@ -1775,6 +1769,7 @@ module Visitors : sig
     method private visit_array :
       'env 'a. ('env -> 'a -> 'a) -> 'env -> 'a array -> 'a array
 
+    method visit_assertion_simple : 'c -> Asrt.simple -> Asrt.simple
     method visit_assertion : 'c -> Asrt.t -> Asrt.t
 
     method visit_bindings :
@@ -1905,7 +1900,7 @@ module Visitors : sig
              (string * (string * Expr.t) list) option ->
              'f
          ; visit_ForAll : 'c -> (string * Type.t option) list -> Formula.t -> 'f
-         ; visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> 'f
+         ; visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> 'f
          ; visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> 'f
          ; visit_GUnfold : 'c -> string -> 'f
          ; visit_Goto : 'c -> 'g -> 'f
@@ -2003,7 +1998,6 @@ module Visitors : sig
          ; visit_SignedRightShiftF : 'c -> 'f
          ; visit_Skip : 'c -> 'f
          ; visit_FreshSVar : 'c -> string -> 'f
-         ; visit_Star : 'c -> Asrt.t -> Asrt.t -> 'f
          ; visit_StrCat : 'c -> 'f
          ; visit_StrLen : 'c -> 'f
          ; visit_IntToNum : 'c -> 'f
@@ -2045,6 +2039,7 @@ module Visitors : sig
          ; visit_UnsignedRightShift : 'c -> 'f
          ; visit_UnsignedRightShiftL : 'c -> 'f
          ; visit_UnsignedRightShiftF : 'c -> 'f
+         ; visit_assertion_simple : 'c -> Asrt.simple -> 'f
          ; visit_assertion : 'c -> Asrt.t -> 'f
          ; visit_bindings : 'c -> string * (string * Expr.t) list -> 'f
          ; visit_binop : 'c -> BinOp.t -> 'f
@@ -2143,7 +2138,7 @@ module Visitors : sig
       'f
 
     method visit_ForAll : 'c -> (string * Type.t option) list -> Formula.t -> 'f
-    method visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> 'f
+    method visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> 'f
     method visit_Wand : 'c -> string * Expr.t list -> string * Expr.t list -> 'f
     method visit_GUnfold : 'c -> string -> 'f
     method visit_Goto : 'c -> 'g -> 'f
@@ -2241,7 +2236,6 @@ module Visitors : sig
     method visit_SignedRightShiftF : 'c -> 'f
     method visit_Skip : 'c -> 'f
     method visit_FreshSVar : 'c -> string -> 'f
-    method visit_Star : 'c -> Asrt.t -> Asrt.t -> 'f
     method visit_StrCat : 'c -> 'f
     method visit_StrLen : 'c -> 'f
     method visit_IntToNum : 'c -> 'f
@@ -2281,6 +2275,7 @@ module Visitors : sig
     method visit_UnsignedRightShift : 'c -> 'f
     method visit_UnsignedRightShiftL : 'c -> 'f
     method visit_UnsignedRightShiftF : 'c -> 'f
+    method visit_assertion_simple : 'c -> Asrt.simple -> 'f
     method visit_assertion : 'c -> Asrt.t -> 'f
     method visit_bindings : 'c -> string * (string * Expr.t) list -> 'f
     method visit_binop : 'c -> BinOp.t -> 'f
@@ -2382,7 +2377,7 @@ module Visitors : sig
              unit
          ; visit_ForAll :
              'c -> (string * Type.t option) list -> Formula.t -> unit
-         ; visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> unit
+         ; visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> unit
          ; visit_Wand :
              'c -> string * Expr.t list -> string * Expr.t list -> unit
          ; visit_GUnfold : 'c -> string -> unit
@@ -2479,7 +2474,6 @@ module Visitors : sig
          ; visit_SignedRightShiftF : 'c -> unit
          ; visit_Skip : 'c -> unit
          ; visit_FreshSVar : 'c -> string -> unit
-         ; visit_Star : 'c -> Asrt.t -> Asrt.t -> unit
          ; visit_StrCat : 'c -> unit
          ; visit_StrLen : 'c -> unit
          ; visit_IntToNum : 'c -> unit
@@ -2517,6 +2511,7 @@ module Visitors : sig
          ; visit_UnsignedRightShift : 'c -> unit
          ; visit_UnsignedRightShiftL : 'c -> unit
          ; visit_UnsignedRightShiftF : 'c -> unit
+         ; visit_assertion_simple : 'c -> Asrt.simple -> unit
          ; visit_assertion : 'c -> Asrt.t -> unit
          ; visit_bindings : 'c -> string * (string * Expr.t) list -> unit
          ; visit_binop : 'c -> BinOp.t -> unit
@@ -2622,7 +2617,7 @@ module Visitors : sig
     method visit_ForAll :
       'c -> (string * Type.t option) list -> Formula.t -> unit
 
-    method visit_GA : 'c -> string -> Expr.t list -> Expr.t list -> unit
+    method visit_CorePred : 'c -> string -> Expr.t list -> Expr.t list -> unit
 
     method visit_Wand :
       'c -> string * Expr.t list -> string * Expr.t list -> unit
@@ -2721,7 +2716,6 @@ module Visitors : sig
     method visit_SignedRightShiftF : 'c -> unit
     method visit_Skip : 'c -> unit
     method visit_FreshSVar : 'c -> string -> unit
-    method visit_Star : 'c -> Asrt.t -> Asrt.t -> unit
     method visit_StrCat : 'c -> unit
     method visit_StrLen : 'c -> unit
     method visit_IntToNum : 'c -> unit
@@ -2766,6 +2760,7 @@ module Visitors : sig
     method private visit_array :
       'env 'a. ('env -> 'a -> unit) -> 'env -> 'a array -> unit
 
+    method visit_assertion_simple : 'c -> Asrt.simple -> unit
     method visit_assertion : 'c -> Asrt.t -> unit
     method visit_bindings : 'c -> string * (string * Expr.t) list -> unit
     method visit_binop : 'c -> BinOp.t -> unit
diff --git a/GillianCore/GIL_Syntax/LCmd.ml b/GillianCore/GIL_Syntax/LCmd.ml
index 71242700..fbcb53e4 100644
--- a/GillianCore/GIL_Syntax/LCmd.ml
+++ b/GillianCore/GIL_Syntax/LCmd.ml
@@ -14,30 +14,19 @@ type t = TypeDef__.lcmd =
 [@@deriving yojson]
 
 let rec map
-    (f_l : (t -> t) option)
-    (f_e : (Expr.t -> Expr.t) option)
-    (f_p : (Formula.t -> Formula.t) option)
-    (f_sl : (SLCmd.t -> SLCmd.t) option)
-    (lcmd : t) : t =
-  (* Functions to map over formulas, expressions, and sl-commands *)
-  let f = map f_l f_e f_p f_sl in
-  let map_e = Option.value ~default:(fun x -> x) f_e in
-  let map_p = Option.value ~default:(fun x -> x) f_p in
-  let map_sl = Option.value ~default:(fun x -> x) f_sl in
-
-  (* Apply the given function to the logical command *)
-  let mapped_lcmd = Option.fold ~some:(fun f -> f lcmd) ~none:lcmd f_l in
-
-  (* Map over the elements of the command *)
-  match mapped_lcmd with
-  | Branch a -> Branch (map_p a)
-  | If (e, l1, l2) -> If (map_e e, List.map f l1, List.map f l2)
-  | Macro (s, l) -> Macro (s, List.map map_e l)
-  | Assume a -> Assume (map_p a)
-  | Assert a -> Assert (map_p a)
-  | AssumeType (e, t) -> AssumeType (map_e e, t)
-  | FreshSVar _ -> mapped_lcmd
-  | SL sl_cmd -> SL (map_sl sl_cmd)
+    (f_e : Expr.t -> Expr.t)
+    (f_p : Formula.t -> Formula.t)
+    (f_sl : SLCmd.t -> SLCmd.t) =
+  let f = map f_e f_p f_sl in
+  function
+  | Branch a -> Branch (f_p a)
+  | If (e, l1, l2) -> If (f_e e, List.map f l1, List.map f l2)
+  | Macro (s, l) -> Macro (s, List.map f_e l)
+  | Assume a -> Assume (f_p a)
+  | Assert a -> Assert (f_p a)
+  | AssumeType (e, t) -> AssumeType (f_e e, t)
+  | FreshSVar _ as lcmd -> lcmd
+  | SL sl_cmd -> SL (f_sl sl_cmd)
 
 let fold = List.fold_left SS.union SS.empty
 
diff --git a/GillianCore/GIL_Syntax/Lemma.ml b/GillianCore/GIL_Syntax/Lemma.ml
index ad40a132..de8f19e1 100644
--- a/GillianCore/GIL_Syntax/Lemma.ml
+++ b/GillianCore/GIL_Syntax/Lemma.ml
@@ -48,43 +48,11 @@ let pp fmt lemma =
     lemma.lemma_specs (Fmt.option pp_proof) lemma.lemma_proof
 
 let parameter_types (preds : (string, Pred.t) Hashtbl.t) (lemma : t) : t =
-  (* copied from spec - needs refactoring *)
-  let pt_asrt (a : Asrt.t) : Asrt.t =
-    let f_a_after a : Asrt.t =
-      match (a : Asrt.t) with
-      | Pred (name, les) ->
-          let pred =
-            try Hashtbl.find preds name
-            with _ ->
-              raise
-                (Failure
-                   ("DEATH. parameter_types: predicate " ^ name
-                  ^ " does not exist."))
-          in
-          (* Printf.printf "Pred: %s\n\tParams1: %s\n\tParams2: %s\n" name
-             (String.concat ", " (let x, _ = List.split pred.params in x)) (String.concat ", " (List.map (Fmt.to_to_string Expr.pp) les)); *)
-          let ac_types =
-            List.fold_left
-              (fun ac_types ((_, t_x), le) ->
-                match t_x with
-                | None -> ac_types
-                | Some t_x -> (le, t_x) :: ac_types)
-              []
-              (try List.combine pred.pred_params les
-               with Invalid_argument _ ->
-                 Fmt.failwith
-                   "Invalid number of arguments: %a.\nInside of lemma: %s"
-                   Asrt.pp a lemma.lemma_name)
-          in
-          Star (Types ac_types, a)
-      | _ -> a
-    in
-    Asrt.map None (Some f_a_after) None None a
-  in
+  let map_asrts = Pred.extend_asrt_pred_types preds in
   let pt_spec { lemma_hyp; lemma_concs; lemma_spec_variant } =
     {
-      lemma_hyp = pt_asrt lemma_hyp;
-      lemma_concs = List.map pt_asrt lemma_concs;
+      lemma_hyp = map_asrts lemma_hyp;
+      lemma_concs = List.map map_asrts lemma_concs;
       lemma_spec_variant;
     }
   in
@@ -99,8 +67,5 @@ let add_param_bindings (lemma : t) =
       (fun pv lv -> Asrt.Pure (Eq (PVar pv, LVar lv)))
       params lvar_params
   in
-  let param_eqs = Asrt.star param_eqs in
-  let add_to_spec spec =
-    { spec with lemma_hyp = Asrt.Star (param_eqs, spec.lemma_hyp) }
-  in
+  let add_to_spec spec = { spec with lemma_hyp = param_eqs @ spec.lemma_hyp } in
   { lemma with lemma_specs = List.map add_to_spec lemma.lemma_specs }
diff --git a/GillianCore/GIL_Syntax/Pred.ml b/GillianCore/GIL_Syntax/Pred.ml
index 32a39b63..f2d083b9 100644
--- a/GillianCore/GIL_Syntax/Pred.ml
+++ b/GillianCore/GIL_Syntax/Pred.ml
@@ -177,54 +177,48 @@ let check_pvars (predicates : (string, t) Hashtbl.t) : unit =
 
   Hashtbl.iter check_pred_pvars predicates
 
+let extend_asrt_pred_types (preds : (string, t) Hashtbl.t) : Asrt.t -> Asrt.t =
+  List.concat_map @@ function
+  | Asrt.Pred (name, les) as a ->
+      let pred =
+        try Hashtbl.find preds name
+        with _ ->
+          raise
+            (Failure
+               ("DEATH. parameter_types: predicate " ^ name ^ " does not exist."))
+      in
+      Logging.tmi (fun fmt ->
+          fmt "Gillian explicit param types: %s (%d, %d)" pred.pred_name
+            (List.length pred.pred_params)
+            (List.length les));
+      let combined =
+        try List.combine pred.pred_params les
+        with Invalid_argument _ ->
+          let message =
+            Fmt.str
+              "Invalid number of parameters for predicate %s which requires %i \
+               parameters and was used with the following %i parameters: %a"
+              pred.pred_name pred.pred_num_params (List.length les)
+              (Fmt.Dump.list Expr.pp) les
+          in
+          raise (Invalid_argument message)
+      in
+      let ac_types =
+        List.fold_left
+          (fun ac_types ((_, t_x), le) ->
+            match t_x with
+            | None -> ac_types
+            | Some t_x -> (le, t_x) :: ac_types)
+          [] combined
+      in
+      [ Asrt.Types ac_types; a ]
+  | a -> [ a ]
+
 (**
    GIL Predicates can have non-pvar parameters - to say that a given parameter
    always has a certain value...
   *)
 let explicit_param_types (preds : (string, t) Hashtbl.t) (pred : t) : t =
-  let pt_asrt (a : Asrt.t) : Asrt.t =
-    let f_a_after a : Asrt.t =
-      match (a : Asrt.t) with
-      | Pred (name, les) ->
-          let pred =
-            try Hashtbl.find preds name
-            with _ ->
-              raise
-                (Failure
-                   ("DEATH. parameter_types: predicate " ^ name
-                  ^ " does not exist."))
-          in
-          Logging.tmi (fun fmt ->
-              fmt "Gillian explicit param types: %s (%d, %d)" pred.pred_name
-                (List.length pred.pred_params)
-                (List.length les));
-          let combined =
-            try List.combine pred.pred_params les
-            with Invalid_argument _ ->
-              let message =
-                Fmt.str
-                  "Invalid number of parameters for predicate %s which \
-                   requires %i parameters and was used with the following %i \
-                   parameters: %a"
-                  pred.pred_name pred.pred_num_params (List.length les)
-                  (Fmt.Dump.list Expr.pp) les
-              in
-              raise (Invalid_argument message)
-          in
-          let ac_types =
-            List.fold_left
-              (fun ac_types ((_, t_x), le) ->
-                match t_x with
-                | None -> ac_types
-                | Some t_x -> (le, t_x) :: ac_types)
-              [] combined
-          in
-          Star (Types ac_types, a)
-      | _ -> a
-    in
-    Asrt.map None (Some f_a_after) None None a
-  in
-
   let new_asrts =
     List.fold_right
       (fun (x, t_x) new_asrts ->
@@ -235,7 +229,7 @@ let explicit_param_types (preds : (string, t) Hashtbl.t) (pred : t) : t =
   in
   let new_defs =
     List.map
-      (fun (oid, a) -> (oid, pt_asrt (Asrt.star (a :: new_asrts))))
+      (fun (oid, a) -> (oid, extend_asrt_pred_types preds (a @ new_asrts)))
       pred.pred_definitions
   in
   let new_facts =
@@ -321,7 +315,7 @@ let close_token_name (pred : t) : string =
     failwith "close_token_name called on non-guarded predicate";
   pred.pred_name ^ close_suffix
 
-let close_token_call (pred : t) : Asrt.t =
+let close_token_call (pred : t) : Asrt.simple =
   let name = close_token_name pred in
   let args =
     in_args pred pred.pred_params |> List.map (fun (x, _t) -> Expr.PVar x)
diff --git a/GillianCore/GIL_Syntax/SLCmd.ml b/GillianCore/GIL_Syntax/SLCmd.ml
index 43ba2d2e..584e5235 100644
--- a/GillianCore/GIL_Syntax/SLCmd.ml
+++ b/GillianCore/GIL_Syntax/SLCmd.ml
@@ -26,40 +26,23 @@ type t = TypeDef__.slcmd =
   | SymbExec
 [@@deriving yojson]
 
-let map
-    (f_l : (t -> t) option)
-    (f_a : (Asrt.t -> Asrt.t) option)
-    (f_e : (Expr.t -> Expr.t) option)
-    (lcmd : t) : t =
-  (* Functions to map over assertions and expressions *)
-  let map_e = Option.value ~default:(fun x -> x) f_e in
-  let map_a = Option.value ~default:(fun x -> x) f_a in
-
-  let mapped_lcmd = Option.fold ~some:(fun f -> f lcmd) ~none:lcmd f_l in
-
-  (* Map over the elements of the command *)
-  match mapped_lcmd with
-  | Fold (name, les, None) -> Fold (name, List.map map_e les, None)
+let map (f_a : Asrt.t -> Asrt.t) (f_e : Expr.t -> Expr.t) : t -> t = function
+  | Fold (name, les, None) -> Fold (name, List.map f_e les, None)
   | Fold (name, les, Some (s, l)) ->
       Fold
-        ( name,
-          List.map map_e les,
-          Some (s, List.map (fun (x, e) -> (x, map_e e)) l) )
+        (name, List.map f_e les, Some (s, List.map (fun (x, e) -> (x, f_e e)) l))
   | Unfold (name, les, unfold_info, b) ->
-      Unfold (name, List.map map_e les, unfold_info, b)
+      Unfold (name, List.map f_e les, unfold_info, b)
   | GUnfold name -> GUnfold name
-  | ApplyLem (s, l, existentials) -> ApplyLem (s, List.map map_e l, existentials)
-  | SepAssert (a, binders) -> SepAssert (map_a a, binders)
-  | Invariant (a, existentials) -> Invariant (map_a a, existentials)
-  | Consume (a, binders) -> Consume (map_a a, binders)
-  | Produce a -> Produce (map_a a)
+  | ApplyLem (s, l, existentials) -> ApplyLem (s, List.map f_e l, existentials)
+  | SepAssert (a, binders) -> SepAssert (f_a a, binders)
+  | Invariant (a, existentials) -> Invariant (f_a a, existentials)
+  | Consume (a, binders) -> Consume (f_a a, binders)
+  | Produce a -> Produce (f_a a)
   | SymbExec -> SymbExec
   | Package { lhs = lname, largs; rhs = rname, rargs } ->
       Package
-        {
-          lhs = (lname, List.map map_e largs);
-          rhs = (rname, List.map map_e rargs);
-        }
+        { lhs = (lname, List.map f_e largs); rhs = (rname, List.map f_e rargs) }
 
 let fold = List.fold_left SS.union SS.empty
 
diff --git a/GillianCore/GIL_Syntax/Spec.ml b/GillianCore/GIL_Syntax/Spec.ml
index f9350355..5dc96161 100644
--- a/GillianCore/GIL_Syntax/Spec.ml
+++ b/GillianCore/GIL_Syntax/Spec.ml
@@ -76,51 +76,12 @@ let pp fmt spec =
     spec.spec_sspecs
 
 let parameter_types (preds : (string, Pred.t) Hashtbl.t) (spec : t) : t =
-  let pt_asrt (a : Asrt.t) : Asrt.t =
-    let f_a_after a : Asrt.t =
-      match (a : Asrt.t) with
-      | Pred (name, les) ->
-          let pred =
-            try Hashtbl.find preds name
-            with _ ->
-              raise
-                (Failure
-                   ("DEATH. parameter_types: predicate " ^ name
-                  ^ " does not exist."))
-          in
-          (* Printf.printf "Pred: %s\n\tParams1: %s\n\tParams2: %s\n" name
-             (String.concat ", " (let x, _ = List.split pred.params in x)) (String.concat ", " (List.map (Fmt.to_to_string Expr.pp) les)); *)
-          let combined_params =
-            try List.combine pred.pred_params les
-            with Invalid_argument _ ->
-              let message =
-                Fmt.str
-                  "Predicate %s is expecting %i arguments but is used with the \
-                   following %i arguments : %a"
-                  pred.pred_name pred.pred_num_params (List.length les)
-                  (Fmt.Dump.list Expr.pp) les
-              in
-              raise (Invalid_argument message)
-          in
-          let ac_types =
-            List.fold_left
-              (fun ac_types ((_, t_x), le) ->
-                match t_x with
-                | None -> ac_types
-                | Some t_x -> (le, t_x) :: ac_types)
-              [] combined_params
-          in
-          Star (Types ac_types, a)
-      | _ -> a
-    in
-    Asrt.map None (Some f_a_after) None None a
-  in
-
+  let map_asrts = Pred.extend_asrt_pred_types preds in
   let pt_sspec (sspec : st) : st =
     {
       sspec with
-      ss_pre = pt_asrt sspec.ss_pre;
-      ss_posts = List.map pt_asrt sspec.ss_posts;
+      ss_pre = map_asrts sspec.ss_pre;
+      ss_posts = List.map map_asrts sspec.ss_posts;
     }
   in
   { spec with spec_sspecs = List.map pt_sspec spec.spec_sspecs }
diff --git a/GillianCore/GIL_Syntax/TypeDef__.ml b/GillianCore/GIL_Syntax/TypeDef__.ml
index 0ae9811b..49473e46 100644
--- a/GillianCore/GIL_Syntax/TypeDef__.ml
+++ b/GillianCore/GIL_Syntax/TypeDef__.ml
@@ -162,15 +162,15 @@ and formula =
   | ForAll of (string * typ option) list * formula
   | IsInt of expr
 
-and assertion =
+and assertion_simple =
   | Emp
-  | Star of assertion * assertion
   | Pred of string * expr list
   | Pure of formula
   | Types of (expr * typ) list
-  | GA of string * expr list * expr list
+  | CorePred of string * expr list * expr list
   | Wand of { lhs : string * expr list; rhs : string * expr list }
 
+and assertion = assertion_simple list
 and bindings = string * (string * expr) list
 
 and slcmd =
diff --git a/GillianCore/debugging/utils/match_map.ml b/GillianCore/debugging/utils/match_map.ml
index 05a10c68..364c1957 100644
--- a/GillianCore/debugging/utils/match_map.ml
+++ b/GillianCore/debugging/utils/match_map.ml
@@ -63,7 +63,7 @@ functor
         in
         let assertion =
           let asrt, _ = asrt_report.step in
-          Fmt.str "%a" Asrt.pp asrt
+          Fmt.str "%a" Asrt.pp_simple asrt
         in
         let substitutions =
           asrt_report.subst |> Subst.to_list_pp
diff --git a/GillianCore/engine/Abstraction/LogicPreprocessing.ml b/GillianCore/engine/Abstraction/LogicPreprocessing.ml
index 19f8751b..a499b837 100644
--- a/GillianCore/engine/Abstraction/LogicPreprocessing.ml
+++ b/GillianCore/engine/Abstraction/LogicPreprocessing.ml
@@ -12,74 +12,93 @@ let rec auto_unfold
     (predicates : (string, Pred.t) Hashtbl.t)
     (rec_tbl : (string, bool) Hashtbl.t)
     (asrt : Asrt.t) : Asrt.t list =
-  let au_rec = auto_unfold ~unfold_rec_predicates predicates rec_tbl in
   let au_no_rec = auto_unfold ~unfold_rec_predicates:false predicates rec_tbl in
-  match (asrt : Asrt.t) with
-  | Star (a1, a2) ->
-      List.filter Simplifications.admissible_assertion
-        (List_utils.cross_product (au_rec a1) (au_rec a2) (fun asrt1 asrt2 ->
-             Asrt.Star (asrt1, asrt2)))
-  (* We don't unfold:
-      - Recursive predicates (except in some very specific cases)
-      - predicates marked with no-unfold
-      - predicates with a guard *)
-  | Pred (name, _)
-    when (Hashtbl.find rec_tbl name && not unfold_rec_predicates)
-         ||
-         let pred = Hashtbl.find predicates name in
-         pred.pred_nounfold || Option.is_some pred.pred_guard -> [ asrt ]
-  | Pred (name, args) when Hashtbl.mem unfolded_preds name ->
-      L.verbose (fun fmt ->
-          fmt "Unfolding predicate: %s with nounfold %b" name
-            (Hashtbl.find predicates name).pred_nounfold);
-      let pred = Hashtbl.find unfolded_preds name in
-      let params, _ = List.split pred.pred_params in
-      let combined =
-        try List.combine params args
-        with Invalid_argument _ ->
-          Fmt.failwith
-            "Impossible to auto unfold predicate %s. Used with %i args instead \
-             of %i"
-            name (List.length args) (List.length params)
-      in
-      let subst = SVal.SSubst.init combined in
-      let defs = List.map (fun (_, def) -> def) pred.pred_definitions in
-      List.map (SVal.SSubst.substitute_asrt subst ~partial:false) defs
-  | Pred (name, args) -> (
-      try
-        L.tmi (fun fmt -> fmt "AutoUnfold: %a : %s" Asrt.pp asrt name);
-        let pred : Pred.t = Hashtbl.find predicates name in
-        (* If it is not, replace the predicate assertion for the list of its definitions
-           substituting the formal parameters of the predicate with the corresponding
-           logical expressions in the argument list *)
-        let params, _ = List.split pred.pred_params in
-        let subst = SVal.SSubst.init (List.combine params args) in
-        Logging.tmi (fun fmt ->
-            fmt "PREDICATE %s has %d definitions" pred.pred_name
-              (List.length pred.pred_definitions));
-        let new_asrts =
-          List.map
-            (fun (_, a) ->
-              L.tmi (fun fmt -> fmt "Before Auto Unfolding: %a" Asrt.pp a);
-              let facts =
-                List.map (fun fact -> Asrt.Pure fact) pred.pred_facts
-              in
-              let a = Asrt.star (a :: facts) in
-              let result = SVal.SSubst.substitute_asrt subst ~partial:false a in
-              L.tmi (fun fmt -> fmt "After Auto Unfolding: %a" Asrt.pp result);
-              result)
-            pred.pred_definitions
-        in
-
-        (* FIXME:
-           If we processed the predicate definitions in order the recursive call to auto unfold
-           would be avoided *)
-        let result = List.concat (List.map au_no_rec new_asrts) in
-        let result = List.filter Simplifications.admissible_assertion result in
-        result
-      with Not_found ->
-        raise (Failure ("Error: Can't auto_unfold predicate " ^ name)))
-  | _ -> [ asrt ]
+  let options =
+    asrt
+    |> List.map (fun asrt ->
+           match asrt with
+           (* We don't unfold:
+               - Recursive predicates (except in some very specific cases)
+               - predicates marked with no-unfold
+               - predicates with a guard *)
+           | Asrt.Pred (name, _)
+             when (Hashtbl.find rec_tbl name && not unfold_rec_predicates)
+                  ||
+                  let pred = Hashtbl.find predicates name in
+                  pred.pred_nounfold || Option.is_some pred.pred_guard ->
+               [ [ asrt ] ]
+           | Pred (name, args) when Hashtbl.mem unfolded_preds name ->
+               L.verbose (fun fmt ->
+                   fmt "Unfolding predicate: %s with nounfold %b" name
+                     (Hashtbl.find predicates name).pred_nounfold);
+               let pred = Hashtbl.find unfolded_preds name in
+               let params, _ = List.split pred.pred_params in
+               let combined =
+                 try List.combine params args
+                 with Invalid_argument _ ->
+                   Fmt.failwith
+                     "Impossible to auto unfold predicate %s. Used with %i \
+                      args instead of %i"
+                     name (List.length args) (List.length params)
+               in
+               let subst = SVal.SSubst.init combined in
+               let defs =
+                 List.map (fun (_, def) -> def) pred.pred_definitions
+               in
+               List.map (SVal.SSubst.substitute_asrt subst ~partial:false) defs
+           | Pred (name, args) -> (
+               try
+                 L.tmi (fun fmt ->
+                     fmt "AutoUnfold: %a : %s" Asrt.pp_simple asrt name);
+                 let pred : Pred.t = Hashtbl.find predicates name in
+                 (* If it is not, replace the predicate assertion for the list of its definitions
+                    substituting the formal parameters of the predicate with the corresponding
+                    logical expressions in the argument list *)
+                 let params, _ = List.split pred.pred_params in
+                 let subst = SVal.SSubst.init (List.combine params args) in
+                 Logging.tmi (fun fmt ->
+                     fmt "PREDICATE %s has %d definitions" pred.pred_name
+                       (List.length pred.pred_definitions));
+                 let new_asrts =
+                   List.map
+                     (fun (_, a) ->
+                       L.tmi (fun fmt ->
+                           fmt "Before Auto Unfolding: %a" Asrt.pp a);
+                       let facts =
+                         List.map (fun fact -> Asrt.Pure fact) pred.pred_facts
+                       in
+                       let a = a @ facts in
+                       let result =
+                         SVal.SSubst.substitute_asrt subst ~partial:false a
+                       in
+                       L.tmi (fun fmt ->
+                           fmt "After Auto Unfolding: %a" Asrt.pp result);
+                       result)
+                     pred.pred_definitions
+                 in
+
+                 (* FIXME:
+                    If we processed the predicate definitions in order the recursive call to auto unfold
+                    would be avoided *)
+                 let result = List.concat_map au_no_rec new_asrts in
+                 List.filter Simplifications.admissible_assertion result
+               with Not_found ->
+                 raise (Failure ("Error: Can't auto_unfold predicate " ^ name)))
+           | _ -> [ [ asrt ] ])
+  in
+  (* Now that all assertions have been unfolded to multiple options, do a cross
+      product of all options to get all possible combinations of assertions
+     options: Asrt.t list list, ie list of options to choose from
+  *)
+  let rec cross_product (options : Asrt.t list list) : Asrt.t list =
+    match options with
+    | [] -> []
+    | [ o ] -> o
+    | o :: os ->
+        let rest = cross_product os in
+        List.concat_map (fun a -> List.map (fun b -> a @ b) rest) o
+  in
+  cross_product options
 
 (*
  * Return: Hashtbl from predicate name to boolean
@@ -186,7 +205,7 @@ let find_pure_preds (preds : (string, Pred.t) Hashtbl.t) :
         let pred = Hashtbl.find preds pred_name in
         let is_pure =
           List.for_all
-            (fun (_, asrt) -> Asrt.is_pure_asrt asrt)
+            (fun (_, asrt) -> List.for_all Asrt.is_pure_asrt asrt)
             pred.pred_definitions
         in
 
@@ -253,15 +272,15 @@ let unfold_spec
     (preds : (string, Pred.t) Hashtbl.t)
     (rec_info : (string, bool) Hashtbl.t)
     (spec : Spec.t) : Spec.t =
-  let aux spec_name (sspec : Spec.st) : Spec.st list =
+  let aux (sspec : Spec.st) : Spec.st list =
     let pres : Asrt.t list = auto_unfold preds rec_info sspec.ss_pre in
-    L.verbose (fun fmt -> fmt "Pre admissibility: %s" spec_name);
+    L.verbose (fun fmt -> fmt "Pre admissibility: %s" spec.spec_name);
     let pres = List.filter Simplifications.admissible_assertion pres in
     let posts : Asrt.t list =
       List.concat_map (auto_unfold preds rec_info) sspec.ss_posts
     in
     let posts = List.map Reduction.reduce_assertion posts in
-    L.verbose (fun fmt -> fmt "Post admissibility: %s" spec_name);
+    L.verbose (fun fmt -> fmt "Post admissibility: %s" spec.spec_name);
     L.tmi (fun fmt ->
         fmt "@[<hov 2>Testing admissibility for assertions:@.%a@]"
           (Fmt.list Asrt.pp) posts);
@@ -270,14 +289,12 @@ let unfold_spec
       Fmt.failwith
         "Unfolding: Postcondition of %s seems invalid, it has been reduced to \
          no postcondition"
-        spec_name;
+        spec.spec_name;
     List.map
       (fun pre -> Spec.{ sspec with ss_pre = pre; ss_posts = posts })
       pres
   in
-  let spec_sspecs =
-    List.concat (List.map (aux spec.spec_name) spec.spec_sspecs)
-  in
+  let spec_sspecs = List.concat_map aux spec.spec_sspecs in
   match spec_sspecs with
   | [] -> Fmt.failwith "unfolding in spec at preprocessing led to no spec!"
   | _ ->
@@ -396,6 +413,7 @@ let unfold_proc
     (preds : (string, Pred.t) Hashtbl.t)
     (rec_info : (string, bool) Hashtbl.t)
     (proc : ('a, int) Proc.t) : ('a, int) Proc.t =
+  Logging.normal (fun f -> f "UNFOLD_PROC ! %a" Proc.pp_indexed proc);
   let new_spec = Option.map (unfold_spec preds rec_info) proc.proc_spec in
   let new_body =
     Array.map
@@ -567,8 +585,7 @@ let add_closing_tokens preds =
            pred with
            pred_definitions =
              List.map
-               (fun (x, def) ->
-                 (x, Asrt.Star (def, Pred.close_token_call pred)))
+               (fun (x, def) -> (x, Pred.close_token_call pred :: def))
                pred.pred_definitions;
          })
   |> Seq.iter (fun (pred : Pred.t) -> Hashtbl.replace preds pred.pred_name pred);
diff --git a/GillianCore/engine/Abstraction/MP.ml b/GillianCore/engine/Abstraction/MP.ml
index 646454bb..8b8ee5c0 100644
--- a/GillianCore/engine/Abstraction/MP.ml
+++ b/GillianCore/engine/Abstraction/MP.ml
@@ -12,9 +12,9 @@ let outs_pp =
 (** The [mp_step] type represents a matching plan step,
     consisting of an assertion together with the possible
     learned outs *)
-type step = Asrt.t * outs [@@deriving yojson, eq]
+type step = Asrt.simple * outs [@@deriving yojson, eq]
 
-let pp_step = Fmt.pair ~sep:(Fmt.any ", ") Asrt.pp outs_pp
+let pp_step = Fmt.pair ~sep:(Fmt.any ", ") Asrt.pp_simple_full outs_pp
 let pp_step_list = Fmt.Dump.list pp_step
 
 type label = string * SS.t [@@deriving eq, yojson]
@@ -25,7 +25,7 @@ let pp_label ft (lab, ss) =
 type post = Flag.t * Asrt.t list [@@deriving eq, yojson]
 
 let pp_post ft (flag, asrts) =
-  Fmt.pf ft "%a: %a" Flag.pp flag Asrt.pp (Asrt.star asrts)
+  Fmt.pf ft "%a: %a" Flag.pp flag Fmt.(list ~sep:comma Asrt.pp) asrts
 
 (** At a high level, a matching plan is a tree of assertions.
      *)
@@ -68,11 +68,11 @@ let kb_pp = Fmt.(braces (iter ~sep:comma KB.iter Expr.full_pp))
 type preds_tbl_t = (string, pred) Hashtbl.t
 
 type err =
-  | MPSpec of string * Asrt.t list list
-  | MPPred of string * Asrt.t list list
-  | MPLemma of string * Asrt.t list list
-  | MPAssert of Asrt.t * Asrt.t list list
-  | MPInvariant of Asrt.t * Asrt.t list list
+  | MPSpec of string * Asrt.t list
+  | MPPred of string * Asrt.t list
+  | MPLemma of string * Asrt.t list
+  | MPAssert of Asrt.t * Asrt.t list
+  | MPInvariant of Asrt.t * Asrt.t list
 [@@deriving show]
 
 exception MPError of err
@@ -499,15 +499,15 @@ let ins_outs_formula (kb : KB.t) (pf : Formula.t) : (KB.t * outs) list =
 let ins_outs_assertion
     (pred_ins : (string, int list) Hashtbl.t)
     (kb : KB.t)
-    (asrt : Asrt.t) : (KB.t * outs) list =
+    (asrt : Asrt.simple) : (KB.t * outs) list =
   let get_pred_ins name =
     match Hashtbl.find_opt pred_ins name with
     | None -> raise (Failure ("ins_outs_assertion. Unknown Predicate: " ^ name))
     | Some ins -> ins
   in
-  match (asrt : Asrt.t) with
+  match (asrt : Asrt.simple) with
   | Pure form -> ins_outs_formula kb form
-  | GA (_, lie, loe) -> ins_and_outs_from_lists kb lie loe
+  | CorePred (_, lie, loe) -> ins_and_outs_from_lists kb lie loe
   | Pred (p_name, args) ->
       let p_ins = get_pred_ins p_name in
       let _, lie, loe =
@@ -535,35 +535,24 @@ let ins_outs_assertion
   | _ ->
       raise (Failure "Impossible: non-simple assertion in ins_outs_assertion.")
 
-let collect_simple_asrts a =
-  let rec aux (a : Asrt.t) : Asrt.t Seq.t =
+let simplify_asrts a =
+  let rec aux (a : Asrt.simple) : Asrt.simple list =
     match a with
-    | Pure True | Emp -> Seq.empty
-    | Pure (And (f1, f2)) -> Seq.append (aux (Pure f1)) (aux (Pure f2))
-    | Pure _ | Pred _ | GA _ | Wand _ -> Seq.return a
+    | Pure True | Emp -> []
+    | Pure (And (f1, f2)) -> aux (Pure f1) @ aux (Pure f2)
+    | Pure _ | Pred _ | CorePred _ | Wand _ -> [ a ]
     | Types _ -> (
-        let a = Reduction.reduce_assertion a in
+        let a = Reduction.reduce_assertion [ a ] in
         match a with
-        | Types les -> Seq.map (fun e -> Asrt.Types [ e ]) (List.to_seq les)
-        | _ -> aux a)
-    | Star (a1, a2) -> Seq.append (aux a1) (aux a2)
+        | [ Types les ] -> List.map (fun e -> Asrt.Types [ e ]) les
+        | _ -> List.concat_map aux a)
   in
-  List.of_seq (aux a)
-
-let collect_and_simplify_atoms a =
-  let atoms = collect_simple_asrts a in
-  let atoms =
-    if List.mem (Asrt.Pure False) atoms then [ Asrt.Pure False ] else atoms
-  in
-  let separating, overlapping =
-    List.partition
-      (function
-        | Asrt.Pred _ | Asrt.GA _ | Asrt.Wand _ -> true
-        | _ -> false)
-      atoms
-  in
-  let overlapping = List.sort_uniq Stdlib.compare overlapping in
-  List.sort Asrt.prioritise (separating @ overlapping)
+  let atoms = List.concat_map aux a in
+  if List.mem (Asrt.Pure False) atoms then [ Asrt.Pure False ]
+  else
+    let overlapping, separating = List.partition Asrt.is_pure_asrt atoms in
+    let overlapping = List.sort_uniq Stdlib.compare overlapping in
+    List.sort Asrt.prioritise (separating @ overlapping)
 
 let s_init_atoms ~preds kb atoms =
   let step_of_atom ~kb atom =
@@ -575,7 +564,7 @@ let s_init_atoms ~preds kb atoms =
     L.verbose (fun m ->
         m "KNOWN: @[%a@].@\n@[<v 2>CUR MP:@\n%a@]@\nTO VISIT: @[%a@]" kb_pp kb
           pp_step_list current
-          (Fmt.list ~sep:(Fmt.any "@\n") Asrt.full_pp)
+          (Fmt.list ~sep:(Fmt.any "@\n") Asrt.pp_simple_full)
           rest);
     match rest with
     | [] ->
@@ -595,9 +584,9 @@ let s_init_atoms ~preds kb atoms =
   search [] kb atoms
 
 let s_init ~(preds : (string, int list) Hashtbl.t) (kb : KB.t) (a : Asrt.t) :
-    (step list, Asrt.t list) result =
+    (step list, Asrt.t) result =
   L.verbose (fun m -> m "Entering s-init on: %a\n\nKB: %a\n" Asrt.pp a kb_pp kb);
-  let atoms = collect_and_simplify_atoms a in
+  let atoms = simplify_asrts a in
   s_init_atoms ~preds kb atoms
 
 let of_step_list ?post ?label (steps : step list) : t =
@@ -659,7 +648,7 @@ let init
     (preds : (string, int list) Hashtbl.t)
     (asrts_posts :
       (Asrt.t * ((string * SS.t) option * (Flag.t * Asrt.t list) option)) list)
-    : (t, Asrt.t list list) result =
+    : (t, Asrt.simple list list) result =
   let known_matchables =
     match use_params with
     | None -> known_matchables
@@ -908,32 +897,32 @@ let get_lemma (prog : 'a prog) (name : string) : (lemma, unit) result =
   | Some lemma -> Ok lemma
   | None -> Error ()
 
-let rec pp_asrt
+let pp_asrt
     ?(preds_printer : (Format.formatter -> string * Expr.t list -> unit) option)
     ~(preds : preds_tbl_t)
     (fmt : Format.formatter)
     (a : Asrt.t) =
-  let pp_asrt = pp_asrt ?preds_printer ~preds in
-  match a with
-  | Star (a1, a2) -> Fmt.pf fmt "%a *@ %a" pp_asrt a1 pp_asrt a2
-  | Pred (name, args) -> (
-      match preds_printer with
-      | Some pp_pred -> (Fmt.hbox pp_pred) fmt (name, args)
-      | None -> (
-          try
-            let pred = get_pred_def preds name in
-            let out_params = Pred.out_params pred.pred in
-            let out_args = Pred.out_args pred.pred args in
-            let in_args = Pred.in_args pred.pred args in
-            let out_params_args = List.combine out_params out_args in
-            let pp_out_params_args fmt (x, e) =
-              Fmt.pf fmt "@[<h>%s: %a@]" x Expr.pp e
-            in
-            Fmt.pf fmt "%s(@[<h>%a@])" name
-              (Pred.pp_ins_outs pred.pred Expr.pp pp_out_params_args)
-              (in_args, out_params_args)
-          with _ -> Asrt.pp fmt a))
-  | a -> Asrt.pp fmt a
+  let pp_simple_asrt fmt = function
+    | Asrt.Pred (name, args) -> (
+        match preds_printer with
+        | Some pp_pred -> (Fmt.hbox pp_pred) fmt (name, args)
+        | None -> (
+            try
+              let pred = get_pred_def preds name in
+              let out_params = Pred.out_params pred.pred in
+              let out_args = Pred.out_args pred.pred args in
+              let in_args = Pred.in_args pred.pred args in
+              let out_params_args = List.combine out_params out_args in
+              let pp_out_params_args fmt (x, e) =
+                Fmt.pf fmt "@[<h>%s: %a@]" x Expr.pp e
+              in
+              Fmt.pf fmt "%s(@[<h>%a@])" name
+                (Pred.pp_ins_outs pred.pred Expr.pp pp_out_params_args)
+                (in_args, out_params_args)
+            with _ -> Asrt.pp fmt a))
+    | a -> Asrt.pp_simple fmt a
+  in
+  Fmt.list ~sep:(Fmt.any " *@ ") pp_simple_asrt fmt a
 
 let pp_sspec
     ?(preds_printer : (Format.formatter -> string * Expr.t list -> unit) option)
diff --git a/GillianCore/engine/Abstraction/MP.mli b/GillianCore/engine/Abstraction/MP.mli
index 63a85792..df54af13 100644
--- a/GillianCore/engine/Abstraction/MP.mli
+++ b/GillianCore/engine/Abstraction/MP.mli
@@ -7,7 +7,7 @@ val outs_pp : outs Fmt.t
 (** The [step] type represents a matching plan step,
     consisting of an assertion together with the possible
     learned outs *)
-type step = Asrt.t * outs [@@deriving yojson]
+type step = Asrt.simple * outs [@@deriving yojson]
 
 type label = string * SS.t [@@deriving yojson]
 type post = Flag.t * Asrt.t list [@@deriving yojson]
@@ -40,11 +40,11 @@ type 'annot prog = {
 type preds_tbl_t = (string, pred) Hashtbl.t
 
 type err =
-  | MPSpec of string * Asrt.t list list
-  | MPPred of string * Asrt.t list list
-  | MPLemma of string * Asrt.t list list
-  | MPAssert of Asrt.t * Asrt.t list list
-  | MPInvariant of Asrt.t * Asrt.t list list
+  | MPSpec of string * Asrt.t list
+  | MPPred of string * Asrt.t list
+  | MPLemma of string * Asrt.t list
+  | MPAssert of Asrt.t * Asrt.t list
+  | MPInvariant of Asrt.t * Asrt.t list
 [@@deriving show]
 
 module KB = Expr.Set
@@ -53,13 +53,13 @@ val learn_expr :
   ?top_level:bool -> KB.t -> Gil_syntax.Expr.t -> Gil_syntax.Expr.t -> outs
 
 val ins_outs_expr : KB.t -> Expr.t -> Expr.t -> (KB.t * outs) list
-val collect_simple_asrts : Asrt.t -> Asrt.t list
+val simplify_asrts : Asrt.t -> Asrt.t
 
 val s_init_atoms :
   preds:(string, int list) Hashtbl.t ->
   KB.t ->
-  Asrt.t list ->
-  (step list, Asrt.t list) result
+  Asrt.t ->
+  (step list, Asrt.t) result
 
 val of_step_list : ?post:post -> ?label:label -> step list -> t
 
@@ -69,7 +69,7 @@ val init :
   KB.t ->
   (string, int list) Hashtbl.t ->
   (Asrt.t * ((string * SS.t) option * (Flag.t * Asrt.t list) option)) list ->
-  (t, Asrt.t list list) result
+  (t, Asrt.t list) result
 
 val init_prog :
   ?preds_tbl:(string, pred) Hashtbl.t ->
diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 17d6edec..9a7c678c 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -76,7 +76,9 @@ module type S = sig
 
   type unfold_info_t = (string * string) list
 
-  val produce_assertion : t -> SVal.SESubst.t -> Asrt.t -> (t, err_t) Res_list.t
+  val produce_assertion :
+    t -> SVal.SESubst.t -> Asrt.simple -> (t, err_t) Res_list.t
+
   val produce : t -> SVal.SESubst.t -> Asrt.t -> (t, err_t) Res_list.t
   val produce_posts : t -> SVal.SESubst.t -> Asrt.t list -> t list
 
@@ -568,8 +570,10 @@ module Make (State : SState.S) :
         in
         Some (actual_pred, args)
 
-  let rec produce_assertion (astate : t) (subst : SVal.SESubst.t) (a : Asrt.t) :
-      (t, err_t) Res_list.t =
+  let rec produce_assertion
+      (astate : t)
+      (subst : SVal.SESubst.t)
+      (a : Asrt.simple) : (t, err_t) Res_list.t =
     let open Res_list.Syntax in
     let { state; preds; pred_defs; variants; wands } = astate in
     let other_state_err msg = [ Error (StateErr.EOther msg) ] in
@@ -580,12 +584,15 @@ module Make (State : SState.S) :
            Produce simple assertion: @[<h>%a@]@\n\
            With subst: %a\n\
           \           -------------------------@\n"
-          Asrt.pp a SVal.SESubst.pp subst);
+          Asrt.pp_simple a SVal.SESubst.pp subst);
 
     L.verbose (fun m -> m "STATE: %a" pp_astate astate);
 
-    match a with
-    | GA (a_id, ins, outs) ->
+    match (a : Asrt.simple) with
+    | Emp ->
+        L.verbose (fun fmt -> fmt "Emp assertion.");
+        [ Ok astate ]
+    | CorePred (a_id, ins, outs) ->
         L.verbose (fun fmt -> fmt "Memory producer.");
 
         let vs = List.map (subst_in_expr subst) (ins @ outs) in
@@ -712,12 +719,9 @@ module Make (State : SState.S) :
         | Some state' ->
             Res_list.return
               { state = state'; preds; wands; pred_defs; variants })
-    | _ -> L.fail "Produce simple assertion: unsupported assertion"
 
-  and produce_asrt_list
-      (astate : t)
-      (subst : SVal.SESubst.t)
-      (sas : Asrt.t list) : (t, err_t) Res_list.t =
+  and produce_asrt_list (astate : t) (subst : SVal.SESubst.t) (sas : Asrt.t) :
+      (t, err_t) Res_list.t =
     let open Res_list.Syntax in
     let other_state_err msg = Res_list.error_with (StateErr.EOther msg) in
     let () =
@@ -764,7 +768,7 @@ module Make (State : SState.S) :
           "@[-----------------@\n\
            -----------------@\n\
            Produce assertion: @[%a@]@]" Asrt.pp a);
-    let sas = MP.collect_simple_asrts a in
+    let sas = MP.simplify_asrts a in
     produce_asrt_list astate subst sas
 
   let produce_posts (state : t) (subst : SVal.SESubst.t) (asrts : Asrt.t list) :
@@ -956,26 +960,13 @@ module Make (State : SState.S) :
       | Some (pname, v_args) -> (
           L.verbose (fun m -> m "FOUND STH TO UNFOLD: %s!!!!\n" pname);
           let rets = unfold (copy_astate astate) pname v_args in
-          let only_errors =
-            List.filter_map
-              (function
-                | Error e -> Some e
-                | _ -> None)
-              rets
-          in
+          let only_successes, only_errors = Res_list.split rets in
           match only_errors with
           | [] ->
               L.verbose (fun m ->
                   m "Unfold complete: %s(@[<h>%a@]): %d" pname
                     Fmt.(list ~sep:comma Expr.pp)
                     v_args (List.length rets));
-              let only_successes =
-                List.filter_map
-                  (function
-                    | Ok x -> Some x
-                    | _ -> None)
-                  rets
-              in
               Some only_successes
           | _ :: _ ->
               L.verbose (fun m ->
@@ -1214,7 +1205,7 @@ module Make (State : SState.S) :
           (let a = fst step in
            (* Get pvars, lvars, locs from the assertion *)
            let a_pvars, a_lvars, a_locs =
-             (Asrt.pvars a, Asrt.lvars a, Asrt.locs a)
+             (Asrt.pvars [ a ], Asrt.lvars [ a ], Asrt.locs [ a ])
            in
            let filter_vars = SS.union a_pvars (SS.union a_lvars a_locs) in
 
@@ -1269,12 +1260,12 @@ module Make (State : SState.S) :
       L.Logging_constants.Content_type.assertion (fun () ->
         let p, outs = step in
         let open Res_list.Syntax in
-        match (p : Asrt.t) with
-        | GA (a_id, e_ins, e_outs) -> (
+        match (p : Asrt.simple) with
+        | CorePred (a_id, e_ins, e_outs) -> (
             let vs_ins = List.map (subst_in_expr_opt astate subst) e_ins in
             let failure = List.exists (fun x -> x = None) vs_ins in
             if failure then (
-              Fmt.pr "I don't know all ins for %a????" Asrt.pp p;
+              Fmt.pr "I don't know all ins for %a????" Asrt.pp_simple p;
               if !Config.under_approximation then [] else resource_fail)
             else
               let vs_ins = List.map Option.get vs_ins in
@@ -1437,7 +1428,7 @@ module Make (State : SState.S) :
                     StateErr.EAsrt (les, Not conjunct, [ [ Pure conjunct ] ])
                   in
                   Res_list.error_with error)
-        (* LTrue, LFalse, LEmp, LStar *)
+        (* LTrue, LFalse, LEmp *)
         | _ -> raise (Failure "Illegal Assertion in Matching Plan"))
 
   and match_assertion_safely ?(no_auto_fold = false) state subst step =
@@ -1463,7 +1454,7 @@ module Make (State : SState.S) :
             let other_error =
               StateErr.EOther
                 (Fmt.str "Uncaught exception while matching assertions %a"
-                   Asrt.pp (fst step))
+                   Asrt.pp_simple (fst step))
             in
             Res_list.error_with other_error)
 
@@ -1862,14 +1853,13 @@ module Make (State : SState.S) :
 
     let get_defs (pred : Pred.t) largs =
       if pred.pred_abstract || Option.is_some pred.pred_guard then
-        [ Asrt.Pred (pred.pred_name, largs) ]
+        [ [ Asrt.Pred (pred.pred_name, largs) ] ]
       else
         let unfolded_pred =
           Hashtbl.find_opt LogicPreprocessing.unfolded_preds pred.pred_name
         in
-        match unfolded_pred with
-        | Some pred -> List.map snd pred.pred_definitions
-        | None -> List.map snd pred.pred_definitions
+        let pred = Option.value ~default:pred unfolded_pred in
+        List.map snd pred.pred_definitions
 
     let make_lhs_states ~pred_defs ~empty_state (lname, largs) =
       let open Syntaxes.List in
@@ -1970,7 +1960,7 @@ module Make (State : SState.S) :
               init_subst;
               fold_outs_info = (subst, step, out_params, out_args);
             }
-      | (GA (core_pred, ins, outs), _), [ err ] ->
+      | (CorePred (core_pred, ins, outs), _), [ err ] ->
           (* What we do here is simulate the idea that the core predicate is actually a folded core-predicate *)
           let kb =
             List.to_seq ins
@@ -2017,7 +2007,7 @@ module Make (State : SState.S) :
                   List.init out_amount (fun o_i ->
                       all_new_outs.((cp_i * out_amount) + o_i))
                 in
-                Asrt.GA (core_pred, ins, outs))
+                Asrt.CorePred (core_pred, ins, outs))
               new_ins_l
           in
           let learning_equalities =
@@ -2091,11 +2081,12 @@ module Make (State : SState.S) :
               ])
         (Ok state) obtained expected
 
-    let rec package_case_step { lhs_state; current_state; subst } step :
-        (package_state list, err_t list) Result.t =
+    let rec package_case_step
+        { lhs_state; current_state; subst }
+        (step : MP.step) : (package_state list, err_t list) Result.t =
       let open Syntaxes.Result in
       L.verbose (fun m ->
-          m "Wand about to consume RHS step: %a" Asrt.pp (fst step));
+          m "Wand about to consume RHS step: %a" Asrt.pp_simple (fst step));
       (* States are modified in place unfortunately.. so we have to copy them just in case *)
       (* First we try to consume from the lhs_state *)
       let- lhs_errs =
diff --git a/GillianCore/engine/Abstraction/Matcher.mli b/GillianCore/engine/Abstraction/Matcher.mli
index c9f3e8bb..d82ae684 100644
--- a/GillianCore/engine/Abstraction/Matcher.mli
+++ b/GillianCore/engine/Abstraction/Matcher.mli
@@ -76,11 +76,13 @@ module type S = sig
 
   type unfold_info_t = (string * string) list
 
-  val produce_assertion : t -> SVal.SESubst.t -> Asrt.t -> (t, err_t) Res_list.t
+  val produce_assertion :
+    t -> SVal.SESubst.t -> Asrt.simple -> (t, err_t) Res_list.t
+
   val produce : t -> SVal.SESubst.t -> Asrt.t -> (t, err_t) Res_list.t
   val produce_posts : t -> SVal.SESubst.t -> Asrt.t list -> t list
 
-  (** [unfold state name args unfold_info] returns a 
+  (** [unfold state name args unfold_info] returns a
       list of pairs (subst, state), resulting from unfolding
       the predicate [name(..args..)] from the given state.
       unfold_info contains information about how to bind new variables. *)
diff --git a/GillianCore/engine/Abstraction/Normaliser.ml b/GillianCore/engine/Abstraction/Normaliser.ml
index 67686cc2..46a64d99 100644
--- a/GillianCore/engine/Abstraction/Normaliser.ml
+++ b/GillianCore/engine/Abstraction/Normaliser.ml
@@ -20,7 +20,7 @@ module Make (SPState : PState.S) = struct
     (* 1 - Find the lists for which we know the length *)
     let find_list_exprs_to_concretize (a : Asrt.t) :
         (Expr.t, Expr.t list) Hashtbl.t =
-      let rec collect_concretizable_lists = function
+      let collect_concretizable_lists = function
         | Asrt.Pure (Eq (EList _, EList _)) -> []
         | Pure (Eq (le, EList les)) | Pure (Eq (EList les, le)) -> [ (le, les) ]
         | Pure (Eq (UnOp (LstLen, le), Lit (Int i)))
@@ -29,13 +29,9 @@ module Make (SPState : PState.S) = struct
               List.init (Z.to_int i) (fun _ -> Expr.LVar (LVar.alloc ()))
             in
             [ (le, les) ]
-        | Star (a1, a2) ->
-            List.rev_append
-              (collect_concretizable_lists a1)
-              (collect_concretizable_lists a2)
         | _ -> []
       in
-      let lst_exprs = collect_concretizable_lists a in
+      let lst_exprs = List.concat_map collect_concretizable_lists a in
       let lists_tbl = Hashtbl.create 1 in
       List.iter
         (fun (le, les) ->
@@ -77,12 +73,9 @@ module Make (SPState : PState.S) = struct
     let make_new_list_as
         (a : Asrt.t)
         (new_lists : (Expr.t, Expr.t list) Hashtbl.t) : Asrt.t =
-      let new_list_as =
-        Hashtbl.fold
-          (fun le les (ac : Asrt.t list) -> Pure (Eq (le, EList les)) :: ac)
-          new_lists [ a ]
-      in
-      Asrt.star new_list_as
+      Hashtbl.fold
+        (fun le les (ac : Asrt.t) -> Pure (Eq (le, EList les)) :: ac)
+        new_lists a
     in
 
     (* Doing IT *)
@@ -561,29 +554,25 @@ module Make (SPState : PState.S) = struct
     result
 
   (** Separate an assertion into:  core_asrts, pure, typing and predicates *)
-  let rec separate_assertion (a : Asrt.t) :
+  let separate_assertion (a : Asrt.t) :
       (string * Expr.t list * Expr.t list) list
       * Formula.t list
       * (Expr.t * Type.t) list
       * (string * Expr.t list) list
       * Wands.wand list =
-    let f = separate_assertion in
-
-    match a with
-    | Star (al, ar) ->
-        let core_asrts_l, pure_l, types_l, preds_l, wands_l = f al in
-        let core_asrts_r, pure_r, types_r, preds_r, wands_r = f ar in
-        ( core_asrts_l @ core_asrts_r,
-          pure_l @ pure_r,
-          types_l @ types_r,
-          preds_l @ preds_r,
-          wands_l @ wands_r )
-    | GA (a, es1, es2) -> ([ (a, es1, es2) ], [], [], [], [])
-    | Wand { lhs; rhs } -> ([], [], [], [], [ { lhs; rhs } ])
-    | Emp -> ([], [], [], [], [])
-    | Types lst -> ([], [], lst, [], [])
-    | Pred (name, params) -> ([], [], [], [ (name, params) ], [])
-    | Pure f -> ([], [ f ], [], [], [])
+    List.fold_left
+      (fun (core_asrts, pure, types, preds, wands) (a : Asrt.simple) ->
+        match a with
+        | CorePred (a, es1, es2) ->
+            ((a, es1, es2) :: core_asrts, pure, types, preds, wands)
+        | Wand { lhs; rhs } ->
+            (core_asrts, pure, types, preds, Wands.{ lhs; rhs } :: wands)
+        | Emp -> (core_asrts, pure, types, preds, wands)
+        | Types lst -> (core_asrts, pure, lst @ types, preds, wands)
+        | Pred (name, params) ->
+            (core_asrts, pure, types, (name, params) :: preds, wands)
+        | Pure f -> (core_asrts, f :: pure, types, preds, wands))
+      ([], [], [], [], []) a
 
   (** Normalise type assertions (Intialise type environment *)
   let normalise_types
@@ -844,7 +833,7 @@ module Make (SPState : PState.S) = struct
          (fun current_states (a, ins, outs) ->
            let open Syntaxes.List in
            let* current_state = current_states in
-           SPState.produce current_state subst (Asrt.GA (a, ins, outs))
+           SPState.produce current_state subst [ Asrt.CorePred (a, ins, outs) ]
            |> (* If some production fails, we ignore *)
            List.filter_map (function
              | Ok x -> Some x
@@ -852,8 +841,9 @@ module Make (SPState : PState.S) = struct
                  L.verbose (fun m ->
                      m
                        "One branch of produce GA failed for: %a!\n\
-                        with Message: %a. Might have lost some paths ?" Asrt.pp
-                       (Asrt.GA (a, ins, outs))
+                        with Message: %a. Might have lost some paths ?"
+                       Asrt.pp_simple
+                       (Asrt.CorePred (a, ins, outs))
                        SPState.pp_err msg);
                  None))
          [ astate ]
@@ -883,12 +873,8 @@ module Make (SPState : PState.S) = struct
     let a = Reduction.reduce_assertion a in
     let subst = SESubst.init [] in
 
-    let rec find_spec_var_eqs (a : Asrt.t) =
-      let f = find_spec_var_eqs in
+    let find_spec_var_eqs (a : Asrt.simple) =
       match a with
-      | Star (al, ar) ->
-          f al;
-          f ar
       | Pure (Eq (LVar x, LVar y))
         when is_spec_var_name x && not (is_spec_var_name y) ->
           SESubst.put subst (LVar y) (LVar x)
@@ -897,7 +883,7 @@ module Make (SPState : PState.S) = struct
           SESubst.put subst (LVar x) (LVar y)
       | _ -> ()
     in
-    find_spec_var_eqs a;
+    List.iter find_spec_var_eqs a;
     SESubst.substitute_asrt subst ~partial:true a
 
   (** Given an assertion creates a symbolic state and a substitution *)
diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml
index 200377d4..ac0a1ce3 100644
--- a/GillianCore/engine/Abstraction/PState.ml
+++ b/GillianCore/engine/Abstraction/PState.ml
@@ -262,7 +262,7 @@ module Make (State : SState.S) :
     |> SS.union (Preds.get_lvars preds)
     |> SS.union (Wands.get_lvars wands)
 
-  let to_assertions ?(to_keep : SS.t option) (astate : t) : Asrt.t list =
+  let to_assertions ?(to_keep : SS.t option) (astate : t) : Asrt.t =
     let { state; preds; wands; _ } = astate in
     let s_asrts = State.to_assertions ?to_keep state in
     let p_asrts = Preds.to_assertions preds in
@@ -410,7 +410,7 @@ module Make (State : SState.S) :
       preds_list;
     { state; preds; wands = Wands.init []; pred_defs; variants }
 
-  let consume ~(prog : 'a MP.prog) astate a binders =
+  let consume ~(prog : 'a MP.prog) astate (a : Asrt.t) binders =
     if not (List.for_all Names.is_lvar_name binders) then
       failwith "Binding of pure variables in *-assert.";
     let store = State.get_store astate.state in
@@ -505,9 +505,8 @@ module Make (State : SState.S) :
         let new_bindings =
           List.map (fun (e, e_v) -> Asrt.Pure (Eq (e, e_v))) new_bindings
         in
-        let a_new_bindings = Asrt.star new_bindings in
         let full_subst = make_id_subst a in
-        let a_produce = a_new_bindings in
+        let a_produce = new_bindings in
         let open Res_list.Syntax in
         let result =
           let** new_astate = SMatcher.produce new_state full_subst a_produce in
@@ -723,8 +722,7 @@ module Make (State : SState.S) :
                | _ -> true)
         |> List.map (fun (e, e_v) -> Asrt.Pure (Eq (e, e_v)))
       in
-      let a_bindings = Asrt.star bindings in
-      let subst_bindings = make_id_subst a_bindings in
+      let subst_bindings = make_id_subst bindings in
       let pvar_subst_list_known =
         List.map
           (fun x ->
@@ -748,9 +746,7 @@ module Make (State : SState.S) :
           (SVal.SESubst.substitute_asrt subst_bindings ~partial:true a)
       in
       L.verbose (fun fmt -> fmt "Invariant v2: %a" Asrt.pp a_substed);
-      let a_produce =
-        Reduction.reduce_assertion (Asrt.star [ a_bindings; a_substed ])
-      in
+      let a_produce = Reduction.reduce_assertion (bindings @ a_substed) in
       L.verbose (fun fmt -> fmt "Invariant v3: %a" Asrt.pp a_produce);
       (* Create empty state *)
       let invariant_state : t = clear_resource new_state in
@@ -803,7 +799,7 @@ module Make (State : SState.S) :
       (fun astates (id, frame) ->
         let** astate = astates in
         let** astate =
-          let frame_asrt = Asrt.star (to_assertions frame) in
+          let frame_asrt = to_assertions frame in
           let full_subst = make_id_subst frame_asrt in
           let+ produced = SMatcher.produce astate full_subst frame_asrt in
           match produced with
@@ -1013,14 +1009,14 @@ module Make (State : SState.S) :
               let new_bindings =
                 List.map (fun (e, e_v) -> Asrt.Pure (Eq (e, e_v))) new_bindings
               in
-              let a_new_bindings = Asrt.star new_bindings in
+              let a_new_bindings = new_bindings in
               let subst_bindings = make_id_subst a_new_bindings in
               let full_subst = make_id_subst a in
               let _ = SVal.SESubst.merge_left full_subst subst_bindings in
               let a_substed =
                 SVal.SESubst.substitute_asrt subst_bindings ~partial:true a
               in
-              let a_produce = Asrt.star [ a_new_bindings; a_substed ] in
+              let a_produce = a_new_bindings @ a_substed in
               let result =
                 let** new_astate =
                   SMatcher.produce new_state full_subst a_produce
diff --git a/GillianCore/engine/Abstraction/Preds.ml b/GillianCore/engine/Abstraction/Preds.ml
index 5b950f88..46d6d950 100644
--- a/GillianCore/engine/Abstraction/Preds.ml
+++ b/GillianCore/engine/Abstraction/Preds.ml
@@ -223,7 +223,7 @@ let substitution_in_place (subst : st) (preds : t) : unit =
   let pred_substitution subst (s, vs) = (s, List.map (subst_in_val subst) vs) in
   preds := List.map (pred_substitution subst) !preds
 
-let to_assertions (preds : t) : Asrt.t list =
+let to_assertions (preds : t) : Asrt.simple list =
   let preds = to_list preds in
   let pred_to_assert (n, args) = Asrt.Pred (n, args) in
   List.sort Asrt.compare (List.map pred_to_assert preds)
diff --git a/GillianCore/engine/Abstraction/Preds.mli b/GillianCore/engine/Abstraction/Preds.mli
index 89c35fde..ad1e0011 100644
--- a/GillianCore/engine/Abstraction/Preds.mli
+++ b/GillianCore/engine/Abstraction/Preds.mli
@@ -40,4 +40,4 @@ val get_all : maintain:bool -> (abs_t -> bool) -> t -> abs_t list
 val substitution_in_place : SVal.SESubst.t -> t -> unit
 
 (** Turns a predicate set into a list of assertions *)
-val to_assertions : t -> Asrt.t list
+val to_assertions : t -> Asrt.t
diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml
index 0f2a1114..cb8cb7a8 100644
--- a/GillianCore/engine/Abstraction/Verifier.ml
+++ b/GillianCore/engine/Abstraction/Verifier.ml
@@ -189,7 +189,7 @@ struct
           posts
       in
       if not to_verify then
-        let pre' = Asrt.star (SPState.to_assertions ss_pre) in
+        let pre' = SPState.to_assertions ss_pre in
         (None, Some (pre', posts))
       else
         (* Step 4 - create a matching plan for the postconditions and s_test *)
@@ -229,7 +229,7 @@ struct
             L.verbose (fun m -> m "%s" msg);
             (None, None)
         | Ok post_mp ->
-            let pre' = Asrt.star (SPState.to_assertions ss_pre) in
+            let pre' = SPState.to_assertions ss_pre in
             let ss_pre =
               match flag with
               (* Lemmas should not have stores when being proven *)
diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml
index 28a153ce..75add5ab 100644
--- a/GillianCore/engine/BiAbduction/Abductor.ml
+++ b/GillianCore/engine/BiAbduction/Abductor.ml
@@ -90,13 +90,12 @@ module Make
           SPState.simplify ~kill_new_lvars:true state_f
         in
         let+ final_simplified = finals_simplified in
-        Asrt.star
-          (List.sort Asrt.compare
-             (SPState.to_assertions ~to_keep:pvars final_simplified))
+        List.sort Asrt.compare
+          (SPState.to_assertions ~to_keep:pvars final_simplified)
       in
 
       let+ pre =
-        let af_asrt = Asrt.star (SPState.to_assertions state_af) in
+        let af_asrt = SPState.to_assertions state_af in
         let af_subst = make_id_subst af_asrt in
         let* af_produce_res = SPState.produce state_i af_subst af_asrt in
         match af_produce_res with
@@ -105,9 +104,8 @@ module Make
               SPState.simplify ~kill_new_lvars:true state_i'
             in
             let+ simplified = simplifieds in
-            Asrt.star
-              (List.sort Asrt.compare
-                 (SPState.to_assertions ~to_keep:pvars simplified))
+            List.sort Asrt.compare
+              (SPState.to_assertions ~to_keep:pvars simplified)
         | Error _ ->
             L.verbose (fun m -> m "Failed to produce anti-frame");
             []
diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml
index 056bb9cd..3f68e243 100644
--- a/GillianCore/engine/BiAbduction/BiState.ml
+++ b/GillianCore/engine/BiAbduction/BiState.ml
@@ -149,7 +149,7 @@ module Make (State : SState.S) = struct
   let get_spec_vars ({ state; _ } : t) : Var.Set.t = State.get_spec_vars state
   let get_lvars ({ state; _ } : t) : Var.Set.t = State.get_lvars state
 
-  let to_assertions ?(to_keep : SS.t option) ({ state; _ } : t) : Asrt.t list =
+  let to_assertions ?(to_keep : SS.t option) ({ state; _ } : t) : Asrt.t =
     State.to_assertions ?to_keep state
 
   let evaluate_slcmd (prog : 'a MP.prog) (lcmd : SLCmd.t) (bi_state : t) :
@@ -193,12 +193,12 @@ module Make (State : SState.S) = struct
     in
     SVal.SESubst.init bindings
 
-  let fix_list_apply s =
+  let fix_list_apply (s : state_t) (asrt : Asrt.t) =
     let open Syntaxes.List in
     List.fold_left
       (fun acc a ->
         let* this_state = acc in
-        let lvars = Asrt.lvars a in
+        let lvars = Asrt.lvars [ a ] in
         let this_state = State.add_spec_vars this_state lvars in
         match a with
         | Asrt.Emp -> [ this_state ]
@@ -213,12 +213,11 @@ module Make (State : SState.S) = struct
                    | Some s -> State.assume_t s e t)
                  (Some this_state)
             |> Option.to_list
-        | GA (corepred, ins, outs) ->
+        | CorePred (corepred, ins, outs) ->
             State.produce_core_pred corepred this_state (ins @ outs)
-        | Star _ -> raise (Failure "DEATH. fix_list_apply star")
         | Wand _ -> raise (Failure "DEATH. fix_list_apply wand")
         | Pred _ -> raise (Failure "DEATH. fix_list_apply pred"))
-      [ s ]
+      [ s ] asrt
 
   type post_res = (Flag.t * Asrt.t list) option
 
@@ -258,7 +257,8 @@ module Make (State : SState.S) = struct
                     "@[<v 2>WARNING: Match Assertion Failed: %a with error: \
                      %a. CUR SUBST:@\n\
                      %a@]@\n"
-                    Asrt.pp (fst step) State.pp_err err SVal.SESubst.pp subst);
+                    Asrt.pp_simple (fst step) State.pp_err err SVal.SESubst.pp
+                    subst);
               if not (State.can_fix err) then (
                 L.verbose (fun m -> m "CANNOT FIX!");
                 [])
@@ -448,7 +448,7 @@ module Make (State : SState.S) = struct
 
   (* to throw errors: *)
 
-  let get_fixes (_ : err_t) : Asrt.t list list =
+  let get_fixes (_ : err_t) : Asrt.t list =
     raise (Failure "get_fixes not implemented in MakeBiState")
 
   let get_recovery_tactic (_ : t) (_ : err_t list) =
diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 31a205c0..3f37bb8a 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2159,7 +2159,7 @@ and simplify_int_arithmetic_lexpr
   | _ -> le
 
 (** Checks if an int expression is greater than zero.
-      
+
     @returns [Some true] if definitely > 0, [Some false] if definitely < 0,
       and [None] if both outcomes are satisfiable. *)
 and check_ge_zero_int ?(top_level = false) (pfs : PFS.t) (e : Expr.t) :
@@ -3172,59 +3172,53 @@ end
 module ETSet = Set.Make (MyET)
 
 let reduce_types (a : Asrt.t) : Asrt.t =
-  let rec separate (a : Asrt.t) =
-    match a with
-    | Pure True -> ([], [])
-    | Pure False -> raise PFSFalse
-    | Pure (Eq (UnOp (TypeOf, e), Lit (Type t)))
-    | Pure (Eq (Lit (Type t), UnOp (TypeOf, e))) -> ([], [ (e, t) ])
-    | Star (a1, a2) ->
-        let fa1, ft1 = separate a1 in
-        let fa2, ft2 = separate a2 in
-        (fa1 @ fa2, ft1 @ ft2)
-    | Types ets -> ([], ets)
-    | _ -> ([ a ], [])
-  in
-
   try
-    let others, ets = separate a in
+    let others, ets =
+      List.fold_left
+        (fun (others, ets) -> function
+          | Asrt.Pure True -> (others, ets)
+          | Asrt.Pure False -> raise PFSFalse
+          | Asrt.Pure (Eq (UnOp (TypeOf, e), Lit (Type t)))
+          | Asrt.Pure (Eq (Lit (Type t), UnOp (TypeOf, e))) ->
+              (others, (e, t) :: ets)
+          | Asrt.Types ets' -> (others, ets' @ ets)
+          | a -> (a :: others, ets))
+        ([], []) a
+    in
 
     let ets = ETSet.elements (ETSet.of_list ets) in
     match (others, ets) with
-    | [], [] -> Pure True
-    | [], ets -> Types ets
-    | a, ets ->
-        let result = Asrt.star a in
-        if ets = [] then result else Star (Types ets, result)
-  with PFSFalse -> Pure False
+    | [], [] -> [ Asrt.Pure True ] (* Could this be []? *)
+    | [], ets -> [ Asrt.Types ets ]
+    | others, [] -> others
+    | others, ets -> Asrt.Types ets :: others
+  with PFSFalse -> [ Asrt.Pure False ]
 
 (* Reduction of assertions *)
-let rec reduce_assertion_loop
+let reduce_assertion_loop
     (matching : bool)
     (pfs : PFS.t)
     (gamma : Type_env.t)
     (a : Asrt.t) : Asrt.t =
-  let f = reduce_assertion_loop matching pfs gamma in
   let fe = reduce_lexpr_loop ~matching pfs gamma in
-  let result =
-    match a with
+  let f : Asrt.simple -> Asrt.t = function
     (* Empty heap *)
-    | Emp -> Asrt.Emp
+    | Asrt.Emp -> []
     (* Star *)
-    | Star (a1, a2) -> (
-        match (f a1, f a2) with
-        | Emp, a | a, Emp -> a
-        | Pure False, _ | _, Pure False -> Asrt.Pure False
-        | Pure True, a | a, Pure True -> a
-        | fa1, fa2 -> Star (fa1, fa2))
     | Wand { lhs = lname, largs; rhs = rname, rargs } ->
-        Wand
-          { lhs = (lname, List.map fe largs); rhs = (rname, List.map fe rargs) }
+        [
+          Wand
+            {
+              lhs = (lname, List.map fe largs);
+              rhs = (rname, List.map fe rargs);
+            };
+        ]
     (* Predicates *)
-    | Pred (name, les) -> Pred (name, List.map fe les)
+    | Pred (name, les) -> [ Pred (name, List.map fe les) ]
     (* Pure assertions *)
-    | Pure True -> Emp
-    | Pure f -> Pure (reduce_formula_loop ~top_level:true matching pfs gamma f)
+    | Pure True -> []
+    | Pure f ->
+        [ Pure (reduce_formula_loop ~top_level:true matching pfs gamma f) ]
     (* Types *)
     | Types lvt -> (
         try
@@ -3232,29 +3226,32 @@ let rec reduce_assertion_loop
             List.fold_right
               (fun (e, t) ac ->
                 match (e : Expr.t) with
-                | Lit lit ->
-                    if t <> Literal.type_of lit then raise WrongType else ac
+                | Lit lit when t <> Literal.type_of lit -> raise WrongType
+                | Lit _ -> ac
                 | _ -> (e, t) :: ac)
               lvt []
           in
-          if lvt = [] then Emp else Types lvt
-        with WrongType -> Pure False)
+          if lvt = [] then [] else [ Types lvt ]
+        with WrongType -> [ Pure False ])
     (* General action *)
-    | GA (act, l_ins, l_outs) -> GA (act, List.map fe l_ins, List.map fe l_outs)
+    | CorePred (act, l_ins, l_outs) ->
+        [ CorePred (act, List.map fe l_ins, List.map fe l_outs) ]
+  in
+  let result = List.concat_map f a in
+  let result =
+    if List.mem (Asrt.Pure False) result then [ Asrt.Pure False ] else result
   in
 
-  if a <> result && not (a == result) then (
-    L.(tmi (fun m -> m "Reduce_assertion: %a -> %a" Asrt.pp a Asrt.pp result));
-    f result)
-  else result
+  (if a <> result && not (a == result) then
+     L.(tmi (fun m -> m "Reduce_assertion: %a -> %a" Asrt.pp a Asrt.pp result)));
+  result
 
-let rec extract_lvar_equalities (a : Asrt.t) =
-  match a with
-  | Pure (Eq (LVar x, v) | Eq (v, LVar x)) ->
-      if Names.is_lvar_name x && not (Names.is_spec_var_name x) then [ (x, v) ]
-      else []
-  | Star (a1, a2) -> extract_lvar_equalities a1 @ extract_lvar_equalities a2
-  | _ -> []
+let extract_lvar_equalities : Asrt.t -> (string * Expr.t) list =
+  List.filter_map @@ function
+  | Asrt.Pure (Eq (LVar x, v) | Eq (v, LVar x)) ->
+      if Names.is_lvar_name x && not (Names.is_spec_var_name x) then Some (x, v)
+      else None
+  | _ -> None
 
 let reduce_assertion
     ?(matching = false)
diff --git a/GillianCore/engine/FOLogic/Simplifications.ml b/GillianCore/engine/FOLogic/Simplifications.ml
index 3603cfec..02bf2d3b 100644
--- a/GillianCore/engine/FOLogic/Simplifications.ml
+++ b/GillianCore/engine/FOLogic/Simplifications.ml
@@ -997,11 +997,7 @@ let admissible_assertion (a : Asrt.t) : bool =
 
   let a = Asrt.pvars_to_lvars a in
 
-  let rec separate (a : Asrt.t) =
-    match a with
-    | Star (a1, a2) ->
-        separate a1;
-        separate a2
+  let separate : Asrt.simple -> unit = function
     | Pure f -> PFS.extend pfs f
     | Types ets ->
         List.iter
@@ -1013,11 +1009,10 @@ let admissible_assertion (a : Asrt.t) : bool =
     | _ -> ()
   in
   try
-    separate a;
+    List.iter separate a;
     let _ = simplify_pfs_and_gamma ~kill_new_lvars:true pfs gamma in
     let res = not (PFS.mem pfs Formula.False) in
-    if res then L.tmi (fun m -> m "Admissible !!")
-    else L.tmi (fun m -> m "Not admissible !!");
+    L.tmi (fun m -> m "Admissible? %b" res);
     res
   with e ->
     L.tmi (fun m ->
diff --git a/GillianCore/engine/concrete_semantics/CState.ml b/GillianCore/engine/concrete_semantics/CState.ml
index 71bb9c00..03a60e7b 100644
--- a/GillianCore/engine/concrete_semantics/CState.ml
+++ b/GillianCore/engine/concrete_semantics/CState.ml
@@ -141,7 +141,7 @@ end = struct
   let get_lvars _ =
     raise (Failure "ERROR: get_lvars called for concrete executions")
 
-  let to_assertions ?to_keep:_ (_ : t) : Asrt.t list =
+  let to_assertions ?to_keep:_ (_ : t) : Asrt.t =
     raise (Failure "ERROR: to_assertions called for concrete executions")
 
   let run_spec
@@ -209,7 +209,7 @@ end = struct
   let can_fix (_ : err_t) : bool = false
   let get_failing_constraint (_ : err_t) : Formula.t = True
 
-  let get_fixes (_ : err_t) : Asrt.t list list =
+  let get_fixes (_ : err_t) : Asrt.t list =
     raise (Failure "Concrete: get_fixes not implemented in CState.Make")
 
   let get_equal_values _ vs = vs
diff --git a/GillianCore/engine/general_semantics/state.ml b/GillianCore/engine/general_semantics/state.ml
index c677d0e4..37ec1701 100644
--- a/GillianCore/engine/general_semantics/state.ml
+++ b/GillianCore/engine/general_semantics/state.ml
@@ -107,7 +107,7 @@ module type S = sig
   val get_lvars : t -> Var.Set.t
 
   (** Turns a state into a list of assertions *)
-  val to_assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
+  val to_assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t
 
   val evaluate_slcmd : 'a MP.prog -> SLCmd.t -> t -> (t, err_t) Res_list.t
 
@@ -144,7 +144,7 @@ module type S = sig
   val mem_constraints : t -> Formula.t list
   val can_fix : err_t -> bool
   val get_failing_constraint : err_t -> Formula.t
-  val get_fixes : err_t -> Asrt.t list list
+  val get_fixes : err_t -> Asrt.t list
   val get_equal_values : t -> vt list -> vt list
   val get_heap : t -> heap_t
 end
diff --git a/GillianCore/engine/general_semantics/stateErr.ml b/GillianCore/engine/general_semantics/stateErr.ml
index 88375c25..732f26d2 100644
--- a/GillianCore/engine/general_semantics/stateErr.ml
+++ b/GillianCore/engine/general_semantics/stateErr.ml
@@ -7,7 +7,7 @@ type ('mem_err, 'value) t =
       (** Incorrect type, depends on value *)
   | EPure of Formula.t (* Missing formula that should be true *)
   | EVar of Var.t (* Undefined variable *)
-  | EAsrt of ('value list * Formula.t * Asrt.t list list)
+  | EAsrt of ('value list * Formula.t * Asrt.t list)
   | EOther of string
     (* We want all errors to be proper errors - this is a temporary placeholder *)
 [@@deriving yojson, show]
@@ -39,9 +39,7 @@ let pp_err
   | EPure f -> Fmt.pf fmt "EPure(%a)" Formula.pp f
   | EVar x -> Fmt.pf fmt "EVar(%s)" x
   | EAsrt (vs, f, asrtss) ->
-      let pp_asrts fmt asrts =
-        Fmt.pf fmt "[%a]" (Fmt.list ~sep:(Fmt.any ", ") Asrt.pp) asrts
-      in
+      let pp_asrts fmt asrts = Fmt.pf fmt "[%a]" Asrt.pp asrts in
       Fmt.pf fmt "EAsrt(%a; %a; %a)"
         (Fmt.list ~sep:(Fmt.any ", ") pp_v)
         vs Formula.pp f
diff --git a/GillianCore/engine/general_semantics/subst.ml b/GillianCore/engine/general_semantics/subst.ml
index d03a84ea..2648715a 100644
--- a/GillianCore/engine/general_semantics/subst.ml
+++ b/GillianCore/engine/general_semantics/subst.ml
@@ -345,8 +345,8 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
 
   let is_empty (subst : t) : bool = Hashtbl.length subst = 0
 
-  let substitute_formula (subst : t) ~(partial : bool) (a : Formula.t) :
-      Formula.t =
+  let substitute_formula (subst : t) ~(partial : bool) : Formula.t -> Formula.t
+      =
     let open Formula in
     let old_binders_substs = ref [] in
     let f_before a =
@@ -376,25 +376,17 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
           a
       | _ -> a
     in
-    map (Some f_before) (Some f_after) (Some (subst_in_expr subst ~partial)) a
+    map (Some f_before) (Some f_after) (Some (subst_in_expr subst ~partial))
 
-  let substitute_asrt (subst : t) ~(partial : bool) (a : Asrt.t) : Asrt.t =
-    Asrt.map None None
-      (Some (subst_in_expr subst ~partial))
-      (Some (substitute_formula subst ~partial))
-      a
+  let substitute_asrt (subst : t) ~(partial : bool) : Asrt.t -> Asrt.t =
+    Asrt.map (subst_in_expr subst ~partial) (substitute_formula subst ~partial)
 
-  let substitute_slcmd (subst : t) ~(partial : bool) (lcmd : SLCmd.t) : SLCmd.t
-      =
-    SLCmd.map None
-      (Some (substitute_asrt subst ~partial))
-      (Some (subst_in_expr subst ~partial))
-      lcmd
-
-  let substitute_lcmd (subst : t) ~(partial : bool) (lcmd : LCmd.t) : LCmd.t =
-    LCmd.map None
-      (Some (subst_in_expr subst ~partial))
-      (Some (substitute_formula subst ~partial))
-      (Some (substitute_slcmd subst ~partial))
-      lcmd
+  let substitute_slcmd (subst : t) ~(partial : bool) : SLCmd.t -> SLCmd.t =
+    SLCmd.map (substitute_asrt subst ~partial) (subst_in_expr subst ~partial)
+
+  let substitute_lcmd (subst : t) ~(partial : bool) : LCmd.t -> LCmd.t =
+    LCmd.map
+      (subst_in_expr subst ~partial)
+      (substitute_formula subst ~partial)
+      (substitute_slcmd subst ~partial)
 end
diff --git a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
index 07fd9b00..d2317315 100644
--- a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
+++ b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
@@ -59,13 +59,13 @@ module type S = sig
   val clean_up : ?keep:Expr.Set.t -> t -> Expr.Set.t * Expr.Set.t
   val lvars : t -> Containers.SS.t
   val alocs : t -> Containers.SS.t
-  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
+  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t
   val mem_constraints : t -> Formula.t list
   val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t
   val pp_err : Format.formatter -> err_t -> unit
   val get_failing_constraint : err_t -> Formula.t
   val can_fix : err_t -> bool
-  val get_fixes : err_t -> Asrt.t list list
+  val get_fixes : err_t -> Asrt.t list
   val sure_is_nonempty : t -> bool
 end
 
diff --git a/GillianCore/engine/symbolic_semantics/SMemory.ml b/GillianCore/engine/symbolic_semantics/SMemory.ml
index 0ca184d6..86267bea 100644
--- a/GillianCore/engine/symbolic_semantics/SMemory.ml
+++ b/GillianCore/engine/symbolic_semantics/SMemory.ml
@@ -54,12 +54,12 @@ module type S = sig
   val clean_up : ?keep:Expr.Set.t -> t -> Expr.Set.t * Expr.Set.t
   val lvars : t -> Containers.SS.t
   val alocs : t -> Containers.SS.t
-  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
+  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t
   val mem_constraints : t -> Formula.t list
   val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t
   val pp_err : Format.formatter -> err_t -> unit
   val get_failing_constraint : err_t -> Formula.t
-  val get_fixes : err_t -> Asrt.t list list
+  val get_fixes : err_t -> Asrt.t list
   val can_fix : err_t -> bool
   val sure_is_nonempty : t -> bool
 
diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml
index 9b6b0526..0dc1854e 100644
--- a/GillianCore/engine/symbolic_semantics/SState.ml
+++ b/GillianCore/engine/symbolic_semantics/SState.ml
@@ -507,7 +507,7 @@ module Make (SMemory : SMemory.S) :
     |> SS.union (Type_env.lvars gamma)
     |> SS.union spec_vars
 
-  let to_assertions ?(to_keep : SS.t option) (state : t) : Asrt.t list =
+  let to_assertions ?(to_keep : SS.t option) (state : t) : Asrt.t =
     let { heap; store; pfs; gamma; _ } = state in
     let store' =
       Option.fold
@@ -714,18 +714,16 @@ module Make (SMemory : SMemory.S) :
 
   (* get_fixes returns a list of possible fixes.
      Each "fix" is actually a list of assertions, each of which have to be applied to the same state *)
-  let get_fixes (err : err_t) : Asrt.t list list =
-    let pp_fixes fmt fixes =
-      Fmt.pf fmt "[[ %a ]]" (Fmt.list ~sep:(Fmt.any ", ") Asrt.pp) fixes
-    in
-    let one_step_fixes : Asrt.t list list =
+  let get_fixes (err : err_t) : Asrt.t list =
+    let pp_fix fmt fix = Fmt.pf fmt "[[ %a ]]" Asrt.pp fix in
+    let one_step_fixes : Asrt.t list =
       match err with
       | EMem err -> SMemory.get_fixes err
       | EPure f ->
           let result = [ [ Asrt.Pure f ] ] in
           L.verbose (fun m ->
               m "@[<v 2>Memory: Fixes found:@\n%a@]"
-                (Fmt.list ~sep:(Fmt.any "@\n") pp_fixes)
+                (Fmt.list ~sep:(Fmt.any "@\n") pp_fix)
                 result);
           result
       | EAsrt (_, _, fixes) ->
@@ -741,7 +739,7 @@ module Make (SMemory : SMemory.S) :
           in
           L.verbose (fun m ->
               m "@[<v 2>Memory: Fixes found:@\n%a@]"
-                (Fmt.list ~sep:(Fmt.any "@\n") pp_fixes)
+                (Fmt.list ~sep:(Fmt.any "@\n") pp_fix)
                 result);
           result
       | _ -> raise (Failure "DEATH: get_fixes: error cannot be fixed.")
@@ -749,7 +747,7 @@ module Make (SMemory : SMemory.S) :
 
     L.tmi (fun m ->
         m "All fixes before normalisation: %a"
-          Fmt.Dump.(list @@ list @@ Asrt.pp)
+          Fmt.Dump.(list Asrt.pp)
           one_step_fixes);
     List.map
       (fun fixes ->
diff --git a/GillianCore/gil_parser/GIL_Parser.mly b/GillianCore/gil_parser/GIL_Parser.mly
index 81ab250f..1495efd8 100644
--- a/GillianCore/gil_parser/GIL_Parser.mly
+++ b/GillianCore/gil_parser/GIL_Parser.mly
@@ -129,7 +129,7 @@ let normalised_lvar_r = Str.regexp "##NORMALISED_LVAR"
 %token ASSERT
 %token SEPASSERT
 %token INVARIANT
-%token CONSUME 
+%token CONSUME
 %token PRODUCE
 %token ASSUME_TYPE
 %token LSTNTH
@@ -699,30 +699,30 @@ g_assertion_target:
 (* P * Q *)
 (* The precedence of the separating conjunction is not the same as the arithmetic product *)
   | left_ass=g_assertion_target; FTIMES; right_ass=g_assertion_target
-    { Asrt.Star (left_ass, right_ass) } %prec separating_conjunction
+    { left_ass @ right_ass } %prec separating_conjunction
   | lhs = predicate_call; WAND; rhs = predicate_call
-    { Asrt.Wand {lhs; rhs } } %prec magic_wand
-(* <GA>(es; es) *)
+    { [ Asrt.Wand {lhs; rhs } ] } %prec magic_wand
+(* <CorePred>(es; es) *)
   | FLT; v=VAR; FGT; LBRACE; es1=separated_list(COMMA, expr_target); SCOLON; es2=separated_list(COMMA, expr_target); RBRACE
-    { Asrt.GA (v, es1, es2) }
+    { [ Asrt.CorePred (v, es1, es2) ] }
 (* emp *)
   | LEMP;
-    { Asrt.Emp }
+    { [ Asrt.Emp ] }
 (* x(e1, ..., en) *)
   | pcall = predicate_call
-    { 
+    {
       let (name, params) = pcall in
-      Asrt.Pred (name, params)
+      [ Asrt.Pred (name, params) ]
     }
 (* types (type_pairs) *)
   | LTYPES; LBRACE; type_pairs = separated_list(COMMA, type_env_pair_target); RBRACE
-    { Asrt.Types type_pairs }
+    { [ Asrt.Types type_pairs ] }
 (* (P) *)
   | LBRACE; g_assertion_target; RBRACE
     { $2 }
 (* pure *)
   | pure_assertion_target
-    { Asrt.Pure $1 }
+    { [ Asrt.Pure $1 ] }
 ;
 
 g_macro_target:
@@ -752,7 +752,7 @@ g_logic_cmd_target:
 (* unfold* x(e1, ..., en) [ def with #x := le1 and ... ] *)
   | RECUNFOLD; name = proc_name; LBRACE; les=separated_list(COMMA, expr_target); RBRACE; unfold_info = option(unfold_info_target)
     { LCmd.SL (Unfold (name, les, unfold_info, true)) }
-  
+
   | PACKAGE; LBRACE; lhs = predicate_call; WAND; rhs = predicate_call; RBRACE;
     { LCmd.SL (Package { lhs; rhs })}
 
@@ -765,10 +765,10 @@ g_logic_cmd_target:
 (* invariant (a) [existentials: x, y, z] *)
   | INVARIANT; LBRACE; a = g_assertion_target; RBRACE; binders = option(binders_target)
     { LCmd.SL (Invariant (a, Option.value ~default:[ ] binders)) }
-  
+
   | CONSUME; LBRACE; a = g_assertion_target; RBRACE; binders = option(binders_target)
     { LCmd.SL (Consume (a, Option.value ~default:[ ] binders)) }
-    
+
   | PRODUCE; LBRACE; a = g_assertion_target; RBRACE;
     { LCmd.SL (Produce a) }
 
diff --git a/GillianCore/monadic/MonadicSMemory.ml b/GillianCore/monadic/MonadicSMemory.ml
index c53d1376..c657baca 100644
--- a/GillianCore/monadic/MonadicSMemory.ml
+++ b/GillianCore/monadic/MonadicSMemory.ml
@@ -42,12 +42,12 @@ module type S = sig
   val clean_up : ?keep:Expr.Set.t -> t -> Expr.Set.t * Expr.Set.t
   val lvars : t -> Containers.SS.t
   val alocs : t -> Containers.SS.t
-  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
+  val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t
   val mem_constraints : t -> Formula.t list
   val get_recovery_tactic : t -> err_t -> vt Recovery_tactic.t
   val pp_err : Format.formatter -> err_t -> unit
   val get_failing_constraint : err_t -> Formula.t
-  val get_fixes : err_t -> Asrt.t list list
+  val get_fixes : err_t -> Asrt.t list
   val can_fix : err_t -> bool
   val pp_by_need : Containers.SS.t -> Format.formatter -> t -> unit
   val get_print_info : Containers.SS.t -> t -> Containers.SS.t * Containers.SS.t
@@ -67,7 +67,7 @@ module Lift (MSM : S) :
   include MSM
 
   let assertions ?to_keep t =
-    List.map Engine.Reduction.reduce_assertion (assertions ?to_keep t)
+    Engine.Reduction.reduce_assertion (assertions ?to_keep t)
 
   let execute_action action_name mem gpc params =
     let open Syntaxes.List in
diff --git a/kanillian/lib/compiler/logics.ml b/kanillian/lib/compiler/logics.ml
index 259881b4..19153cc4 100644
--- a/kanillian/lib/compiler/logics.ml
+++ b/kanillian/lib/compiler/logics.ml
@@ -2,7 +2,6 @@ open Gil_syntax
 module GType = Goto_lib.Type
 
 let rec asrt_of_scalar_like ~ctx (type_ : GType.t) (expr : Expr.t) : Asrt.t =
-  let open Asrt.Infix in
   match type_ with
   | CInteger I_bool ->
       (* Special case, the bounds are different *)
@@ -12,7 +11,7 @@ let rec asrt_of_scalar_like ~ctx (type_ : GType.t) (expr : Expr.t) : Asrt.t =
         expr #== Expr.one_i #|| (expr #== Expr.zero_i)
       in
       let asrt_range = Asrt.Pure condition in
-      assume_int ** asrt_range
+      [ assume_int; asrt_range ]
   | CInteger _ | Signedbv _ | Unsignedbv _ ->
       let assume_int = Asrt.Types [ (expr, IntType) ] in
       let bounds =
@@ -28,8 +27,8 @@ let rec asrt_of_scalar_like ~ctx (type_ : GType.t) (expr : Expr.t) : Asrt.t =
             in
             Asrt.Pure condition
       in
-      assume_int ** assume_range
-  | Double | Float -> Asrt.Types [ (expr, NumberType) ]
+      [ assume_int; assume_range ]
+  | Double | Float -> [ Asrt.Types [ (expr, NumberType) ] ]
   | Pointer _ ->
       let loc = LVar.alloc () in
       let ofs = LVar.alloc () in
@@ -40,8 +39,8 @@ let rec asrt_of_scalar_like ~ctx (type_ : GType.t) (expr : Expr.t) : Asrt.t =
         Asrt.Pure f
       in
       let types = Asrt.Types [ (e_loc, ObjectType); (e_ofs, IntType) ] in
-      assume_list ** types
-  | Bool -> Asrt.Types [ (expr, BooleanType) ]
+      [ assume_list; types ]
+  | Bool -> [ Asrt.Types [ (expr, BooleanType) ] ]
   | StructTag _ | Struct _ ->
       let ty =
         let fields = Ctx.resolve_struct_components ctx type_ in
@@ -56,11 +55,10 @@ let rec asrt_of_scalar_like ~ctx (type_ : GType.t) (expr : Expr.t) : Asrt.t =
 let assumption_of_param ~ctx ~(v : Var.t) ~(ty : GType.t) =
   (* The logic of what formulaes is generated should be factorised
      with [Compiled_expr.nondet_expr] *)
-  let open Asrt.Infix in
   if Ctx.representable_in_store ctx ty then
     let e_s = Expr.LVar (LVar.alloc ()) in
     let f = Formula.Eq (Expr.PVar v, e_s) in
-    Asrt.Pure f ** asrt_of_scalar_like ~ctx ty e_s
+    Asrt.Pure f :: asrt_of_scalar_like ~ctx ty e_s
   else failwith "unhandled: composit parameter"
 
 let assumption_of_ret_by_copy ~ctx ty =
@@ -71,11 +69,11 @@ let assumption_of_ret_by_copy ~ctx ty =
       ~perm:(Some Freeable)
   in
   let types = Asrt.Types [ (loc, ObjectType) ] in
-  Asrt.Star (types, hole)
+  [ types; hole ]
 
 let bispec ~ctx ~(compiled : (K_annot.t, string) Proc.t) (f : Program.Func.t) =
   let ret_type_assume =
-    if Ctx.representable_in_store ctx f.return_type then Asrt.Emp
+    if Ctx.representable_in_store ctx f.return_type then []
     else assumption_of_ret_by_copy ~ctx f.return_type
   in
   let param_names =
@@ -88,7 +86,7 @@ let bispec ~ctx ~(compiled : (K_annot.t, string) Proc.t) (f : Program.Func.t) =
       (fun v Param.{ type_ = ty; _ } -> assumption_of_param ~ctx ~v ~ty)
       param_names f.params
   in
-  let pre = List.fold_left Asrt.Infix.( ** ) ret_type_assume param_asrts in
+  let pre = ret_type_assume @ List.flatten param_asrts in
   BiSpec.
     {
       bispec_name = compiled.proc_name;
diff --git a/kanillian/lib/memory_model/GEnv.mli b/kanillian/lib/memory_model/GEnv.mli
index 6723bb82..5e4affdc 100644
--- a/kanillian/lib/memory_model/GEnv.mli
+++ b/kanillian/lib/memory_model/GEnv.mli
@@ -39,7 +39,7 @@ module Concrete : sig
   (** {3 Symbolic things} *)
 
   val substitution : Gillian.Symbolic.Subst.t -> t -> t
-  val assertions : t -> string list * Gillian.Gil_syntax.Asrt.t list
+  val assertions : t -> string list * Gillian.Gil_syntax.Asrt.t
 end
 
 module Symbolic : sig
@@ -79,5 +79,5 @@ module Symbolic : sig
   (** {3 Symbolic things} *)
 
   val substitution : Gillian.Symbolic.Subst.t -> t -> t
-  val assertions : t -> string list * Gillian.Gil_syntax.Asrt.t list
+  val assertions : t -> string list * Gillian.Gil_syntax.Asrt.t
 end
diff --git a/kanillian/lib/memory_model/SHeapTree.mli b/kanillian/lib/memory_model/SHeapTree.mli
index e0e13f8e..40a91970 100644
--- a/kanillian/lib/memory_model/SHeapTree.mli
+++ b/kanillian/lib/memory_model/SHeapTree.mli
@@ -74,7 +74,7 @@ val weak_valid_pointer : t -> Expr.t -> bool d_or_error
     [dst_tree] after modification *)
 val move : t -> Expr.t -> t -> Expr.t -> Expr.t -> t d_or_error
 
-val assertions : loc:string -> t -> Asrt.t list
+val assertions : loc:string -> t -> Asrt.t
 
 val substitution :
   le_subst:(Expr.t -> Expr.t) ->
diff --git a/kanillian/lib/memory_model/predicates.ml b/kanillian/lib/memory_model/predicates.ml
index 26cf9c72..80a296fc 100644
--- a/kanillian/lib/memory_model/predicates.ml
+++ b/kanillian/lib/memory_model/predicates.ml
@@ -3,7 +3,7 @@ open Gil_syntax
 module Core = struct
   let pred ga ins outs =
     let ga_name = Interface.str_ga ga in
-    Asrt.GA (ga_name, ins, outs)
+    Asrt.CorePred (ga_name, ins, outs)
 
   let single ~loc ~ofs ~chunk ~sval ~perm =
     let chunk = Expr.Lit (String (Chunk.to_string chunk)) in
diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml
index b7cc2a06..7f7ab1e4 100644
--- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml
+++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml
@@ -150,7 +150,7 @@ let rec compile_expr ?(fname = "main") ?(is_loop_prefix = false) expr :
     compiles a WLExpr into an output expression and a list of Global Assertions.
     the string list contains the name of the variables that are generated. They are existentials. *)
 let rec compile_lexpr ?(fname = "main") (lexpr : WLExpr.t) :
-    string list * Asrt.t list * Expr.t =
+    string list * Asrt.t * Expr.t =
   let gen_str = Generators.gen_str fname in
   let compile_lexpr = compile_lexpr ~fname in
   let expr_pname_of_binop b =
@@ -237,7 +237,7 @@ let rec compile_lexpr ?(fname = "main") (lexpr : WLExpr.t) :
         (List.concat gvars, List.concat asrtsl, Expr.ESet comp_exprs))
 
 (* TODO: compile_lformula should return also the list of created existentials *)
-let rec compile_lformula ?(fname = "main") formula : Asrt.t list * Formula.t =
+let rec compile_lformula ?(fname = "main") formula : Asrt.t * Formula.t =
   let gen_str = Generators.gen_str fname in
   let compile_lformula = compile_lformula ~fname in
   let compile_lexpr = compile_lexpr ~fname in
@@ -295,7 +295,6 @@ let rec compile_lassert ?(fname = "main") asser : string list * Asrt.t =
   let gen_str = Generators.gen_str fname in
   let compile_lexpr = compile_lexpr ~fname in
   let compile_lformula = compile_lformula ~fname in
-  let concat_star = List.fold_left (fun a1 a2 -> Asrt.Star (a1, a2)) in
   let gil_add e k =
     (* builds GIL expression that is e + k *)
     let k_e = Expr.int k in
@@ -362,9 +361,8 @@ let rec compile_lassert ?(fname = "main") asser : string list * Asrt.t =
     | [ le ] ->
         let exs2, la2, e2 = compile_lexpr le in
         ( exs1 @ exs2,
-          concat_star
-            (Asrt.GA (cell, [ eloc; eoffs ], [ e2 ]))
-            (bound @ la1 @ la2) )
+          Asrt.CorePred (cell, [ eloc; eoffs ], [ e2 ]) :: (bound @ la1 @ la2)
+        )
     | le :: r ->
         let exs2, la2, e2 = compile_lexpr le in
         let exs3, la3 =
@@ -373,47 +371,42 @@ let rec compile_lassert ?(fname = "main") asser : string list * Asrt.t =
             le1 r ~curr:(curr + 1)
         in
         ( exs1 @ exs2 @ exs3,
-          concat_star
-            (Asrt.GA (cell, [ eloc; eoffs ], [ e2 ]))
-            (bound @ (la3 :: (la1 @ la2))) )
+          Asrt.CorePred (cell, [ eloc; eoffs ], [ e2 ])
+          :: (bound @ la1 @ la2 @ la3) )
   in
   WLAssert.(
     match get asser with
-    | LEmp -> ([], Asrt.Emp)
+    | LEmp -> ([], [])
     | LStar (la1, la2) ->
         let exs1, cla1 = compile_lassert la1 in
         let exs2, cla2 = compile_lassert la2 in
-        (exs1 @ exs2, Asrt.Star (cla1, cla2))
+        (exs1 @ exs2, cla1 @ cla2)
     | LPointsTo (le1, lle) -> compile_pointsto ~block:false le1 lle
     | LBlockPointsTo (le1, lle) -> compile_pointsto ~block:true le1 lle
     | LPred (pr, lel) ->
         let exsl, all, el = list_split_3 (List.map compile_lexpr lel) in
         let exs = List.concat exsl in
         let al = List.concat all in
-        (exs, concat_star (Asrt.Pred (pr, el)) al)
+        (exs, Asrt.Pred (pr, el) :: al)
     | LWand { lhs = lname, largs; rhs = rname, rargs } ->
         let exs1, al1, el1 = list_split_3 (List.map compile_lexpr largs) in
         let exs2, al2, el2 = list_split_3 (List.map compile_lexpr rargs) in
         let exs = List.concat (exs1 @ exs2) in
         let al = List.concat (al1 @ al2) in
-        ( exs,
-          concat_star (Asrt.Wand { lhs = (lname, el1); rhs = (rname, el2) }) al
-        )
+        (exs, Asrt.Wand { lhs = (lname, el1); rhs = (rname, el2) } :: al)
     | LPure lf ->
         let al, f = compile_lformula lf in
-        ([], concat_star (Asrt.Pure f) al))
+        ([], Asrt.Pure f :: al))
 
 let rec compile_lcmd ?(fname = "main") lcmd =
   let compile_lassert = compile_lassert ~fname in
   let compile_lcmd = compile_lcmd ~fname in
   let compile_lexpr = compile_lexpr ~fname in
-  let concat_star = List.fold_left (fun a1 a2 -> Asrt.Star (a1, a2)) in
   let build_assert existentials lasrts =
     match lasrts with
     | [] -> None
-    | a :: r ->
-        let to_assert = concat_star a r in
-        let cmd = LCmd.SL (SLCmd.SepAssert (to_assert, existentials)) in
+    | _ ->
+        let cmd = LCmd.SL (SLCmd.SepAssert (lasrts, existentials)) in
         (* assert (assertions) {existentials: gvars} *)
         Some cmd
   in
@@ -1174,8 +1167,8 @@ let compile ~filepath WProg.{ context; predicates; lemmas } =
           List.map
             (fun var -> Asrt.Pure (Eq (Expr.PVar var, Expr.LVar ("#" ^ var))))
             proc.Proc.proc_params
-          |> Asrt.star
         in
+
         let bispec =
           BiSpec.
             {
diff --git a/wisl/lib/semantics/constr.ml b/wisl/lib/semantics/constr.ml
index 76eb85db..317da920 100644
--- a/wisl/lib/semantics/constr.ml
+++ b/wisl/lib/semantics/constr.ml
@@ -3,13 +3,13 @@ open Gil_syntax
 
 let cell ~loc ~offset ~value =
   let cell = str_ga Cell in
-  Asrt.GA (cell, [ loc; offset ], [ value ])
+  Asrt.CorePred (cell, [ loc; offset ], [ value ])
 
 let bound ~loc ~bound =
   let bound_ga = str_ga Bound in
   let bound = Expr.int bound in
-  Asrt.GA (bound_ga, [ loc ], [ bound ])
+  Asrt.CorePred (bound_ga, [ loc ], [ bound ])
 
 let freed ~loc =
   let freed = str_ga Freed in
-  Asrt.GA (freed, [ loc ], [])
+  Asrt.CorePred (freed, [ loc ], [])
diff --git a/wisl/lib/semantics/wislSHeap.mli b/wisl/lib/semantics/wislSHeap.mli
index e8f919f9..6fad4af1 100644
--- a/wisl/lib/semantics/wislSHeap.mli
+++ b/wisl/lib/semantics/wislSHeap.mli
@@ -56,7 +56,7 @@ val substitution_in_place :
   * (string * Gillian.Gil_syntax.Type.t) list)
   list
 
-val assertions : t -> Gillian.Gil_syntax.Asrt.t list
+val assertions : t -> Gillian.Gil_syntax.Asrt.t
 
 val add_debugger_variables :
   store:(string * Gillian.Gil_syntax.Expr.t) list ->
diff --git a/wisl/lib/semantics/wislSMemory.ml b/wisl/lib/semantics/wislSMemory.ml
index 512a198e..9fc830a2 100644
--- a/wisl/lib/semantics/wislSMemory.ml
+++ b/wisl/lib/semantics/wislSMemory.ml
@@ -311,7 +311,7 @@ let get_fixes (err : err_t) =
       let value = Expr.LVar new_var in
       let loc = Expr.loc_from_loc_name loc in
       let ga = WislLActions.str_ga WislLActions.Cell in
-      [ [ Asrt.GA (ga, [ loc; ofs ], [ value ]) ] ]
+      [ [ Asrt.CorePred (ga, [ loc; ofs ], [ value ]) ] ]
   | InvalidLocation loc ->
       let new_loc = ALoc.alloc () in
       let new_expr = Expr.ALoc new_loc in