From f39d5b97fdec88ae2b95238c542bb422f96ffa21 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 15:47:49 +0100
Subject: [PATCH 01/23] Something is over-approx for some reason...

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml | 42 +++++++----------------
 GillianCore/monadic/delayed.ml            |  7 ++--
 2 files changed, 16 insertions(+), 33 deletions(-)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 17d6edec..43da0913 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -139,7 +139,6 @@ end
 
 module Make (State : SState.S) :
   S with type state_t = State.t and type err_t = State.err_t = struct
-  open Literal
   open Containers
   module L = Logging
 
@@ -1727,7 +1726,7 @@ module Make (State : SState.S) :
 
     let is_unfoldable_lit lit =
       match lit with
-      | Loc _ | LList _ -> false
+      | Literal.Loc _ | LList _ -> false
       | _ -> true
     in
 
@@ -2105,6 +2104,8 @@ module Make (State : SState.S) :
         in
         [ { lhs_state = new_lhs_state; current_state; subst } ]
       in
+      (* Importantly, we must *never* unfold anything on the lhs
+         without checking that it yields a unique state, as to avoid unsoundness. *)
       (* If it fails, we try splitting the step and we try again *)
       let- split_errs =
         let split_option =
@@ -2245,36 +2246,17 @@ module Make (State : SState.S) :
         let in_bindings = Pred.in_args rpred.pred all_bindings in
         SVal.SESubst.init in_bindings
       in
-      let start_states =
+      let start_state =
         match lhs_states with
-        | [] -> failwith "wand lhs is False!"
-        | first :: rest ->
-            let rest_pack_states =
-              List.map
-                (fun lhs_state ->
-                  {
-                    lhs_state;
-                    current_state = copy_astate astate;
-                    subst = SVal.SESubst.copy subst;
-                  })
-                rest
-            in
-            let first_pack_state =
-              { lhs_state = first; current_state = astate; subst }
-            in
-            first_pack_state :: rest_pack_states
-      in
-      L.verbose (fun m ->
-          m "About to start consuming rhs of wand. Currently %d search states"
-            (List.length start_states));
-      let final_states =
-        List.fold_left
-          (fun acc state ->
-            let* acc = acc in
-            let+ case = package_mp rhs_mp state in
-            case @ acc)
-          (Ok []) start_states
+        | [] -> Fmt.kstr L.fail "wand lhs is False!"
+        | [ lhs_state ] -> { lhs_state; current_state = astate; subst }
+        | _ :: _ ->
+            Fmt.kstr L.fail "Wand lhs produced %d states!@\n%a"
+              (List.length lhs_states)
+              (Fmt.list ~sep:(Fmt.any "@\n@\n@\nNEXT STATE@\n@\n@\n") pp_astate)
+              lhs_states
       in
+      let final_states = package_mp rhs_mp start_state in
       let* states = final_states in
       let all_res =
         List.map
diff --git a/GillianCore/monadic/delayed.ml b/GillianCore/monadic/delayed.ml
index 9b71a14c..dbef82b1 100644
--- a/GillianCore/monadic/delayed.ml
+++ b/GillianCore/monadic/delayed.ml
@@ -44,11 +44,12 @@ let branch_on
   | guard -> (
       try
         let guard_sat = FOSolver.sat ~pc:curr_pc guard in
-        if not guard_sat then (* [Not guard)] has to be sat *)
-          else_ () ~curr_pc
+        let not_guard = Formula.Infix.fnot guard in
+        if not guard_sat then
+          (* [Not guard] has to be sat *)
+          else_ () ~curr_pc:(Pc.extend curr_pc [ not_guard ])
         else
           let then_branches = then_ () ~curr_pc:(Pc.extend curr_pc [ guard ]) in
-          let not_guard = Formula.Infix.fnot guard in
           if FOSolver.sat ~pc:curr_pc not_guard then
             let else_branches =
               else_ () ~curr_pc:(Pc.extend curr_pc [ not_guard ])

From d23368c3f4c53c0814d7543765ddeef31c01f8a3 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 17:58:00 +0100
Subject: [PATCH 02/23] playing with gillian-c fire here

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml | 14 ++++++++++++++
 ppx_sat/test/out.expected                 |  2 +-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 43da0913..5ffe9607 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -756,6 +756,15 @@ module Make (State : SState.S) :
     | None -> other_state_err "final state non admissible"
     | Some state -> Res_list.return { state; preds; pred_defs; wands; variants }
 
+  let production_priority (a : Asrt.t) : int =
+    match a with
+    | Emp -> 0
+    | Types _ -> 0
+    | Pure _ -> 1
+    | Pred _ | Wand _ -> 2
+    | GA _ -> 3
+    | Star _ -> failwith "unreachable"
+
   let produce (astate : t) (subst : SVal.SESubst.t) (a : Asrt.t) :
       (t, err_t) Res_list.t =
     L.verbose (fun m ->
@@ -764,6 +773,11 @@ module Make (State : SState.S) :
            -----------------@\n\
            Produce assertion: @[%a@]@]" Asrt.pp a);
     let sas = MP.collect_simple_asrts a in
