From 4cc7f8b22f2615a53b087b14b3d00e8aa919bfb5 Mon Sep 17 00:00:00 2001
From: N1ark <n1ark.officiel@gmail.com>
Date: Thu, 10 Oct 2024 14:26:48 +0100
Subject: [PATCH] Use `Asrt.t` instead of fixes! (#313)

* Use `Asrt.t` instead of fixes!

* Rename types of `fix_t`

* Add note

* Remove `FSpecVars`??

* Remove fixes entirely?

* Oh wow ok
---
 Gillian-C/lib/MonadicSMemory.ml               | 127 +++----------
 Gillian-JS/lib/Semantics/JSILSMemory.ml       | 153 +++++-----------
 GillianCore/engine/Abstraction/PState.ml      |  17 +-
 GillianCore/engine/BiAbduction/BiState.ml     |  52 ++++--
 .../engine/concrete_semantics/CState.ml       |   8 +-
 GillianCore/engine/general_semantics/state.ml |   5 +-
 .../symbolic_semantics/Legacy_s_memory.ml     |  24 +--
 .../engine/symbolic_semantics/SMemory.ml      |  22 +--
 .../engine/symbolic_semantics/SState.ml       | 167 +++---------------
 GillianCore/monadic/MonadicSMemory.ml         |  27 +--
 kanillian/lib/memory_model/MonadicSMemory.ml  |  12 +-
 wisl/lib/semantics/wislSMemory.ml             |  22 +--
 12 files changed, 148 insertions(+), 488 deletions(-)

diff --git a/Gillian-C/lib/MonadicSMemory.ml b/Gillian-C/lib/MonadicSMemory.ml
index 8dea96a4..8cbb2d1a 100644
--- a/Gillian-C/lib/MonadicSMemory.ml
+++ b/Gillian-C/lib/MonadicSMemory.ml
@@ -656,28 +656,8 @@ let execute_genvgetdef heap params =
 
 (* Complete fixes  *)
 
-(* type c_fix_t *)
-type c_fix_t =
-  | AddSingle of { loc : string; ofs : Expr.t; value : Expr.t; chunk : Chunk.t }
-  | AddUnitialized of {
-      loc : string;
-      low : Expr.t;
-      high : Expr.t;
-      chunk : Chunk.t;
-    }
-
 (* Pretty printing utils *)
 
-let pp_c_fix fmt c_fix =
-  match c_fix with
-  | AddSingle { loc : string; ofs : Expr.t; value : Expr.t; chunk : Chunk.t } ->
-      Fmt.pf fmt "AddSingle(%s, %a, %a, %a)" loc Expr.pp ofs Expr.pp value
-        Chunk.pp chunk
-  | AddUnitialized
-      { loc : string; low : Expr.t; high : Expr.t; chunk : Chunk.t } ->
-      Fmt.pf fmt "AddUnitialized(%s, %a, %a, %a)" loc Expr.pp low Expr.pp high
-        Chunk.pp chunk
-
 let pp_err fmt (e : err_t) =
   match e with
   | InvalidLocation loc ->
@@ -909,74 +889,56 @@ let can_fix err =
   | SHeapTreeErr { sheaptree_err = MissingResource _; _ } -> true
   | _ -> false
 
-let get_fixes _heap _pfs _gamma err =
+let get_fixes err =
+  let open Constr.Core in
   Logging.verbose (fun m -> m "Getting fixes for error : %a" pp_err err);
   let get_fixes_h is_store loc ofs chunk =
     let open CConstants.VTypes in
+    let perm = Some Perm.Freeable in
+
     let fixes =
       match chunk with
-      | Chunk.Mfloat32 ->
-          let new_var = LVar.alloc () in
-          let set = SS.singleton new_var in
-          let new_var_e = Expr.LVar new_var in
-          let value = Expr.EList [ Expr.string single_type; new_var_e ] in
-          let vtypes = [ (new_var, Type.NumberType) ] in
-          [ ([ AddSingle { loc; ofs; value; chunk } ], [], vtypes, set) ]
-      | Mfloat64 ->
-          let new_var = LVar.alloc () in
-          let set = SS.singleton new_var in
-          let new_var_e = Expr.LVar new_var in
-          let value = Expr.EList [ Expr.string float_type; new_var_e ] in
-          let vtypes = [ (new_var, Type.NumberType) ] in
-          [ ([ AddSingle { loc; ofs; value; chunk } ], [], vtypes, set) ]
-      | Mint64 ->
-          let new_var = LVar.alloc () in
-          let set = SS.singleton new_var in
-          let new_var_e = Expr.LVar new_var in
-          let value = Expr.EList [ Expr.string long_type; new_var_e ] in
-          let vtypes = [ (new_var, Type.IntType) ] in
-          [ ([ AddSingle { loc; ofs; value; chunk } ], [], vtypes, set) ]
-      | Mptr ->
+      | Chunk.Mptr ->
           let new_var1 = LVar.alloc () in
           let new_var_e1 = Expr.LVar new_var1 in
           let new_var2 = LVar.alloc () in
           let new_var_e2 = Expr.LVar new_var2 in
-          let set = SS.add new_var2 (SS.singleton new_var1) in
           let value = Expr.EList [ new_var_e1; new_var_e2 ] in
           let null_typ =
             if Compcert.Archi.ptr64 then Expr.string long_type
             else Expr.string int_type
           in
           let null_ptr = Expr.EList [ null_typ; Expr.int 0 ] in
-          let vtypes =
-            [ (new_var1, Type.ObjectType); (new_var2, Type.IntType) ]
-          in
           [
-            ([ AddSingle { loc; ofs; value; chunk } ], [], vtypes, set);
-            ( [ AddSingle { loc; ofs; value = null_ptr; chunk } ],
-              [],
-              [],
-              SS.empty );
+            [
+              single ~loc ~ofs ~chunk ~sval:value ~perm;
+              Asrt.Types
+                [ (new_var_e1, Type.ObjectType); (new_var_e2, Type.IntType) ];
+            ];
+            [ single ~loc ~ofs ~chunk ~sval:null_ptr ~perm ];
           ]
       | _ ->
+          let type_str, type_gil =
+            match chunk with
+            | Chunk.Mfloat32 -> (single_type, Type.NumberType)
+            | Chunk.Mfloat64 -> (float_type, Type.NumberType)
+            | Chunk.Mint64 -> (long_type, Type.IntType)
+            | _ -> (int_type, Type.IntType)
+          in
           let new_var = LVar.alloc () in
-          let set = SS.singleton new_var in
           let new_var_e = Expr.LVar new_var in
-          let value = Expr.EList [ Expr.string int_type; new_var_e ] in
-          let vtypes = [ (new_var, Type.IntType) ] in
-          [ ([ AddSingle { loc; ofs; value; chunk } ], [], vtypes, set) ]
+          let value = Expr.EList [ Expr.string type_str; new_var_e ] in
+          [
+            [
+              single ~loc ~ofs ~chunk ~sval:value ~perm;
+              Asrt.Types [ (new_var_e, type_gil) ];
+            ];
+          ]
     in
     (* Additional fix for store operation to handle case of unitialized memory *)
     let fixes =
       if is_store then
-        ( [
-            AddUnitialized
-              { loc; low = ofs; high = offset_by_chunk ofs chunk; chunk };
-          ],
-          [],
-          [],
-          SS.empty )
-        :: fixes
+        [ hole ~loc ~low:ofs ~high:(offset_by_chunk ofs chunk) ~perm ] :: fixes
       else fixes
     in
     fixes
@@ -989,53 +951,22 @@ let get_fixes _heap _pfs _gamma err =
         loc_name;
         ofs_opt = Some ofs;
         chunk_opt = Some chunk;
-      } -> get_fixes_h is_store loc_name ofs chunk
+      } -> get_fixes_h is_store (Expr.loc_from_loc_name loc_name) ofs chunk
   | InvalidLocation loc ->
       let new_loc = ALoc.alloc () in
       let new_expr = Expr.ALoc new_loc in