+    let sas =
+      List.sort
+        (fun a1 a2 -> compare (production_priority a1) (production_priority a2))
+        sas
+    in
     produce_asrt_list astate subst sas
 
   let produce_posts (state : t) (subst : SVal.SESubst.t) (asrts : Asrt.t list) :
diff --git a/ppx_sat/test/out.expected b/ppx_sat/test/out.expected
index b77944da..9d8b627e 100644
--- a/ppx_sat/test/out.expected
+++ b/ppx_sat/test/out.expected
@@ -1,7 +1,7 @@
 [{pc:
    {pfs: [(! (x == 1i))];
     gamma: (x: Int);
-    learned: [(1i i<=# x); (2i i<=# x)];
+    learned: [(0i i<# x); (1i i<# x); (1i i<=# x); (2i i<=# x)];
     learned_types: []};
   value: 12},
  {pc:

From 3336e20a47c9bf77a9e044aab08205ec5d548c03 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 18:53:48 +0100
Subject: [PATCH 03/23] trying something?

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/monadic/FOSolver.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/GillianCore/monadic/FOSolver.ml b/GillianCore/monadic/FOSolver.ml
index 9e8c10c1..ed2e1004 100644
--- a/GillianCore/monadic/FOSolver.ml
+++ b/GillianCore/monadic/FOSolver.ml
@@ -37,7 +37,6 @@ let check_entailment ~(pc : Pc.t) formula =
     in
     match f with
     | True -> true
-    | False -> false
     | _ ->
         FOSolver.check_entailment ~matching:pc.matching
           Utils.Containers.SS.empty pfs [ f ] gamma

From 859dc794d59ffb82fd46545ce740d7d3b34493b7 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 18:55:52 +0100
Subject: [PATCH 04/23] fix production in Gillian-C

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 Gillian-C/lib/MonadicSMemory.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Gillian-C/lib/MonadicSMemory.ml b/Gillian-C/lib/MonadicSMemory.ml
index 8dea96a4..bf26ae5d 100644
--- a/Gillian-C/lib/MonadicSMemory.ml
+++ b/Gillian-C/lib/MonadicSMemory.ml
@@ -525,7 +525,10 @@ 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 =
+        try SVal.of_gil_expr_exn sval_e
+        with SVal.NotACompCertValue _ -> Delayed.vanish ()
+      in
       let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
       { heap with mem }
   | _ -> fail_ungracefully "set_single" params

From 580bddb75c7e7f114c2a25bb182478aab5564ad5 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 19:17:09 +0100
Subject: [PATCH 05/23] What the fuck

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/FOSolver.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml
index 15ac1c79..6d070f4b 100644
--- a/GillianCore/engine/FOLogic/FOSolver.ml
+++ b/GillianCore/engine/FOLogic/FOSolver.ml
@@ -152,8 +152,7 @@ let check_entailment
   in
   let gamma_right = Type_env.filter gamma (fun v -> SS.mem v existentials) in
 
-  (* If left side is false, return false *)
-  if List.mem Formula.False (left_fs @ right_fs) then false
+  if List.mem Formula.False left_fs then true
   else
     (* Check satisfiability of left side *)
     let left_sat =

From 6a0316fb776a643bd898377678a5d4ed0f030999 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Mon, 8 Jul 2024 20:32:13 +0100
Subject: [PATCH 06/23] kill reduction exception on formula reduction

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 9a8202c1..a9610493 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2322,9 +2322,11 @@ and substitute_in_int_expr (le_to_find : Expr.t) (le_to_subst : Expr.t) le :
                       let c = Option.get c in
                       let () =
                         if not (Z.equal (c mod s) Z.zero) then
-                          failwith
-                            "Reduction.substitute_in_int_expr, scaling with \
-                             invalid number"
+                          raise
+                            (ReductionException
+                               ( le,
+                                 "Reduction.substitute_in_int_expr, scaling \
+                                  with invalid number" ))
                       in
                       c / s)
                     coeffs c_le_tf_symb
@@ -3034,7 +3036,14 @@ let reduce_formula
     ?(pfs : PFS.t = PFS.init ())
     ?(gamma = Type_env.init ())
     (a : Formula.t) : Formula.t =
-  reduce_formula_loop ~top_level:true ~rpfs matching pfs gamma a
+  try reduce_formula_loop ~top_level:true ~rpfs matching pfs gamma a
+  with ReductionException (e, msg) ->
+    Logging.normal (fun m ->
+        m
+          "WARNING: Reduction of formula %a failed while reducing %a with \
+           message %s. Not reducing this formula."
+          Formula.pp a Expr.pp e msg);
+    a
 
 let relate_llen
     (pfs : PFS.t)

From 9796097c0de172362263b4b2ce624361ff17f453 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 10 Jul 2024 15:09:59 +0100
Subject: [PATCH 07/23] experiment

---
 GillianCore/engine/general_semantics/general/g_interpreter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index 254f335e..a286b858 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -1719,7 +1719,7 @@ struct
   let evaluate_cmd = Evaluate_cmd.eval_cmd
 
   let simplify state =
-    snd (State.simplify ~save:true ~kill_new_lvars:true state)
+    snd (State.simplify ~kill_new_lvars:true state)
 
   let protected_evaluate_cmd
       (prog : annot MP.prog)

From 3765ddbcf0098f7ab4b1ffadacf57544772effa8 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 10 Jul 2024 16:01:40 +0100
Subject: [PATCH 08/23] flattening

---
 GillianCore/engine/symbolic_semantics/SState.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml
index 40534ef8..2ffd09f8 100644
--- a/GillianCore/engine/symbolic_semantics/SState.ml
+++ b/GillianCore/engine/symbolic_semantics/SState.ml
@@ -322,8 +322,9 @@ module Make (SMemory : SMemory.S) :
                (ps @ PFS.to_list pfs)
                gamma
         then (
-          List.iter (PFS.extend pfs) ps;
-          Some state)
+          let ps = List.concat_map Formula.split_conjunct_formulae ps in
+            List.iter (PFS.extend pfs) ps;
+            Some state)
         else (
           Logging.verbose (fun m ->
               m "assume_a: Couldn't assume %a" (Fmt.Dump.list Formula.pp) ps);

From 4036440659a9d0a685a74fff301973ecb763ebea Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 10 Jul 2024 22:03:46 +0100
Subject: [PATCH 09/23] back to life, back to reality

---
 GillianCore/engine/general_semantics/general/g_interpreter.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
index a286b858..254f335e 100644
--- a/GillianCore/engine/general_semantics/general/g_interpreter.ml
+++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -1719,7 +1719,7 @@ struct
   let evaluate_cmd = Evaluate_cmd.eval_cmd
 
   let simplify state =
-    snd (State.simplify ~kill_new_lvars:true state)
+    snd (State.simplify ~save:true ~kill_new_lvars:true state)
 
   let protected_evaluate_cmd
       (prog : annot MP.prog)

From 5f5ceb593a14f8c52367b1ddcced371b1132a405 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 10 Jul 2024 23:51:55 +0100
Subject: [PATCH 10/23] Branching when matching?

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml     | 20 ++++++++++++++++++-
 .../engine/symbolic_semantics/SState.ml       |  4 ++--
 GillianCore/utils/list_res.ml                 |  9 +++++++++
 3 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 5ffe9607..ca31130f 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -1561,7 +1561,6 @@ module Make (State : SState.S) :
                 L.fail "ERROR: IMPOSSIBLE! MATCHING ERRORS IN UX MODE!!!!"
             | false, [], [] ->
                 L.fail "OX MATCHING VANISHED??? MEDOOOOOOOO!!!!!!!!!"
-            | false, _ :: _ :: _, [] -> L.fail "DEATH. OX MATCHING BRANCHED"
             | true, [], _ ->
                 (* Vanished in UX *)
                 explore_next_states (rest_search_states, errs_so_far)
@@ -1582,6 +1581,25 @@ module Make (State : SState.S) :
                   ( ((state, subst, rest_mp), case_depth, false)
                     :: rest_search_states,
                     errs_so_far )
+            | false, states, [] -> (
+                (* We have obtained several branches. So there is a disjunction in the PFS.
+                   All branches need to successfuly unify against this *)
+                let all_next =
+                  List.map
+                    (fun state ->
+                      let state = copy_astate state in
+                      let subst = SVal.SESubst.copy subst in
+                      explore_next_states
+                        ( [ ((state, subst, rest_mp), case_depth, false) ],
+                          errs_so_far ))
+                    states
+                in
+                let res = List_res.flat all_next in
+                match res with
+                | Ok res -> Ok res
+                | Error errs ->
+                    explore_next_states (rest_search_states, errs @ errs_so_far)
+                )
             | true, first :: rem, [] ->
                 let rem =
                   List.map
diff --git a/GillianCore/engine/symbolic_semantics/SState.ml b/GillianCore/engine/symbolic_semantics/SState.ml
index 2ffd09f8..14ff886a 100644
--- a/GillianCore/engine/symbolic_semantics/SState.ml
+++ b/GillianCore/engine/symbolic_semantics/SState.ml
@@ -323,8 +323,8 @@ module Make (SMemory : SMemory.S) :
                gamma
         then (
           let ps = List.concat_map Formula.split_conjunct_formulae ps in
-            List.iter (PFS.extend pfs) ps;
-            Some state)
+          List.iter (PFS.extend pfs) ps;
+          Some state)
         else (
           Logging.verbose (fun m ->
               m "assume_a: Couldn't assume %a" (Fmt.Dump.list Formula.pp) ps);
diff --git a/GillianCore/utils/list_res.ml b/GillianCore/utils/list_res.ml
index c6e7abdb..ee0fe68f 100644
--- a/GillianCore/utils/list_res.ml
+++ b/GillianCore/utils/list_res.ml
@@ -9,6 +9,15 @@ let pp ~ok ~err =
 let return (v : 'a) : ('a, 'b) t = Ok [ v ]
 let vanish = Ok []
 
+let flat (l : ('a, 'b) t list) : ('a, 'b) t =
+  List.fold_left
+    (fun acc x ->
+      match (acc, x) with
+      | Ok l, Ok l' -> Ok (l @ l')
+      | Error l, Error l' -> Error (l @ l')
+      | Ok _, (Error _ as err) | (Error _ as err), Ok _ -> err)
+    (Ok []) l
+
 let bind (x : ('a, 'e) t) (f : 'a -> ('b, 'e) t) : ('b, 'e) t =
   match x with
   | Error errs -> Error errs

From 0c327c865126818afc89caabe555f33486364ffb Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Thu, 11 Jul 2024 00:03:10 +0100
Subject: [PATCH 11/23] some logging

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index ca31130f..4f14fa61 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -1582,6 +1582,11 @@ module Make (State : SState.S) :
                     :: rest_search_states,
                     errs_so_far )
             | false, states, [] -> (
+                L.verbose (fun m ->
+                    m
+                      "!!!CONSUMER YIELDED MULTIPLE BRANCHES IN OX MODE: %d \
+                       branches!!!"
+                      (List.length states));
                 (* We have obtained several branches. So there is a disjunction in the PFS.
                    All branches need to successfuly unify against this *)
                 let all_next =

From 4f38ff92bd140ec0d14e3330db5427081a736af2 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 17:20:50 +0100
Subject: [PATCH 12/23] attempt: make location resolution slightly more
 powerful?

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 101 +++++++++---------------
 1 file changed, 39 insertions(+), 62 deletions(-)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 3daa3b2a..3e1c536f 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2416,74 +2416,51 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     string option =
   let max_fuel = 5 in
 
+  let loc_name = function
+    | Expr.ALoc loc | Lit (Loc loc) -> Some loc
+    | _ -> None
+  in
+
   let rec resolve_expr_to_location_aux
       (fuel : int)
       (tried : Expr.Set.t)
       (to_try : Expr.t list) : string option =
+    let open Syntaxes.Option in
+    let* () = if fuel <= 0 then None else Some () in
     let f = resolve_expr_to_location_aux (fuel - 1) in
-    match fuel = 0 with
-    | true -> None
-    | false -> (
-        match to_try with
-        | [] -> None
-        | e :: _rest -> (
-            match e with
-            | Lit (Loc loc) | ALoc loc -> Some loc
-            | _ -> (
-                let equal_e = get_equal_expressions pfs e in
-                let equal_e =
-                  equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e
-                in
-                let ores =
-                  List.find_opt
-                    (fun x ->
-                      match x with
-                      | Expr.ALoc _ | Lit (Loc _) -> true
-                      | _ -> false)
-                    equal_e
-                in
-                match ores with
-                | Some (ALoc loc) | Some (Lit (Loc loc)) -> Some loc
-                | _ -> (
-                    let lvars_e =
-                      List.map
-                        (fun x -> Expr.LVar x)
-                        (Containers.SS.elements (Expr.lvars e))
-                    in
-                    let found_subst =
-                      List.map
-                        (fun e -> (e, get_equal_expressions pfs e))
-                        lvars_e
-                    in
-                    let found_subst =
-                      List.filter_map
-                        (fun (e, es) ->
-                          match es with
-                          | [] -> None
-                          | es :: _ -> Some (e, es))
-                        found_subst
-                    in
-                    let subst_e =
-                      List.fold_left
-                        (fun (e : Expr.t) (e_to, e_with) ->
-                          Expr.subst_expr_for_expr ~to_subst:e_to
-                            ~subst_with:e_with e)
-                        e found_subst
-                    in
-                    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
-                    match subst_e with
-                    | ALoc loc | Lit (Loc loc) -> Some loc
-                    | _ ->
-                        let new_tried = Expr.Set.add e tried in
-                        let new_to_try = equal_e @ [ subst_e ] in
-                        let new_to_try =
-                          List.filter
-                            (fun e -> not (Expr.Set.mem e new_tried))
-                            new_to_try
-                        in
-                        f new_tried new_to_try))))
+    let* e, rest =
+      match to_try with
+      | [] -> None
+      | e :: rest -> Some (e, rest)
+    in
+    (* If e is a loc name, we return it *)
+    let/ () = loc_name e in
+    let equal_e = get_equal_expressions pfs e in
+    let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
+    (* If we find a loc in there, we return it *)
+    let/ () = List.find_map loc_name equal_e in
+    let found_subst =
+      List.concat_map
+        (fun x ->
+          let e = Expr.LVar x in
+          List.map (fun es -> (e, es)) (get_equal_expressions pfs e))
+        (Containers.SS.elements (Expr.lvars e))
+    in
+    let subst_e =
+      List.fold_left
+        (fun (e : Expr.t) (e_to, e_with) ->
+          Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
+        e found_subst
+    in
+    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
+    let/ () = loc_name subst_e in
+    let new_tried = Expr.Set.add e tried in
+    let new_to_try = rest @ equal_e @ [ subst_e ] in
+    let new_to_try =
+      List.filter (fun e -> not (Expr.Set.mem e new_tried)) new_to_try
+    in
+    f new_tried new_to_try
   in
-
   resolve_expr_to_location_aux max_fuel Expr.Set.empty [ e ]
 
 let rec reduce_formula_loop

From be628fb8ab17efaf4c6398fd44977c5174745ca4 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 17:41:19 +0100
Subject: [PATCH 13/23] do not reduce before resolving location

---
 GillianCore/engine/FOLogic/FOSolver.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/GillianCore/engine/FOLogic/FOSolver.ml b/GillianCore/engine/FOLogic/FOSolver.ml
index 6284e27c..94bd8962 100644
--- a/GillianCore/engine/FOLogic/FOSolver.ml
+++ b/GillianCore/engine/FOLogic/FOSolver.ml
@@ -265,6 +265,4 @@ let num_is_less_or_equal ~pfs ~gamma e1 e2 =
 
 let resolve_loc_name ~pfs ~gamma loc =
   Logging.tmi (fun fmt -> fmt "get_loc_name: %a" Expr.pp loc);
-  match Reduction.reduce_lexpr ~pfs ~gamma loc with
-  | Lit (Loc loc) | ALoc loc -> Some loc
-  | loc' -> Reduction.resolve_expr_to_location pfs gamma loc'
+  Reduction.resolve_expr_to_location pfs gamma loc

From cd4eaed1651a1b9c5c2b6b6f5068bca58534fb03 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 17:55:25 +0100
Subject: [PATCH 14/23] a lot of printing when resolving locations

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 3e1c536f..0752ec35 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2426,6 +2426,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
       (tried : Expr.Set.t)
       (to_try : Expr.t list) : string option =
     let open Syntaxes.Option in
+    L.tmi (fun m -> m "to_try: %a" Fmt.(list ~sep:comma Expr.pp) to_try);
     let* () = if fuel <= 0 then None else Some () in
     let f = resolve_expr_to_location_aux (fuel - 1) in
     let* e, rest =
@@ -2437,6 +2438,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     let/ () = loc_name e in
     let equal_e = get_equal_expressions pfs e in
     let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
+    L.tmi (fun m -> m "equal_e: %a" Fmt.(list ~sep:comma Expr.pp) equal_e);
     (* If we find a loc in there, we return it *)
     let/ () = List.find_map loc_name equal_e in
     let found_subst =
@@ -2446,13 +2448,19 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
           List.map (fun es -> (e, es)) (get_equal_expressions pfs e))
         (Containers.SS.elements (Expr.lvars e))
     in
+    L.tmi (fun m ->
+        m "found_subst: (%a, %a)" Expr.pp e
+          Fmt.(list ~sep:comma (pair Expr.pp Expr.pp))
+          found_subst);
     let subst_e =
       List.fold_left
         (fun (e : Expr.t) (e_to, e_with) ->
           Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
         e found_subst
     in
+    L.tmi (fun m -> m "subst_e: %a" Expr.pp subst_e);
     let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
+    L.tmi (fun m -> m "reduced subst_e: %a" Expr.pp subst_e);
     let/ () = loc_name subst_e in
     let new_tried = Expr.Set.add e tried in
     let new_to_try = rest @ equal_e @ [ subst_e ] in

From 482bfac5f84d2676a1e96ece677b09209063ec61 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 18:01:48 +0100
Subject: [PATCH 15/23] fix printing

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 0752ec35..7d2193f6 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2426,7 +2426,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
       (tried : Expr.Set.t)
       (to_try : Expr.t list) : string option =
     let open Syntaxes.Option in
-    L.tmi (fun m -> m "to_try: %a" Fmt.(list ~sep:comma Expr.pp) to_try);
+    L.tmi (fun m -> m "to_try: %a" (Fmt.Dump.list Expr.pp) to_try);
     let* () = if fuel <= 0 then None else Some () in
     let f = resolve_expr_to_location_aux (fuel - 1) in
     let* e, rest =
@@ -2438,7 +2438,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     let/ () = loc_name e in
     let equal_e = get_equal_expressions pfs e in
     let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
-    L.tmi (fun m -> m "equal_e: %a" Fmt.(list ~sep:comma Expr.pp) equal_e);
+    L.tmi (fun m -> m "equal_e: %a" (Fmt.Dump.list Expr.pp) equal_e);
     (* If we find a loc in there, we return it *)
     let/ () = List.find_map loc_name equal_e in
     let found_subst =
@@ -2450,7 +2450,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     in
     L.tmi (fun m ->
         m "found_subst: (%a, %a)" Expr.pp e
-          Fmt.(list ~sep:comma (pair Expr.pp Expr.pp))
+          Fmt.(Dump.list (pair Expr.pp Expr.pp))
           found_subst);
     let subst_e =
       List.fold_left

From f1bd89035d1a299371f3f2837d1a0795ead03106 Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 20:31:06 +0100
Subject: [PATCH 16/23] ok, proper reinforcement of resolve_expr

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 46 +++++++++++++++----------
 1 file changed, 27 insertions(+), 19 deletions(-)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 7d2193f6..21f5a5ce 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2414,7 +2414,7 @@ and substitute_for_list_length (pfs : PFS.t) (le : Expr.t) : Expr.t =
 
 let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     string option =
-  let max_fuel = 5 in
+  let max_fuel = 10 in
 
   let loc_name = function
     | Expr.ALoc loc | Lit (Loc loc) -> Some loc
@@ -2438,32 +2438,40 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
     let/ () = loc_name e in
     let equal_e = get_equal_expressions pfs e in
     let equal_e = equal_e @ List.map (reduce_lexpr ~pfs ~gamma) equal_e in
-    L.tmi (fun m -> m "equal_e: %a" (Fmt.Dump.list Expr.pp) equal_e);
     (* If we find a loc in there, we return it *)
     let/ () = List.find_map loc_name equal_e in
-    let found_subst =
-      List.concat_map
+    (* We actually want to try all possible substs! *)
+    let all_lvars = Containers.SS.elements (Expr.lvars e) in
+    let subst_for_each_lvar =
+      List.map
         (fun x ->
           let e = Expr.LVar x in
-          List.map (fun es -> (e, es)) (get_equal_expressions pfs e))
-        (Containers.SS.elements (Expr.lvars e))
+          let with_eq =
+            List.map (fun eq -> (e, eq)) (get_equal_expressions pfs e)
+          in
+          (e, e) :: with_eq)
+        all_lvars
     in
-    L.tmi (fun m ->
-        m "found_subst: (%a, %a)" Expr.pp e
-          Fmt.(Dump.list (pair Expr.pp Expr.pp))
-          found_subst);
-    let subst_e =
+    let found_substs =
       List.fold_left
-        (fun (e : Expr.t) (e_to, e_with) ->
-          Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
-        e found_subst
+        (fun l1 l2 -> List_utils.cross_product l1 l2 ( @ ))
+        subst_for_each_lvar []
+    in
+    (* lvar and substs is a list [ (ei, esi) ] where for each ei, esi is a list of equal expressions.
+       We are going to build the product of each esi to obtain *)
+    let subst_es =
+      List.map
+        (fun found_subst ->
+          List.fold_left
+            (fun (e : Expr.t) (e_to, e_with) ->
+              Expr.subst_expr_for_expr ~to_subst:e_to ~subst_with:e_with e)
+            e found_subst)
+        found_substs
     in
-    L.tmi (fun m -> m "subst_e: %a" Expr.pp subst_e);
-    let subst_e = reduce_lexpr ~pfs ~gamma subst_e in
-    L.tmi (fun m -> m "reduced subst_e: %a" Expr.pp subst_e);
-    let/ () = loc_name subst_e in
+    let subst_es = List.map (reduce_lexpr ~pfs ~gamma) subst_es in
+    let/ () = List.find_map loc_name subst_es in
     let new_tried = Expr.Set.add e tried in
-    let new_to_try = rest @ equal_e @ [ subst_e ] in
+    let new_to_try = rest @ equal_e @ subst_es in
     let new_to_try =
       List.filter (fun e -> not (Expr.Set.mem e new_tried)) new_to_try
     in

From 4b03555799f9486ad3a5539d6456a76201d95fbf Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 20:38:47 +0100
Subject: [PATCH 17/23] re more logging

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 21f5a5ce..564f6b6c 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2452,11 +2452,19 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
           (e, e) :: with_eq)
         all_lvars
     in
+    L.tmi (fun m ->
+        m "subst_for_each_lvar: %a"
+          (Fmt.Dump.list (Fmt.Dump.list (Fmt.Dump.pair Expr.pp Expr.pp)))
+          subst_for_each_lvar);
     let found_substs =
       List.fold_left
         (fun l1 l2 -> List_utils.cross_product l1 l2 ( @ ))
         subst_for_each_lvar []
     in
+    L.tmi (fun m ->
+        m "found_substs: %a"
+          (Fmt.Dump.list (Fmt.Dump.list (Fmt.Dump.pair Expr.pp Expr.pp)))
+          found_substs);
     (* lvar and substs is a list [ (ei, esi) ] where for each ei, esi is a list of equal expressions.
        We are going to build the product of each esi to obtain *)
     let subst_es =
@@ -2468,6 +2476,7 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
             e found_subst)
         found_substs
     in
+    L.tmi (fun m -> m "subst_es: %a" (Fmt.Dump.list Expr.pp) subst_es);
     let subst_es = List.map (reduce_lexpr ~pfs ~gamma) subst_es in
     let/ () = List.find_map loc_name subst_es in
     let new_tried = Expr.Set.add e tried in

From 9f40f0ab04d16d23a2496140e58c487d5334d52d Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Wed, 11 Sep 2024 20:53:10 +0100
Subject: [PATCH 18/23] proper cross-product

Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 564f6b6c..20fb24d0 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2458,8 +2458,8 @@ let resolve_expr_to_location (pfs : PFS.t) (gamma : Type_env.t) (e : Expr.t) :
           subst_for_each_lvar);
     let found_substs =
       List.fold_left
-        (fun l1 l2 -> List_utils.cross_product l1 l2 ( @ ))
-        subst_for_each_lvar []
+        (fun l1 l2 -> List_utils.cross_product l1 l2 (fun l x -> x :: l))
+        [ [] ] subst_for_each_lvar
     in
     L.tmi (fun m ->
         m "found_substs: %a"

From 500c8688868baab4e4ef31ed0410d2ff83a5379a Mon Sep 17 00:00:00 2001
From: Sacha Ayoun <sachaayoun@gmail.com>
Date: Sun, 22 Dec 2024 00:23:46 +0100
Subject: [PATCH 19/23] verifier prints error

---
 GillianCore/engine/Abstraction/Verifier.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml
index 0f2a1114..667eb6a2 100644
--- a/GillianCore/engine/Abstraction/Verifier.ml
+++ b/GillianCore/engine/Abstraction/Verifier.ml
@@ -607,7 +607,11 @@ struct
             let successes, errors = Res_list.split lemma_evaluation_results in
             match errors with
             | [] -> analyse_lemma_results test successes
-            | _ ->
+            | errors ->
+                L.normal (fun m ->
+                    m "Failed to verify lemma, terminated with errors:\n%a"
+                      (Fmt.Dump.list SPState.pp_err)
+                      errors);
                 print_success_or_failure false;
                 false))
 

From 7aa8820ce374f4eee762d7f723018a0d52622a15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Sacha-=C3=89lie=20Ayoun?= <sachaayoun@gmail.com>
Date: Thu, 6 Feb 2025 13:16:32 +0100
Subject: [PATCH 20/23] add overly-specific reduction
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Sacha-Élie Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/FOLogic/Reduction.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/GillianCore/engine/FOLogic/Reduction.ml b/GillianCore/engine/FOLogic/Reduction.ml
index 20fb24d0..bbb87288 100644
--- a/GillianCore/engine/FOLogic/Reduction.ml
+++ b/GillianCore/engine/FOLogic/Reduction.ml
@@ -2567,6 +2567,10 @@ let rec reduce_formula_loop
           Eq (e, Lit (Num 0.))
       | Eq (BinOp (Lit (Int x), ITimes, e), Lit (Int z))
         when Z.equal z Z.zero && not (Z.equal x Z.zero) -> Eq (e, Expr.zero_i)
+      | Eq (lst, NOp (LstCat, [Expr.EList [ head ]; Expr.UnOp (Cdr, lst')])) when Expr.equal lst lst' ->
+        (* lst == ([head] @ (cdr lst)) *)
+          let open Formula.Infix in
+          head #== (Expr.list_nth lst 0)
       | Eq (Lit (LList ll), Lit (LList lr)) -> if ll = lr then True else False
       | Eq (EList le, Lit (LList ll)) | Eq (Lit (LList ll), EList le) ->
           if List.length ll <> List.length le then False

From a55e61cb0ca36727b58dc42ff68fb778a1f2f73c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Sacha-=C3=89lie=20Ayoun?= <sachaayoun@gmail.com>
Date: Sun, 9 Feb 2025 20:09:29 +0000
Subject: [PATCH 21/23] try something?
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Sacha-Élie Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 4f14fa61..0524de53 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -2286,7 +2286,12 @@ module Make (State : SState.S) :
       let start_state =
         match lhs_states with
         | [] -> Fmt.kstr L.fail "wand lhs is False!"
-        | [ lhs_state ] -> { lhs_state; current_state = astate; subst }
+        | [ lhs_state ] ->
+          (* We add (persistent) knowledge from lhs state to current state *)
+          let lhs_pfs = State.get_pfs lhs_state.state in
+          let current_pfs = State.get_pfs astate.state in
+          PFS.iter (fun f -> PFS.extend current_pfs f) lhs_pfs;
+          { lhs_state; current_state = astate; subst }
         | _ :: _ ->
             Fmt.kstr L.fail "Wand lhs produced %d states!@\n%a"
               (List.length lhs_states)

From e6987c443917bf3538d5a03064f2437717d9941c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Sacha-=C3=89lie=20Ayoun?= <sachaayoun@gmail.com>
Date: Sun, 9 Feb 2025 20:46:35 +0000
Subject: [PATCH 22/23] try assuming?
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Sacha-Élie Ayoun <sachaayoun@gmail.com>
---
 GillianCore/engine/Abstraction/Matcher.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 0524de53..171dcc4b 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -2286,12 +2286,14 @@ module Make (State : SState.S) :
       let start_state =
         match lhs_states with
         | [] -> Fmt.kstr L.fail "wand lhs is False!"
-        | [ lhs_state ] ->
+        | [ lhs_state ] -> (
           (* We add (persistent) knowledge from lhs state to current state *)
-          let lhs_pfs = State.get_pfs lhs_state.state in
-          let current_pfs = State.get_pfs astate.state in
-          PFS.iter (fun f -> PFS.extend current_pfs f) lhs_pfs;
-          { lhs_state; current_state = astate; subst }
+          let lhs_pfs = State.get_pfs lhs_state.state |> PFS.to_list in
+          match State.assume_a ~matching:true ~production:true astate.state lhs_pfs with
+          | Some state ->
+            { lhs_state; current_state = { astate with state }; subst }
+          | None ->
+            Fmt.kstr L.fail "Wand lhs pure contradicts with current state!")
         | _ :: _ ->
             Fmt.kstr L.fail "Wand lhs produced %d states!@\n%a"
               (List.length lhs_states)

From c6bb19b616da32eac1a98378c6fab3174b2d6c70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Sacha-=C3=89lie=20Ayoun?= <sachaayoun@gmail.com>
Date: Mon, 10 Feb 2025 12:31:14 +0000
Subject: [PATCH 23/23] trying something
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Signed-off-by: Sacha-Élie Ayoun <sachaayoun@gmail.com>
---
 GillianCore/GIL_Syntax/Formula.ml             |  2 +-
 GillianCore/engine/Abstraction/Matcher.ml     | 14 ++++++++++----
 GillianCore/engine/FOLogic/Simplifications.ml |  4 ++--
 3 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/GillianCore/GIL_Syntax/Formula.ml b/GillianCore/GIL_Syntax/Formula.ml
index ae52b295..901ba876 100644
--- a/GillianCore/GIL_Syntax/Formula.ml
+++ b/GillianCore/GIL_Syntax/Formula.ml
@@ -153,7 +153,7 @@ let alocs (f : t) : SS.t = Visitors.Collectors.aloc_collector#visit_formula () f
 let clocs (f : t) : SS.t = Visitors.Collectors.cloc_collector#visit_formula () f
 
 (* Get all the locations in [a] *)
-let locs (f : t) : SS.t = Visitors.Collectors.cloc_collector#visit_formula () f
+let locs (f : t) : SS.t = Visitors.Collectors.loc_collector#visit_formula () f
 let get_print_info (a : t) = (pvars a, lvars a, locs a)
 
 (* Get all the logical expressions of --a-- of the form (Lit (LList lst)) and (EList lst)  *)
diff --git a/GillianCore/engine/Abstraction/Matcher.ml b/GillianCore/engine/Abstraction/Matcher.ml
index 171dcc4b..688d7449 100644
--- a/GillianCore/engine/Abstraction/Matcher.ml
+++ b/GillianCore/engine/Abstraction/Matcher.ml
@@ -1924,7 +1924,7 @@ module Make (State : SState.S) :
       match produced with
       | Error _ -> []
       | Ok state ->
-          let _, simplified = simplify_astate ~matching:true state in
+          let _, simplified = simplify_astate ~save:true ~matching:true state in
           simplified
 
     let match_assertion astate subst step =
@@ -2289,9 +2289,15 @@ module Make (State : SState.S) :
         | [ lhs_state ] -> (
           (* We add (persistent) knowledge from lhs state to current state *)
           let lhs_pfs = State.get_pfs lhs_state.state |> PFS.to_list in
-          match State.assume_a ~matching:true ~production:true astate.state lhs_pfs with
-          | Some state ->
-            { lhs_state; current_state = { astate with state }; subst }
+          let lhs_alocs =
+            List.fold_left
+              (fun acc pf -> SS.union acc (Formula.alocs pf))
+              SS.empty lhs_pfs
+          in
+          let current_sstate =  State.add_spec_vars astate.state lhs_alocs in 
+          match State.assume_a ~matching:true ~production:true current_sstate lhs_pfs with
+          | Some current_sstate ->
+            { lhs_state; current_state = { astate with state = current_sstate }; subst }
           | None ->
             Fmt.kstr L.fail "Wand lhs pure contradicts with current state!")
         | _ :: _ ->
diff --git a/GillianCore/engine/FOLogic/Simplifications.ml b/GillianCore/engine/FOLogic/Simplifications.ml
index 3603cfec..c3433640 100644
--- a/GillianCore/engine/FOLogic/Simplifications.ml
+++ b/GillianCore/engine/FOLogic/Simplifications.ml
@@ -549,9 +549,9 @@ let simplify_pfs_and_gamma
                 | ALoc alocl, ALoc alocr when matching ->
                     L.verbose (fun fmt ->
                         fmt "Two equal alocs: %s and %s" alocl alocr);
-                    SESubst.put result (ALoc alocr) (ALoc alocl);
+                    SESubst.put result (ALoc alocl) (ALoc alocr);
                     let temp_subst =
-                      SESubst.init [ (ALoc alocr, ALoc alocl) ]
+                      SESubst.init [ (ALoc alocl, ALoc alocr) ]
                     in
                     PFS.substitution temp_subst lpfs;
                     let substituted =