-      [ ([], [ Formula.Eq (new_expr, loc) ], [], SS.empty) ]
+      [ [ Asrt.Pure (Eq (new_expr, loc)) ] ]
   | SHeapTreeErr
       {
         at_locations;
         sheaptree_err = MissingResource (Fixable { is_store; low; chunk });
       } -> (
       match at_locations with
-      | [ loc ] -> get_fixes_h is_store loc low chunk
+      | [ loc ] -> get_fixes_h is_store (Expr.loc_from_loc_name loc) low chunk
       | _ ->
           Logging.verbose (fun m ->
               m "SHeapTreeErr: Unsupported for more than 1 location");
           [])
   | _ -> []
 
-let apply_fix heap fix =
-  let open DR.Syntax in
-  match fix with
-  | AddSingle { loc; ofs; value; chunk } ->
-      Logging.verbose (fun m ->
-          m
-            "Applying AddSingle fix for error\n\
-            \ * location: '%s'\n\
-            \ * core_pred: %a\n\
-            \ * value: %a \n\
-            \ * chunk: %a \n"
-            loc Expr.pp ofs Expr.pp value Chunk.pp chunk);
-      let loc = Expr.loc_from_loc_name loc in
-      let* sval = SVal.of_gil_expr_exn value in
-      let perm = Perm.Freeable in
-      let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
-      { heap with mem }
-  | AddUnitialized { loc; low; high; chunk } ->
-      Logging.verbose (fun m ->
-          m
-            "Applying AddUnitialized fix for error\n\
-            \ * location: '%s'\n\
-            \ * low: %a\n\
-            \ * high: %a \n\
-            \ * chunk: %a \n"
-            loc Expr.pp low Expr.pp high Chunk.pp chunk);
-      let loc = Expr.loc_from_loc_name loc in
-      let perm = Perm.Freeable in
-      let++ mem = Mem.prod_hole heap.mem loc low high perm in
-      { heap with mem }
-
 let split_further _ _ _ _ = None
diff --git a/Gillian-JS/lib/Semantics/JSILSMemory.ml b/Gillian-JS/lib/Semantics/JSILSMemory.ml
index 0fc1ff89..9cf0a69e 100644
--- a/Gillian-JS/lib/Semantics/JSILSMemory.ml
+++ b/Gillian-JS/lib/Semantics/JSILSMemory.ml
@@ -31,11 +31,6 @@ module M = struct
     | FPure of Formula.t
   [@@deriving yojson, show]
 
-  type c_fix_t =
-    | CFLoc of string
-    | CFCell of vt * vt * vt
-    | CFMetadata of vt * vt
-
   type err_t = vt list * i_fix_t list list * Formula.t [@@deriving yojson, show]
 
   type action_ret =
@@ -52,15 +47,6 @@ module M = struct
     | FMetadata loc -> pf ft "@[<h>MIFMetadata(%a)@]" SVal.pp loc
     | FPure f -> pf ft "@[<h>MIFPure(%a)@]" Formula.pp f
 
-  let pp_c_fix ft (c_fix : c_fix_t) : unit =
-    let open Fmt in
-    match c_fix with
-    | CFLoc loc_name -> pf ft "@[<h>MCFLoc(%s)@]" loc_name
-    | CFCell (loc, prop, v) ->
-        pf ft "@[<h>MCFCell(%a, %a, %a)@]" SVal.pp loc SVal.pp prop SVal.pp v
-    | CFMetadata (loc, v) ->
-        pf ft "@[<h>MCFMetadata(%a, %a)@]" SVal.pp loc SVal.pp v
-
   let get_failing_constraint (err : err_t) : Formula.t =
     let _, _, f = err in
     f
@@ -611,20 +597,20 @@ module M = struct
   let prop_abduce_none_in_js = [ "@call" ]
   let prop_abduce_both_in_js = [ "hasOwnProperty" ]
 
-  type fix_result =
-    c_fix_t list * Formula.t list * (string * Type.t) list * Containers.SS.t
+  type fix_result = Asrt.t list
 
-  let complete_fix_js (pfs : PFS.t) (gamma : Type_env.t) (i_fix : i_fix_t) :
-      fix_result list =
+  let complete_fix_js (i_fix : i_fix_t) : fix_result list =
     match i_fix with
     | FLoc v ->
         (* Get a fresh location *)
-        let loc_name, _, new_pfs = fresh_loc ~loc:v pfs gamma in
-        (* TODO: If the initial value denoting the location was a variable, we may need to save it as a spec var *)
-        [ ([ CFLoc loc_name ], new_pfs, [], Containers.SS.empty) ]
+        (* This is dodgy, as the old instantiation does a bit more than this for this fix,
+           however it only seemed to add the binding without creating any state, so did it really
+           "do" anything? Bi-abduction is broken for Gillian-JS anyways. *)
+        let al = ALoc.alloc () in
+        [ [ Asrt.Pure (Eq (ALoc al, v)) ] ]
     | FCell (l, p) -> (
         let none_fix () =
-          ([ CFCell (l, p, Lit Nono) ], [], [], Containers.SS.empty)
+          [ Asrt.GA (JSILNames.aCell, [ l; p ], [ Lit Nono ]) ]
         in
 
         let some_fix () =
@@ -645,10 +631,12 @@ module M = struct
                 Lit (Bool true);
               ]
           in
-          ( [ CFCell (l, p, descriptor) ],
-            [ asrt_empty; asrt_none; asrt_list ],
-            [],
-            Containers.SS.singleton vvar )
+          [
+            Asrt.GA (JSILNames.aCell, [ l; p ], [ descriptor ]);
+            Asrt.Pure asrt_empty;
+            Asrt.Pure asrt_none;
+            Asrt.Pure asrt_list;
+          ]
         in
 
         match p with
@@ -658,70 +646,56 @@ module M = struct
             [ none_fix (); some_fix () ]
         | _ -> [ some_fix () ])
     | FMetadata l ->
-        let mloc_name, mloc, _ = fresh_loc pfs gamma in
+        let al = ALoc.alloc () in
+        let mloc = Expr.ALoc al in
         [
-          ( [
-              CFLoc mloc_name;
-              CFMetadata (l, mloc);
-              CFMetadata (mloc, Lit Null);
-              CFCell (mloc, Lit (String "@class"), Lit (String "Object"));
-              CFCell (mloc, Lit (String "@extensible"), Lit (Bool true));
-              CFCell
-                ( mloc,
-                  Lit (String "@proto"),
-                  Lit (Loc JS2JSIL_Helpers.locObjPrototype) );
-            ],
-            [],
-            [],
-            Containers.SS.empty );
+          [
+            Asrt.Pure (Eq (ALoc al, l));
+            Asrt.GA (JSILNames.aMetadata, [ l ], [ mloc ]);
+            Asrt.GA (JSILNames.aMetadata, [ mloc ], [ Lit Null ]);
+            Asrt.GA
+              ( JSILNames.aCell,
+                [ mloc; Lit (String "@class") ],
+                [ Lit (String "Object") ] );
+            Asrt.GA
+              ( JSILNames.aCell,
+                [ mloc; Lit (String "@extensible") ],
+                [ Lit (Bool true) ] );
+            Asrt.GA
+              ( JSILNames.aCell,
+                [ mloc; Lit (String "@proto") ],
+                [ Lit (Loc JS2JSIL_Helpers.locObjPrototype) ] );
+          ];
         ]
-    | FPure f -> [ ([], [ f ], [], Containers.SS.empty) ]
+    | FPure f -> [ [ Asrt.Pure f ] ]
 
   (* Fix completion: simple *)
-  let complete_fix_jsil (pfs : PFS.t) (gamma : Type_env.t) (i_fix : i_fix_t) :
-      fix_result list =
+  let complete_fix_jsil (i_fix : i_fix_t) : fix_result list =
     match i_fix with
     | FLoc v ->
         (* Get a fresh location *)
-        let loc_name, _, new_pfs = fresh_loc ~loc:v pfs gamma in
-        (* TODO: If the initial value denoting the location was a variable, we may need to save it as a spec var *)
-        [ ([ CFLoc loc_name ], new_pfs, [], Containers.SS.empty) ]
+        let al = ALoc.alloc () in
+        [ [ Asrt.Pure (Eq (ALoc al, v)) ] ]
     | FCell (l, p) ->
         (* Fresh variable to denote the property value *)
         let vvar = LVar.alloc () in
         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
-        [
-          ([ CFCell (l, p, v) ], [ not_none ], [], Containers.SS.singleton vvar);
-        ]
+        [ [ Asrt.GA (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
-        [
-          ([ CFMetadata (l, v) ], [ not_none ], [], Containers.SS.singleton vvar);
-        ]
-    | FPure f -> [ ([], [ f ], [], Containers.SS.empty) ]
+        [ [ Asrt.GA (JSILNames.aMetadata, [ l ], [ v ]); Asrt.Pure not_none ] ]
+    | FPure f -> [ [ Asrt.Pure f ] ]
 
   (* An error can have multiple fixes *)
-  let get_fixes (_ : t) (pfs : PFS.t) (gamma : Type_env.t) (err : err_t) :
-      fix_result list =
+  let get_fixes (err : err_t) : fix_result list =
     let pp_fix_result ft res =
       let open Fmt in
-      let fixes, pfs, tys, svars = res in
-      pf ft
-        "@[<v 2>@[<h>[[ %a ]]@]@\n\
-         @[<h>with PFS:%a@]@\n\
-         @[<h>with Types:%a@]@\n\
-         @[<h>spec vars: %a@]@]" (list ~sep:comma pp_c_fix) fixes
-        (list ~sep:comma Formula.pp)
-        pfs
-        (list ~sep:comma (pair ~sep:Fmt.(any ": ") string Type.pp))
-        tys
-        (iter ~sep:comma Containers.SS.iter string)
-        svars
+      pf ft "@[<v 2>@[<h>[[ %a ]]@]@\n@]" (list ~sep:comma Asrt.pp) res
     in
     let _, fixes, _ = err in
     L.verbose (fun m ->
@@ -736,19 +710,11 @@ module M = struct
     in
 
     let complete_ifixes (ifixes : i_fix_t list) : fix_result list =
-      let completed_ifixes = List.map (complete pfs gamma) ifixes in
+      let completed_ifixes = List.map complete ifixes in
       let completed_ifixes = List_utils.list_product completed_ifixes in
       let completed_ifixes : fix_result list =
         List.map
-          (fun fixes ->
-            List.fold_right
-              (fun (mfix, pfs, tys, svars) (mfix', pfs', tys', svars') ->
-                ( mfix @ mfix',
-                  pfs @ pfs',
-                  tys @ tys',
-                  Containers.SS.union svars svars' ))
-              fixes
-              ([], [], [], Containers.SS.empty))
+          (fun fixes -> List.fold_right List.append fixes [])
           completed_ifixes
       in
 
@@ -768,37 +734,6 @@ module M = struct
 
   let can_fix _ = true
 
-  let apply_fix (mem : t) (pfs : PFS.t) (gamma : Type_env.t) (fix : c_fix_t) :
-      t list =
-    let res =
-      match fix with
-      (* Missing metadata: create new, no new variables *)
-      | CFMetadata (l, v) -> (
-          match set_metadata mem pfs gamma l v with
-          | Ok [ (mem, [], new_pfs, []) ] ->
-              List.iter (fun f -> PFS.extend pfs f) new_pfs;
-              mem
-          | _ -> raise (Failure "Bi-abduction: cannot fix metadata."))
-      (* Missing location: create new *)
-      | CFLoc loc_name -> (
-          L.verbose (fun m -> m "CFLoc: %s" loc_name);
-          let loc : vt =
-            if Names.is_aloc_name loc_name then ALoc loc_name
-            else Lit (Loc loc_name)
-          in
-          match alloc mem pfs (Some loc) ~is_empty:true None with
-          | Ok [ (mem, [ loc' ], [], []) ] when loc' = loc -> mem
-          | _ -> raise (Failure "Bi-abduction: cannot fix missing location."))
-      (* Missing cell: create new *)
-      | CFCell (l, p, v) -> (
-          match set_cell mem pfs gamma l p v with
-          | Ok [ (mem, [], new_pfs, []) ] ->
-              List.iter (fun f -> PFS.extend pfs f) new_pfs;
-              mem
-          | _ -> raise (Failure "Bi-abduction: cannot fix cell."))
-    in
-    [ res ]
-
   let sorted_locs_with_vals (smemory : t) =
     let sorted_locs = Containers.SS.elements (SHeap.domain smemory) in
     List.map (fun loc -> (loc, Option.get (SHeap.get smemory loc))) sorted_locs
diff --git a/GillianCore/engine/Abstraction/PState.ml b/GillianCore/engine/Abstraction/PState.ml
index 20b12538..200377d4 100644
--- a/GillianCore/engine/Abstraction/PState.ml
+++ b/GillianCore/engine/Abstraction/PState.ml
@@ -66,7 +66,6 @@ module Make (State : SState.S) :
   type abs_t = Preds.abs_t
   type state_t = State.t
   type err_t = State.err_t [@@deriving yojson, show]
-  type fix_t = State.fix_t
   type m_err_t = State.m_err_t [@@deriving yojson]
 
   exception Internal_State_Error of err_t list * t
@@ -196,9 +195,8 @@ module Make (State : SState.S) :
     | None -> None
 
   let assume_t (astate : t) (v : Expr.t) (t : Type.t) : t option =
-    match State.assume_t astate.state v t with
-    | Some state -> Some { astate with state }
-    | None -> None
+    State.assume_t astate.state v t
+    |> Option.map (fun state -> { astate with state })
 
   let sat_check (astate : t) (v : Expr.t) : bool =
     State.sat_check astate.state v
@@ -1187,7 +1185,6 @@ module Make (State : SState.S) :
 
   let is_overlapping_asrt (a : string) : bool = State.is_overlapping_asrt a
   let pp_err = State.pp_err
-  let pp_fix = State.pp_fix
   let get_recovery_tactic astate vs = State.get_recovery_tactic astate.state vs
 
   let try_recovering (astate : t) (tactic : vt Recovery_tactic.t) :
@@ -1197,15 +1194,9 @@ module Make (State : SState.S) :
   let get_failing_constraint = State.get_failing_constraint
   let can_fix = State.can_fix
 
-  let get_fixes (astate : t) (errs : err_t) : fix_t list list =
+  let get_fixes (errs : err_t) =
     L.verbose (fun m -> m "AState: get_fixes");
-    State.get_fixes astate.state errs
-
-  let apply_fixes (astate : t) (fixes : fix_t list) : t list =
-    L.verbose (fun m -> m "AState: apply_fixes");
-    match State.apply_fixes astate.state fixes with
-    | [ state ] -> [ { astate with state } ]
-    | states -> List.map (copy_with_state astate) states
+    State.get_fixes errs
 
   let get_equal_values astate = State.get_equal_values astate.state
   let get_heap astate = State.get_heap astate.state
diff --git a/GillianCore/engine/BiAbduction/BiState.ml b/GillianCore/engine/BiAbduction/BiState.ml
index 80024928..056bb9cd 100644
--- a/GillianCore/engine/BiAbduction/BiState.ml
+++ b/GillianCore/engine/BiAbduction/BiState.ml
@@ -13,7 +13,6 @@ module Make (State : SState.S) = struct
   type store_t = SStore.t
   type m_err_t = t * State.m_err_t [@@deriving yojson]
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson]
-  type fix_t = State.fix_t
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
   type init_data = State.init_data
 
@@ -85,10 +84,8 @@ module Make (State : SState.S) = struct
     | None -> None
 
   let assume_t (bi_state : t) (v : Expr.t) (t : Type.t) : t option =
-    let { state; _ } = bi_state in
-    match State.assume_t state v t with
-    | Some state -> Some { bi_state with state }
-    | None -> None
+    State.assume_t bi_state.state v t
+    |> Option.map (fun state -> { bi_state with state })
 
   let sat_check ({ state; _ } : t) (v : Expr.t) : bool = State.sat_check state v
 
@@ -196,6 +193,33 @@ module Make (State : SState.S) = struct
     in
     SVal.SESubst.init bindings
 
+  let fix_list_apply s =
+    let open Syntaxes.List in
+    List.fold_left
+      (fun acc a ->
+        let* this_state = acc 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 ]
+        | Pure f ->
+            State.assume_a ~matching:true this_state [ f ] |> Option.to_list
+        | Types types ->
+            types
+            |> List.fold_left
+                 (fun ac (e, t) ->
+                   match ac with
+                   | None -> None
+                   | Some s -> State.assume_t s e t)
+                 (Some this_state)
+            |> Option.to_list
+        | GA (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 ]
+
   type post_res = (Flag.t * Asrt.t list) option
 
   let match_
@@ -240,12 +264,12 @@ module Make (State : SState.S) = struct
                 [])
               else (
                 L.verbose (fun m -> m "May be able to fix!!!");
-                let* fixes = State.get_fixes state err in
+                let* fixes = State.get_fixes err in
                 (* TODO: a better implementation here might be to say that apply_fix returns a list of fixed states, possibly empty *)
                 let state' = State.copy state in
                 let af_state' = State.copy af_state in
-                let* state' = State.apply_fixes state' fixes in
-                let* af_state' = State.apply_fixes af_state' fixes in
+                let* state' = fix_list_apply state' fixes in
+                let* af_state' = fix_list_apply af_state' fixes in
                 L.verbose (fun m -> m "BEFORE THE SIMPLIFICATION!!!");
                 let new_subst, states = State.simplify state' in
                 let state' =
@@ -424,12 +448,9 @@ module Make (State : SState.S) = struct
 
   (* to throw errors: *)
 
-  let get_fixes (_ : t) (_ : err_t) : fix_t list list =
+  let get_fixes (_ : err_t) : Asrt.t list list =
     raise (Failure "get_fixes not implemented in MakeBiState")
 
-  let apply_fixes (_ : t) (_ : fix_t list) : t list =
-    raise (Failure "apply_fixes not implemented in MakeBiState")
-
   let get_recovery_tactic (_ : t) (_ : err_t list) =
     raise (Failure "get_recovery_tactic not implemented in MakeBiState")
 
@@ -445,7 +466,6 @@ module Make (State : SState.S) = struct
 
   let is_overlapping_asrt (a : string) : bool = State.is_overlapping_asrt a
   let pp_err f e = State.pp_err f (unlift_error e)
-  let pp_fix = State.pp_fix
   let get_failing_constraint e = State.get_failing_constraint (unlift_error e)
   let can_fix e = State.can_fix (unlift_error e)
 
@@ -460,14 +480,14 @@ module Make (State : SState.S) = struct
     | Error err when not (State.can_fix err) ->
         [ Error (lift_error { procs; state; af_state } err) ]
     | Error err -> (
-        match State.get_fixes state err with
+        match State.get_fixes err with
         | [] -> [] (* No fix, we stop *)
         | fixes ->
             let* fix = fixes in
             let state' = State.copy state in
             let af_state' = State.copy af_state in
-            let* state' = State.apply_fixes state' fix in
-            let* af_state' = State.apply_fixes af_state' fix in
+            let* state' = fix_list_apply state' fix in
+            let* af_state' = fix_list_apply af_state' fix in
             execute_action action
               { procs; state = state'; af_state = af_state' }
               args)
diff --git a/GillianCore/engine/concrete_semantics/CState.ml b/GillianCore/engine/concrete_semantics/CState.ml
index e5585514..71bb9c00 100644
--- a/GillianCore/engine/concrete_semantics/CState.ml
+++ b/GillianCore/engine/concrete_semantics/CState.ml
@@ -32,7 +32,6 @@ end = struct
   type store_t = CStore.t
   type heap_t = CMemory.t
   type t = CMemory.t * CStore.t * vt list
-  type fix_t
   type m_err_t = CMemory.err_t [@@deriving yojson, show]
   type err_t = (m_err_t, vt) StateErr.t [@@deriving show]
   type init_data = CMemory.init_data
@@ -187,8 +186,6 @@ end = struct
   let mem_constraints (_ : t) : Formula.t list =
     raise (Failure "DEATH. mem_constraints")
 
-  let pp_fix _ _ = raise (Failure "str_of_fix from non-symbolic state.")
-
   let get_recovery_tactic _ =
     raise (Failure "get_recovery_tactic from non-symbolic state.")
 
@@ -212,12 +209,9 @@ end = struct
   let can_fix (_ : err_t) : bool = false
   let get_failing_constraint (_ : err_t) : Formula.t = True
 
-  let get_fixes (_ : t) (_ : err_t) : fix_t list list =
+  let get_fixes (_ : err_t) : Asrt.t list list =
     raise (Failure "Concrete: get_fixes not implemented in CState.Make")
 
-  let apply_fixes (_ : t) (_ : fix_t list) : t list =
-    raise (Failure "Concrete: apply_fixes not implemented in CState.Make")
-
   let get_equal_values _ vs = vs
 
   let get_heap state =
diff --git a/GillianCore/engine/general_semantics/state.ml b/GillianCore/engine/general_semantics/state.ml
index e3960dbd..c677d0e4 100644
--- a/GillianCore/engine/general_semantics/state.ml
+++ b/GillianCore/engine/general_semantics/state.ml
@@ -24,7 +24,6 @@ module type S = sig
   type m_err_t [@@deriving yojson]
 
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
-  type fix_t
 
   exception Internal_State_Error of err_t list * t
 
@@ -93,7 +92,6 @@ module type S = sig
     unit
 
   val pp_err : Format.formatter -> err_t -> unit
-  val pp_fix : Format.formatter -> fix_t -> unit
   val get_recovery_tactic : t -> err_t list -> vt Recovery_tactic.t
 
   (** State Copy *)
@@ -146,8 +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 : t -> err_t -> fix_t list list
-  val apply_fixes : t -> fix_t list -> t list
+  val get_fixes : err_t -> Asrt.t list list
   val get_equal_values : t -> vt list -> vt list
   val get_heap : t -> heap_t
 end
diff --git a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
index b6f6808b..07fd9b00 100644
--- a/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
+++ b/GillianCore/engine/symbolic_semantics/Legacy_s_memory.ml
@@ -9,7 +9,6 @@ module type S = sig
   (** Type of GIL substitutions *)
   type st = SVal.SESubst.t
 
-  type c_fix_t
   type err_t [@@deriving yojson, show]
 
   (** Type of GIL general states *)
@@ -62,21 +61,11 @@ module type S = sig
   val alocs : t -> Containers.SS.t
   val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
   val mem_constraints : t -> Formula.t list
-  val pp_c_fix : Format.formatter -> c_fix_t -> unit
   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 :
-    t ->
-    PFS.t ->
-    Type_env.t ->
-    err_t ->
-    (c_fix_t list * Formula.t list * (string * Type.t) list * Containers.SS.t)
-    list
-
-  val apply_fix : t -> PFS.t -> Type_env.t -> c_fix_t -> t list
+  val get_fixes : err_t -> Asrt.t list list
   val sure_is_nonempty : t -> bool
 end
 
@@ -84,7 +73,6 @@ module Dummy : S with type init_data = unit = struct
   type init_data = unit
   type vt = SVal.M.t
   type st = SVal.SESubst.t
-  type c_fix_t = unit
   type err_t = unit [@@deriving yojson, show]
   type t = unit [@@deriving yojson]
 
@@ -111,12 +99,10 @@ module Dummy : S with type init_data = unit = struct
   let alocs _ = failwith "Please implement SMemory"
   let assertions ?to_keep:_ _ = failwith "Please implement SMemory"
   let mem_constraints _ = failwith "Please implement SMemory"
-  let pp_c_fix _ _ = ()
   let get_recovery_tactic _ _ = failwith "Please implement SMemory"
   let pp_err _ _ = ()
   let get_failing_constraint _ = failwith "Please implement SMemory"
-  let get_fixes _ _ _ _ = failwith "Please implement SMemory"
-  let apply_fix _ _ _ _ = failwith "Please implement SMemory"
+  let get_fixes _ = failwith "Please implement SMemory"
   let can_fix _ = failwith "Please implement SMemory"
   let sure_is_nonempty _ = failwith "Please implement SMemory"
 end
@@ -167,11 +153,5 @@ module Modernize (Old_memory : S) = struct
         [] (* It's ok for failing producers to vanish, no unsoundness *)
     | Ok (heap', _) -> [ { set_res with value = heap' } ]
 
-  let apply_fix heap pfs gamma fix =
-    let open Syntaxes.List in
-    let+ heap = apply_fix heap pfs gamma fix in
-    let pc = Gpc.make ~matching:true ~pfs ~gamma () in
-    Gbranch.{ pc; value = heap }
-
   let split_further _ _ _ _ = None
 end
diff --git a/GillianCore/engine/symbolic_semantics/SMemory.ml b/GillianCore/engine/symbolic_semantics/SMemory.ml
index 572e83e0..0ca184d6 100644
--- a/GillianCore/engine/symbolic_semantics/SMemory.ml
+++ b/GillianCore/engine/symbolic_semantics/SMemory.ml
@@ -9,7 +9,6 @@ module type S = sig
   (** Type of GIL substitutions *)
   type st = SVal.SESubst.t
 
-  type c_fix_t
   type err_t [@@deriving yojson, show]
 
   (** Type of GIL general states *)
@@ -57,28 +56,18 @@ module type S = sig
   val alocs : t -> Containers.SS.t
   val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
   val mem_constraints : t -> Formula.t list
-  val pp_c_fix : Format.formatter -> c_fix_t -> unit
   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 :
-    t ->
-    PFS.t ->
-    Type_env.t ->
-    err_t ->
-    (c_fix_t list * Formula.t list * (string * Type.t) list * Containers.SS.t)
-    list
-
+  val get_fixes : err_t -> Asrt.t list list
   val can_fix : err_t -> bool
-  val apply_fix : t -> PFS.t -> Type_env.t -> c_fix_t -> t Gbranch.t list
   val sure_is_nonempty : t -> bool
 
   (** [split_further core_pred ins err] returns a way to split further a core_predicate if consuming it failed with error, if there is one.
       In that case, it returns a pair containing
       - a list of new ins. Each element is the list of ins for each sub-component of the core predicate;
       - new way of learning the outs, as explained under.
-      
+
       For example let's say the core predicate [(x, []) ↦ [a, b]] (with 2 ins and 1 out) can be split into
       - [(x, [0]) ↦ [a]]
       - [(x, [1]) ↦ [b]]
@@ -86,7 +75,7 @@ module type S = sig
       Then this function, given the appropriate error, should a pair of two elements:
       - the new ins: [ [ [x, [0]], [x, [1]] ] ]
       - the new way of learning the outs: [ [  {{ l-nth(PVar("0:0"), 0), l-nth(PVar("1:0"), 0) }}   ] ]
-      
+
       {b Important}: it is always sound for this function to return [None], it will just reduce the amount of automation.
       *)
   val split_further :
@@ -97,7 +86,6 @@ module Dummy : S with type init_data = unit = struct
   type init_data = unit
   type vt = SVal.M.t
   type st = SVal.SESubst.t
-  type c_fix_t = unit
   type err_t = unit [@@deriving yojson, show]
   type t = unit [@@deriving yojson]
 
@@ -118,12 +106,10 @@ module Dummy : S with type init_data = unit = struct
   let alocs _ = failwith "Please implement SMemory"
   let assertions ?to_keep:_ _ = failwith "Please implement SMemory"
   let mem_constraints _ = failwith "Please implement SMemory"
-  let pp_c_fix _ _ = ()
   let get_recovery_tactic _ _ = failwith "Please implement SMemory"
   let pp_err _ _ = ()
   let get_failing_constraint _ = failwith "Please implement SMemory"
-  let get_fixes _ _ _ _ = failwith "Please implement SMemory"
-  let apply_fix _ _ _ _ = failwith "Please implement SMemory"
+  let get_fixes _ = failwith "Please implement SMemory"
   let can_fix _ = failwith "Please implement SMemory"
   let sure_is_nonempty _ = failwith "Please implement SMemory"
   let split_further _ _ _ = failwith "Please implement SMemory"
diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml
index 50b85033..9b6b0526 100644
--- a/GillianCore/engine/symbolic_semantics/SState.ml
+++ b/GillianCore/engine/symbolic_semantics/SState.ml
@@ -54,13 +54,6 @@ module Make (SMemory : SMemory.S) :
 
   type variants_t = (string, Expr.t option) Hashtbl.t [@@deriving yojson]
   type init_data = SMemory.init_data
-
-  type fix_t =
-    | MFix of SMemory.c_fix_t
-    | FPure of Formula.t
-    | FTypes of (string * Type.t) list
-    | Fspec_vars of SS.t
-
   type err_t = (m_err_t, vt) StateErr.t [@@deriving yojson, show]
   type action_ret = (t * vt list, err_t) result list
 
@@ -336,8 +329,7 @@ module Make (SMemory : SMemory.S) :
             Expr.pp e msg (Fmt.Dump.list Formula.pp) ps);
       None
 
-  let assume_t (state : t) (v : vt) (t : Type.t) : t option =
-    let { gamma; _ } = state in
+  let assume_t ({ gamma; _ } as state : t) (v : vt) (t : Type.t) : t option =
     match Typing.reverse_type_lexpr true gamma [ (v, t) ] with
     | None -> None
     | Some gamma' ->
@@ -683,18 +675,6 @@ module Make (SMemory : SMemory.S) :
   let mem_constraints ({ heap; _ } : t) : Formula.t list =
     SMemory.mem_constraints heap
 
-  let pp_fix fmt = function
-    | MFix mf -> SMemory.pp_c_fix fmt mf
-    | FPure f -> Fmt.pf fmt "SFPure(%a)" Formula.pp f
-    | FTypes ts ->
-        Fmt.pf fmt "SFTypes(%a)"
-          Fmt.(list ~sep:comma (pair ~sep:(any ": ") string Type.pp))
-          ts
-    | Fspec_vars vs ->
-        Fmt.pf fmt "SFSVar(@[<h>%a@])"
-          (Fmt.iter ~sep:Fmt.comma SS.iter Fmt.string)
-          vs
-
   let get_recovery_tactic (state : t) (errs : err_t list) : vt Recovery_tactic.t
       =
     let { heap; pfs; _ } = state in
@@ -732,71 +712,17 @@ module Make (SMemory : SMemory.S) :
   let get_failing_constraint (err : err_t) : Formula.t =
     StateErr.get_failing_constraint err SMemory.get_failing_constraint
 
-  let normalise_fix (pfs : PFS.t) (gamma : Type_env.t) (fix : fix_t list) :
-      fix_t list option =
-    let fixes, pfs', spec_vars, types, asrts =
-      List.fold_right
-        (fun fix (mfix, pfs, spec_vars, types, asrts) ->
-          match fix with
-          | MFix mfix' -> (mfix' :: mfix, pfs, spec_vars, types, asrts)
-          | FPure pf' ->
-              ( mfix,
-                (if pf' = True then pfs else pf' :: pfs),
-                spec_vars,
-                types,
-                asrts )
-          | FTypes ts -> (mfix, pfs, spec_vars, ts @ types, asrts)
-          | Fspec_vars spec_vars' ->
-              (mfix, pfs, SS.union spec_vars' spec_vars, types, asrts))
-        fix ([], [], SS.empty, [], [])
-    in
-    (* Check SAT for some notion of checking SAT *)
-    let mfixes = List.map (fun fix -> MFix fix) fixes in
-    let ftys =
-      match types with
-      | [] -> []
-      | _ -> [ FTypes types ]
-    in
-    let gamma' =
-      let gamma' = Type_env.copy gamma in
-      let () = List.iter (fun (x, y) -> Type_env.update gamma' x y) types in
-      gamma'
-    in
-
-    let is_sat =
-      FOSolver.check_satisfiability (PFS.to_list pfs @ pfs') gamma'
-    in
-    match is_sat with
-    | true ->
-        let pfixes = List.map (fun pfix -> FPure pfix) pfs' in
-        Some
-          ((ftys @ if spec_vars = SS.empty then [] else [ Fspec_vars spec_vars ])
-          @ pfixes @ asrts @ mfixes)
-    | false ->
-        L.verbose (fun m -> m "Warning: invalid fix.");
-        None
-
   (* get_fixes returns a list of possible fixes.
-     Each "fix" is actually a list of fix_t, each of which have to be applied to the same state *)
-  let get_fixes (state : t) (err : err_t) : fix_t list list =
+     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 ", ") pp_fix) fixes
+      Fmt.pf fmt "[[ %a ]]" (Fmt.list ~sep:(Fmt.any ", ") Asrt.pp) fixes
     in
-    let { heap; pfs; gamma; _ } = state in
-    let one_step_fixes : fix_t list list =
+    let one_step_fixes : Asrt.t list list =
       match err with
-      | EMem err ->
-          List.map
-            (fun (mfixes, pfixes, types, spec_vars) ->
-              List.map (fun pf -> FPure pf) pfixes
-              @ (match types with
-                | [] -> []
-                | _ -> [ FTypes types ])
-              @ (if spec_vars == SS.empty then [] else [ Fspec_vars spec_vars ])
-              @ List.map (fun l -> MFix l) mfixes)
-            (SMemory.get_fixes heap pfs gamma err)
+      | EMem err -> SMemory.get_fixes err
       | EPure f ->
-          let result = [ [ FPure f ] ] in
+          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)
@@ -804,17 +730,13 @@ module Make (SMemory : SMemory.S) :
           result
       | EAsrt (_, _, fixes) ->
           let result =
-            List.map
-              (fun (fixes : Asrt.t list) ->
-                List.map
-                  (fun (fix : Asrt.t) ->
-                    match fix with
-                    | Pure fix -> FPure fix
-                    | _ ->
-                        raise
-                          (Exceptions.Impossible
-                             "Non-pure fix for an assertion failure"))
-                  fixes)
+            (List.map
+               (List.map (function
+                 | Asrt.Pure _ as fix -> fix
+                 | _ ->
+                     raise
+                       (Exceptions.Impossible
+                          "Non-pure fix for an assertion failure"))))
               fixes
           in
           L.verbose (fun m ->
@@ -827,62 +749,13 @@ module Make (SMemory : SMemory.S) :
 
     L.tmi (fun m ->
         m "All fixes before normalisation: %a"
-          Fmt.Dump.(list @@ list @@ pp_fix)
+          Fmt.Dump.(list @@ list @@ Asrt.pp)
           one_step_fixes);
-    (* Cartesian product of the fixes *)
-    let result =
-      List.filter_map
-        (fun fix ->
-          match normalise_fix pfs gamma fix with
-          | None | Some [] -> None
-          | other -> other)
-        one_step_fixes
-    in
-    L.(verbose (fun m -> m "Normalised fixes: %i" (List.length result)));
-    L.verbose (fun m ->
-        m "%a" (Fmt.list ~sep:(Fmt.any "@\n@\n") (Fmt.Dump.list pp_fix)) result);
-    result
-
-  (**
-   @param state The state on which to apply the fixes
-   @param fixes A list of fixes to apply
-
-   @return The state resulting from applying the fixes
-
-   [apply_fixes state fixes] applies the fixes [fixes] to the state [state],
-   and returns the resulting state, if successful.
-   *)
-  let apply_fixes (state : t) (fixes : fix_t list) : t list =
-    L.verbose (fun m -> m "SState: apply_fixes");
-    let apply_fix (states : t list) (fix : fix_t) : t list =
-      L.verbose (fun m -> m "applying fix: %a" pp_fix fix);
-      let open Syntaxes.List in
-      let* this_state = states in
-      let { heap; store; pfs; gamma; spec_vars } = this_state in
-      match fix with
-      (* Apply fix in memory - this may change the pfs and gamma *)
-      | MFix fix ->
-          L.verbose (fun m -> m "SState: before applying fixes %a" pp state);
-          let+ Gbranch.{ value = heap; pc } =
-            SMemory.apply_fix heap pfs gamma fix
-          in
-          { heap; store; pfs = pc.pfs; gamma = pc.gamma; spec_vars }
-      | FPure f ->
-          PFS.extend pfs f;
-          [ this_state ]
-      | FTypes types ->
-          List.iter (fun (x, y) -> Type_env.update gamma x y) types;
-          [ this_state ]
-      | Fspec_vars vars ->
-          let spec_vars = SS.union vars spec_vars in
-          [ { heap; store; pfs; gamma; spec_vars } ]
-    in
-
-    let result = List.fold_left apply_fix [ state ] fixes in
-
-    L.verbose (fun m ->
-        m "SState: after applying fixes %a" (Fmt.Dump.list pp) result);
-    result
+    List.map
+      (fun fixes ->
+        let pure, unpure = List.partition Asrt.is_pure_asrt fixes in
+        pure @ unpure)
+      one_step_fixes
 
   let get_equal_values state les =
     let { pfs; _ } = state in
diff --git a/GillianCore/monadic/MonadicSMemory.ml b/GillianCore/monadic/MonadicSMemory.ml
index 66065944..c53d1376 100644
--- a/GillianCore/monadic/MonadicSMemory.ml
+++ b/GillianCore/monadic/MonadicSMemory.ml
@@ -11,7 +11,6 @@ module type S = sig
   (** Type of GIL substitutions *)
   type st = SVal.SESubst.t
 
-  type c_fix_t
   type err_t [@@deriving show, yojson]
 
   (** Type of GIL general states *)
@@ -45,21 +44,11 @@ module type S = sig
   val alocs : t -> Containers.SS.t
   val assertions : ?to_keep:Containers.SS.t -> t -> Asrt.t list
   val mem_constraints : t -> Formula.t list
-  val pp_c_fix : Format.formatter -> c_fix_t -> unit
   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 :
-    t ->
-    PFS.t ->
-    Type_env.t ->
-    err_t ->
-    (c_fix_t list * Formula.t list * (string * Type.t) list * Containers.SS.t)
-    list
-
+  val get_fixes : err_t -> Asrt.t list list
   val can_fix : err_t -> bool
-  val apply_fix : t -> c_fix_t -> (t, err_t) result Delayed.t
   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
   val sure_is_nonempty : t -> bool
@@ -104,20 +93,6 @@ module Lift (MSM : S) :
     let gpc = Pc.to_gpc pc in
     Gbranch.{ pc = gpc; value }
 
-  let apply_fix heap pfs gamma fix =
-    Logging.verbose (fun m -> m "Bi-abduction trying to apply fix");
-    let res = apply_fix heap fix in
-    let curr_pc = Pc.make ~matching:false ~pfs ~gamma () in
-    let results = Delayed.resolve ~curr_pc res in
-
-    List.filter_map
-      (function
-        | Branch.{ pc; value = Ok x } ->
-            let gpc = Pc.to_gpc pc in
-            Some Gbranch.{ pc = gpc; value = x }
-        | _ -> None)
-      results
-
   let substitution_in_place ~pfs ~gamma subst mem :
       (t * Formula.Set.t * (string * Type.t) list) list =
     let process = substitution_in_place subst mem in
diff --git a/kanillian/lib/memory_model/MonadicSMemory.ml b/kanillian/lib/memory_model/MonadicSMemory.ml
index 8722ba61..11142ced 100644
--- a/kanillian/lib/memory_model/MonadicSMemory.ml
+++ b/kanillian/lib/memory_model/MonadicSMemory.ml
@@ -788,14 +788,8 @@ let execute_genvsetdef heap params =
       DR.ok (make_branch ~heap:{ heap with genv } ())
   | _ -> fail_ungracefully "genv_setdef" params
 
-(* Complete fixes  *)
-
-type c_fix_t = Nop
-
 (* Pretty printing utils *)
 
-let pp_c_fix _fmt _c_fix = failwith "Not ready for bi-abduction yet"
-
 let pp_err fmt (e : err_t) =
   match e with
   | InvalidLocation loc ->
@@ -1022,11 +1016,7 @@ let get_failing_constraint e =
   Fmt.failwith "Not ready for bi-abduction yet: get_failing_constraint %a"
     pp_err e
 
-let get_fixes _heap _pfs _gamma err =
-  Fmt.failwith "unimplemented get_fix for %a" pp_err err
-
-let apply_fix _heap fix =
-  Fmt.failwith "Not ready for bi-abdcution: apply_fix %a" pp_c_fix fix
+let get_fixes err = Fmt.failwith "unimplemented get_fix for %a" pp_err err
 
 let can_fix = function
   | MissingLocResource _
diff --git a/wisl/lib/semantics/wislSMemory.ml b/wisl/lib/semantics/wislSMemory.ml
index e2cd609a..512a198e 100644
--- a/wisl/lib/semantics/wislSMemory.ml
+++ b/wisl/lib/semantics/wislSMemory.ml
@@ -10,7 +10,6 @@ type init_data = unit
 type vt = Values.t
 type st = Subst.t
 type err_t = WislSHeap.err [@@deriving yojson, show]
-type c_fix_t = AddCell of { loc : string; ofs : Expr.t; value : Expr.t }
 type t = WislSHeap.t [@@deriving yojson]
 
 type action_ret =
@@ -285,11 +284,6 @@ let pp_err fmt t =
       Fmt.pf fmt "Invalid Location: '%a' cannot be resolved as a location"
         Expr.pp loc
 
-let pp_c_fix fmt c_fix =
-  match c_fix with
-  | AddCell { loc : string; ofs : Expr.t; value : Expr.t } ->
-      Fmt.pf fmt "AddCell(%s, %a, %a)" loc Expr.pp ofs Expr.pp value
-
 let get_recovery_tactic _ e =
   match e with
   | WislSHeap.MissingResource (_, loc, ofs) ->
@@ -309,25 +303,19 @@ let assertions ?to_keep:_ heap = WislSHeap.assertions heap
 let mem_constraints _ = []
 let is_overlapping_asrt _ = false
 
-let apply_fix m pfs gamma fix =
-  Logging.verbose (fun m -> m "Applying fixes for error");
-  match fix with
-  | AddCell { loc; ofs; value } ->
-      WislSHeap.set_cell ~pfs ~gamma m loc ofs value |> Result.get_ok;
-      [ m ]
-
-let get_fixes _ _ _ (err : err_t) =
+let get_fixes (err : err_t) =
   Logging.verbose (fun m -> m "Getting fixes for error : %a" pp_err err);
   match err with
   | MissingResource (Cell, loc, Some ofs) ->
       let new_var = LVar.alloc () in
       let value = Expr.LVar new_var in
-      let set = SS.singleton new_var in
-      [ ([ AddCell { loc; ofs; value } ], [], [], set) ]
+      let loc = Expr.loc_from_loc_name loc in
+      let ga = WislLActions.str_ga WislLActions.Cell in
+      [ [ Asrt.GA (ga, [ loc; ofs ], [ value ]) ] ]
   | InvalidLocation loc ->
       let new_loc = ALoc.alloc () in
       let new_expr = Expr.ALoc new_loc in
-      [ ([], [ Formula.Eq (new_expr, loc) ], [], SS.empty) ]
+      [ [ Asrt.Pure (Eq (new_expr, loc)) ] ]
   | _ -> []
 
 let can_fix = function