diff --git a/lib/analysis/dune b/lib/analysis/dune
index 65f48ebc..a98ac6ef 100644
--- a/lib/analysis/dune
+++ b/lib/analysis/dune
@@ -13,11 +13,12 @@
   ide_live
   lattice_collections
   wrapped_intervals
-  known_bits
   gamma_domain
+  linear_const
   tnum_wint_reduced_product
   known_bits
   wp_dual
+  sva
   linear_const
   inter_copy)
  (libraries
diff --git a/lib/analysis/lattice_collections.ml b/lib/analysis/lattice_collections.ml
index 4ca40967..9d6ed174 100644
--- a/lib/analysis/lattice_collections.ml
+++ b/lib/analysis/lattice_collections.ml
@@ -78,6 +78,7 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct
       let name = V.name ^ "MapLattice"
       let bottom = BotMap KM.empty
       let top = TopMap KM.empty
+      let singleton k v = BotMap (KM.singleton k v)
 
       let top_vjoin _ x y =
         let j = V.join x y in
@@ -195,6 +196,13 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct
       let to_list = function
         | BotMap m -> (`Bottom, KM.to_list m)
         | TopMap m -> (`Top, KM.to_list m)
+
+      let mapi f = function
+        | BotMap m -> BotMap (KM.mapi f m)
+        | TopMap m -> TopMap (KM.mapi f m)
+
+      let fold f m acc =
+        match m with BotMap m -> KM.fold f m acc | TopMap m -> KM.fold f m acc
     end :
       sig
         include StateAbstraction with type val_t = V.t and type key_t = K.t
@@ -204,6 +212,9 @@ module LatticeMap (K : MapKey) (V : TopLattice) = struct
         val of_list_bot : (K.t * V.t) list -> t
         val cardinal : t -> int
         val to_list : t -> [ `Bottom | `Top ] * (K.t * V.t) list
+        val singleton : K.t -> V.t -> t
+        val mapi : (K.t -> V.t -> V.t) -> t -> t
+        val fold : (K.t -> V.t -> 'a -> 'a) -> t -> 'a -> 'a
       end)
 
   module V = V
diff --git a/lib/analysis/sva.ml b/lib/analysis/sva.ml
new file mode 100644
index 00000000..590a90d1
--- /dev/null
+++ b/lib/analysis/sva.ml
@@ -0,0 +1,328 @@
+(*
+  SVA analysis
+    - Based off of the DSA paper
+      the first iteration I believe as newer one have had the SVA sections reduced
+
+  Note: This does not result in amazing results currently, may need a paper focused
+    on SVA or more research to improve it, it only really works with mallocs (for
+    type inference use case) 
+*)
+
+open Lang
+open Containers
+open Common
+open Wrapped_intervals
+
+(*
+  TODO
+    Figure out what the SymBases should actually have in them, is it just for cute printing?
+*)
+
+module SymBase = struct
+  type t =
+    (* Known *)
+    | Stack of string
+    | Heap of { name : string }
+    | GlobSym
+    | Constant
+    (* Unknown *)
+    | Par of { name : string; param : Var.t }
+    | Ret of { name : string; param : Var.t }
+    | Loaded
+  [@@deriving ord, eq]
+
+  let show = function
+    | Stack name -> Printf.sprintf "Stack(%s)" name
+    | Heap { name } -> Printf.sprintf "Heap(%s)" name
+    | GlobSym -> "Global"
+    | Constant -> "Constant"
+    | Par { name; param } -> Printf.sprintf "Par(%s_%s)" name (Var.show param)
+    | Ret { name; param } -> Printf.sprintf "Ret(%s_%s)" name (Var.show param)
+    | Loaded -> Printf.sprintf "Loaded"
+
+  let is_place_holder = function
+    | Stack _ | Heap _ | GlobSym | Constant -> false
+    | Ret _ | Par _ | Loaded -> true
+
+  let to_int = Hashtbl.hash
+  let pretty a = Containers_pp.text @@ show a
+  let is_stack = function Stack _ -> true | _ -> false
+end
+
+module IntervalDomain = struct
+  open WrappedIntervalsLattice
+
+  type t = WrappedIntervalsLattice.t [@@deriving eq, ord]
+
+  let name = "interval offsets domain "
+  let pretty = WrappedIntervalsLattice.pretty
+  let show = WrappedIntervalsLattice.show
+  let bottom = WrappedIntervalsLattice.bottom
+  let leq = WrappedIntervalsLattice.leq
+  let widening = WrappedIntervalsLattice.widening
+  let join = WrappedIntervalsLattice.join
+  let top = WrappedIntervalsLattice.Top
+  let neg = WrappedIntervalsLatticeOps.neg
+  let init a = interval a a
+end
+
+module SymAddrSetLattice = struct
+  include Lattice_collections.LatticeMap (SymBase) (IntervalDomain)
+end
+
+module SVAAbstraction = struct
+  include SymAddrSetLattice
+  open WrappedIntervalsValueAbstractionBasil
+
+  let eval_const (op : Lang.Ops.AllOps.const) rt =
+    SymAddrSetLattice.singleton SymBase.Constant @@ eval_const op rt
+
+  let eval_unop (op : Lang.Ops.AllOps.unary) (a, t) rt =
+    SymAddrSetLattice.mapi
+      (fun sb1 vs1 ->
+        match sb1 with
+        | SymBase.GlobSym | Constant -> eval_unop op (vs1, t) rt
+        | _ -> Top)
+      a
+
+  let eval_binary op (a, ta) (b, tb) rt =
+    SymAddrSetLattice.fold
+      (fun sb1 vs1 map ->
+        SymAddrSetLattice.fold
+          (fun sb2 vs2 map ->
+            match (sb1, sb2) with
+            (* WARN: not 100% sure about this case but makes sense in head we would prefer one over the other? *)
+            | (SymBase.GlobSym | Constant), (SymBase.GlobSym | Constant) ->
+                let sb =
+                  if SymBase.equal sb1 GlobSym || SymBase.equal sb2 GlobSym then
+                    SymBase.GlobSym
+                  else Constant
+                in
+                SymAddrSetLattice.singleton sb
+                  (eval_binary op (vs1, ta) (vs2, tb) rt)
+            | (SymBase.GlobSym | Constant), sb | sb, (SymBase.GlobSym | Constant)
+              ->
+                SymAddrSetLattice.update sb
+                  (eval_binary op (vs1, ta) (vs2, tb) rt)
+                  map
+            | _, _ ->
+                SymAddrSetLattice.update sb1 Top
+                @@ SymAddrSetLattice.update sb2 Top map)
+          b map)
+      a SymAddrSetLattice.bottom
+
+  let eval_binop op a b rt =
+    match op with #Lang.Ops.AllOps.binary as op -> eval_binary op a b rt
+
+  let eval_intrin (op : E.intrin) args rt =
+    let op a b =
+      match op with
+      | (`BVADD | `BVOR | `BVXOR | `BVAND | `BVMUL) as op ->
+          (eval_binary op a b rt, rt)
+      | `OR | `AND | `Cases | `MapUpdate -> (SymAddrSetLattice.top, rt)
+      | `BVConcat ->
+          ( SymAddrSetLattice.fold
+              (fun sb1 vs1 acc ->
+                SymAddrSetLattice.fold
+                  (fun sb2 vs2 map ->
+                    let return_size =
+                      match (snd a, snd b) with
+                      | Types.Bitvector a, Types.Bitvector b ->
+                          Types.Bitvector (a + b)
+                      | _ -> failwith "boom"
+                    in
+                    match (sb1, sb2) with
+                    (* NOTE: OCaml compiler complains when these cases are merged *)
+                    | (SymBase.GlobSym | Constant), sb
+                    | sb, (SymBase.GlobSym | Constant) ->
+                        SymAddrSetLattice.update sb
+                          (WrappedIntervalsValueAbstractionBasil.eval_intrin op
+                             [ (vs1, snd a); (vs2, snd b) ]
+                             return_size)
+                          map
+                    | _, _ ->
+                        SymAddrSetLattice.update sb1 Top
+                        @@ SymAddrSetLattice.update sb2 Top map)
+                  (fst b) acc)
+              (fst a) SymAddrSetLattice.bottom,
+            rt )
+    in
+    match args with
+    | h :: b :: tl -> fst @@ List.fold_left op (op h b) tl
+    | _ -> failwith "Operators must have two operands"
+end
+
+module SVAAbstractionBasil = struct
+  include SVAAbstraction
+  module E = Lang.Expr.BasilExpr
+end
+
+module StateAbstraction = Intra_analysis.MapState (SVAAbstractionBasil)
+module Eval = Intra_analysis.EvalStmt (SVAAbstractionBasil)
+
+module Domain = struct
+  include StateAbstraction
+
+  let stack_pointer = Var.create ~scope:Local "R31_in" @@ Bitvector 64
+  let link_register = Var.create ~scope:Local "R30_in" @@ Bitvector 64
+  let frame_pointer = Var.create ~scope:Local "R29_in" @@ Bitvector 64
+
+  (* These registers are preserved over calls and are not real params, so we can ignore later *)
+  let call_preserve =
+    List.init 11 (fun i -> 19 + i) |> fun lst ->
+    31 :: lst |> List.map (fun i -> "R" ^ string_of_int i)
+
+  let init proc =
+    let open Option in
+    let name = ID.name @@ Procedure.id proc in
+    StringMap.filter (fun param _ ->
+        List.exists (fun a -> String.starts_with param ~prefix:a) call_preserve)
+    @@ Procedure.formal_in_params proc
+    |> StringMap.to_iter
+    |> Iter.filter_map (fun (_, param) ->
+        let* size =
+          match Var.typ param with
+          | Types.Boolean -> Some 1
+          | Types.Bitvector size -> Some size
+          | _ -> None
+        in
+        Some
+          ( param,
+            SymAddrSetLattice.singleton (Par { name; param })
+            @@ IntervalDomain.init @@ Bitvec.zero ~size ))
+    |> Iter.cons
+         ( stack_pointer,
+           SymAddrSetLattice.singleton (SymBase.Stack name)
+           @@ IntervalDomain.init @@ Bitvec.zero ~size:64 )
+    |> Iter.cons
+         ( link_register,
+           SymAddrSetLattice.singleton
+             (SymBase.Par { name; param = link_register })
+           @@ IntervalDomain.init @@ Bitvec.zero ~size:64 )
+    |> Iter.cons
+         ( frame_pointer,
+           SymAddrSetLattice.singleton
+             (SymBase.Par { name; param = frame_pointer })
+           @@ IntervalDomain.init @@ Bitvec.zero ~size:64 )
+    |> Iter.fold (fun m (v, d) -> update v d m) bottom
+
+  let transfer_state read stmt =
+    let stmt = Eval.stmt_eval_fwd read stmt in
+    let updates =
+      match stmt with
+      | Stmt.Instr_Assign assignments -> List.to_iter assignments
+      | Stmt.Instr_Load { lhs; addr; rhs } -> (
+          Iter.singleton
+          @@
+          match addr with
+          | Scalar -> (lhs, rhs)
+          | Addr { size } ->
+              ( lhs,
+                SymAddrSetLattice.singleton Loaded
+                @@ IntervalDomain.init @@ Bitvec.zero ~size ))
+      | Stmt.Instr_Store { lhs; addr; rhs } -> (
+          match addr with
+          | Scalar -> Iter.singleton (lhs, rhs)
+          | Addr { size } -> Iter.empty)
+      | Stmt.Instr_Call { lhs; procid }
+        when (String.equal "@malloc" @@ ID.name procid)
+             || (String.equal "@calloc" @@ ID.name procid) ->
+          let malloc =
+            Iter.filter (fun var ->
+                String.starts_with ~prefix:"R0" @@ Var.name var)
+            @@ StringMap.values lhs
+          in
+          let var = Iter.head_exn malloc in
+          let size =
+            match Var.typ var with
+            | Types.Bitvector size -> size
+            | _ -> failwith "Illegal malloc/calloc return type"
+          in
+
+          Iter.singleton
+            ( var,
+              SymAddrSetLattice.singleton
+                (SymBase.Heap { name = ID.name procid })
+              @@ IntervalDomain.init @@ Bitvec.zero ~size )
+      | Stmt.Instr_Call { lhs; args; procid } ->
+          Iter.map (fun param ->
+              let size =
+                match Var.typ param with
+                | Types.Boolean -> 1
+                | Types.Bitvector size -> size
+                | _ -> failwith "Illegal function parameter type"
+              in
+              ( param,
+                SymAddrSetLattice.singleton
+                  (Ret { name = ID.name procid; param })
+                @@ IntervalDomain.init @@ Bitvec.zero ~size ))
+          @@ StringMap.values lhs
+      | Stmt.Instr_Assert _ | Stmt.Instr_Assume _ -> Iter.empty
+      (* TODO: (From Scala code) "possibly map every live variable to top" *)
+      | Stmt.Instr_IndirectCall _ -> Iter.empty
+      | Stmt.Instr_IntrinCall _ -> Iter.empty
+    in
+    updates
+
+  let transfer dom stmt =
+    Iter.fold (fun a (k, v) -> update k v a) dom
+    @@ transfer_state (flip read dom) stmt
+end
+
+module DFGAnalysis = Dataflow_graph.AnalysisFwd (Domain)
+
+let sva (prog : Program.t) =
+  let constant_within_global_address (interval : WrappedIntervalsLattice.t)
+      (prog : Program.t) : bool =
+    let open Option in
+    (let* symbols =
+       match StringMap.find_opt ".symbols" prog.attrib with
+       | Some symbols -> Some symbols
+       | _ -> None
+     in
+     let* globs =
+       match Attrib.find_opt ".globals" (Some symbols) with
+       | Some Attrib.(`List globals) -> Some globals
+       | _ -> None
+     in
+     Some
+       (List.exists
+          (fun (global : Program.e Attrib.t) ->
+            (let* address =
+               match Attrib.find_opt ".address" (Some global) with
+               | Some Attrib.(`Bitvector bv) -> Some bv
+               | _ -> None
+             in
+             let* size =
+               match Attrib.find_opt ".size" (Some global) with
+               | Some Attrib.(`Bitvector bv) -> Some bv
+               | _ -> None
+             in
+             let end_address =
+               Bitvec.sub (Bitvec.one ~size:64) @@ Bitvec.add address size
+             in
+             let interval2 =
+               WrappedIntervalsLattice.interval address end_address
+             in
+             Some (WrappedIntervalsLattice.leq interval2 interval))
+            |> Option.get_or ~default:false)
+          globs))
+    |> Option.get_or ~default:false
+  in
+  let results =
+    IDMap.fold
+      (fun _ v acc -> DFGAnalysis.flow_insensitive v :: acc)
+      prog.procs []
+  in
+  results
+  |> List.map
+     @@ StateAbstraction.mapi (fun _ domain ->
+         SymAddrSetLattice.to_list domain
+         |> snd
+         |> List.map (fun (sym_base, value) ->
+             if
+               SymBase.equal Constant sym_base
+               && constant_within_global_address value prog
+             then (SymBase.GlobSym, value)
+             else (sym_base, value))
+         |> SymAddrSetLattice.of_list_bot)
diff --git a/lib/passes.ml b/lib/passes.ml
index 93a1f295..fa5554e4 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -122,6 +122,18 @@ module PassManager = struct
          control flow graph and prints results";
     }
 
+  let sva =
+    {
+      name = "sva";
+      apply =
+        Prog
+          (fun p ->
+            let r = Analysis.Sva.sva p in
+            List.iter (print_endline % Analysis.Sva.StateAbstraction.show) r;
+            p);
+      doc = "Runs symbolic value analysis and prints stuff out after";
+    }
+
   let demo_dfg_gamma =
     {
       name = "demo-dfg-gamma-analysis";
@@ -287,6 +299,7 @@ module PassManager = struct
       read_uninit false;
       read_uninit true;
       sssa;
+      sva;
       full_ssa;
       type_check;
       split_memory_encoding;
diff --git a/lib/transforms/may_read_uninit.ml b/lib/transforms/may_read_uninit.ml
index 4edb270d..62534cfc 100644
--- a/lib/transforms/may_read_uninit.ml
+++ b/lib/transforms/may_read_uninit.ml
@@ -148,10 +148,10 @@ let%expect_test "fold_block" =
   in
   [%expect
     {|
-    ($stack->RU, R31_in->RU, R0_in->RU, _->⊥)
-    ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, _->⊥)
-    ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥)
-    ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, _->⊥)
-    ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, _->⊥)
-    ($stack->RU, R31_in->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, R0_10->W, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, _->⊥)
+    (R31_in->RU, $stack->RU, R0_in->RU, load45_1->W, R1_4->W, $mem->RU, load46_1->W, R0_10->W, _->⊥)
     |}]
diff --git a/test/cram/dune b/test/cram/dune
index 001f4e7e..566b52eb 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -26,6 +26,7 @@
   inter_dead.il
   typefail.sexp
   typepass.sexp
+  sva.sexp
   basicssa.sexp
   roundtrip.sexp
   gammavars.sexp
diff --git a/test/cram/malloc_free.t b/test/cram/malloc_free.t
index 02022580..6ad7fdb4 100644
--- a/test/cram/malloc_free.t
+++ b/test/cram/malloc_free.t
@@ -13,10 +13,10 @@
   var $mem_encoding: MemEncoding;
   
   function  f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a }
-  function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64);
-  function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64);
-  function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool);
-  function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool);
+  function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64);
+  function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64);
+  function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool);
+  function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool);
   function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) {
     (((((((#memory[bvadd_bv64(#index, 7bv64)]
            ++
@@ -34,38 +34,38 @@
      ++
      #memory[bvadd_bv64(#index, 0bv64)]): bv64
   }
-  function {:extern } {:inline } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
+  function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
     addr
   }
-  function {:extern } {:inline } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) {
+  function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) {
     mem_encoding->addr_is_heap[addr]
   }
-  function {:extern } {:inline } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
+  function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
     bvand_bv64(addr, 4294967295bv64)
   }
-  function {:extern } {:inline } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
+  function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
     bvand_bv64(alloc, 18446744069414584320bv64)
   }
-  function {:extern } {:inline } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) {
+  function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) {
     mem_encoding->alloc_live[alloc]
   }
-  function {:extern } {:inline } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) {
+  function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) {
     mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live])
   }
-  function {:extern } {:inline } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
+  function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
     mem_encoding->alloc_size[alloc]
   }
-  function {:extern } {:inline } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) {
+  function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) {
     mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size])
   }
-  function {:extern } {:inline } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) {
+  function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) {
     me_alloc_size_update(
       me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2),
       me_addr_alloc(mem_encoding, addr),
       size
     )
   }
-  function {:extern } {:inline } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
+  function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
     ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live(
           mem_encoding,
           me_addr_alloc(mem_encoding, addr)
@@ -74,7 +74,7 @@
        size
      ))
   }
-  function {:extern } {:inline } me_init_encoding(mem_encoding: MemEncoding) returns (bool) {
+  function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) {
     (((forall 
        i: bv64 :: 
        {me_addr_is_heap(mem_encoding, i)} 
@@ -86,7 +86,7 @@
       {me_alloc_live(mem_encoding, i)} 
       ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2))))
   }
-  function {:extern } {:inline } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
+  function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
     (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live(
          mem_encoding,
          me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr))
@@ -99,7 +99,7 @@
       )))
   }
   datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)}
-  function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) {
+  function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) {
     #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64(
       #index,
       2bv64
@@ -111,10 +111,28 @@
       6bv64
     ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]]
   }
-  function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) {
+  function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) {
     #memory[#index := #value[8:0]]
   }
   
+  procedure p$free();
+    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
+    ensures ($mem_encoding == me_alloc_live_update(
+       old($mem_encoding),
+       me_addr_alloc(old($mem_encoding), $R0),
+       2bv2
+     ));
+    requires me_addr_is_heap($mem_encoding, $R0);
+    requires (0bv64 == me_addr_offset($mem_encoding, $R0));
+    requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2);
+  
+  procedure p$malloc();
+    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
+    ensures me_can_allocate(old($mem_encoding), $R0, old($R0));
+    ensures (me_addr_offset($mem_encoding, $R0) == 0bv64);
+    ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0);
+    ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0)));
+  
   procedure p$main();
     modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
     requires me_init_encoding($mem_encoding);
@@ -190,24 +208,6 @@
       assert true;
       return;
   }
-  
-  procedure p$malloc();
-    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
-    ensures me_can_allocate(old($mem_encoding), $R0, old($R0));
-    ensures (me_addr_offset($mem_encoding, $R0) == 0bv64);
-    ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0);
-    ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0)));
-  
-  procedure p$free();
-    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
-    ensures ($mem_encoding == me_alloc_live_update(
-       old($mem_encoding),
-       me_addr_alloc(old($mem_encoding), $R0),
-       2bv2
-     ));
-    requires me_addr_is_heap($mem_encoding, $R0);
-    requires (0bv64 == me_addr_offset($mem_encoding, $R0));
-    requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2);
 
   $ boogie ./good.bpl
   
@@ -226,10 +226,10 @@
   var $mem_encoding: MemEncoding;
   
   function  f$magic(a: [bv64]bv8, b: [bv64]bv8) returns ([bv64]bv8) { a }
-  function {:bvbuiltin "bvadd"} {:extern } bvadd_bv64(bv64, bv64) returns (bv64);
-  function {:bvbuiltin "bvand"} {:extern } bvand_bv64(bv64, bv64) returns (bv64);
-  function {:bvbuiltin "bvule"} {:extern } bvule_bv64_bv64_bool(bv64, bv64) returns (bool);
-  function {:bvbuiltin "bvult"} {:extern } bvult_bv64_bv64_bool(bv64, bv64) returns (bool);
+  function {:extern } {:bvbuiltin "bvadd"} bvadd_bv64(bv64, bv64) returns (bv64);
+  function {:extern } {:bvbuiltin "bvand"} bvand_bv64(bv64, bv64) returns (bv64);
+  function {:extern } {:bvbuiltin "bvule"} bvule_bv64_bv64_bool(bv64, bv64) returns (bool);
+  function {:extern } {:bvbuiltin "bvult"} bvult_bv64_bv64_bool(bv64, bv64) returns (bool);
   function {:extern } load64_le(#memory: [bv64]bv8, #index: bv64) returns (bv64) {
     (((((((#memory[bvadd_bv64(#index, 7bv64)]
            ++
@@ -247,38 +247,38 @@
      ++
      #memory[bvadd_bv64(#index, 0bv64)]): bv64
   }
-  function {:extern } {:inline } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
+  function {:inline } {:extern } me_addr_alloc(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
     addr
   }
-  function {:extern } {:inline } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) {
+  function {:inline } {:extern } me_addr_is_heap(mem_encoding: MemEncoding, addr: bv64) returns (bool) {
     mem_encoding->addr_is_heap[addr]
   }
-  function {:extern } {:inline } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
+  function {:inline } {:extern } me_addr_offset(mem_encoding: MemEncoding, addr: bv64) returns (bv64) {
     bvand_bv64(addr, 4294967295bv64)
   }
-  function {:extern } {:inline } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
+  function {:inline } {:extern } me_alloc_base(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
     bvand_bv64(alloc, 18446744069414584320bv64)
   }
-  function {:extern } {:inline } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) {
+  function {:inline } {:extern } me_alloc_live(mem_encoding: MemEncoding, alloc: bv64) returns (bv2) {
     mem_encoding->alloc_live[alloc]
   }
-  function {:extern } {:inline } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) {
+  function {:inline } {:extern } me_alloc_live_update(mem_encoding: MemEncoding, alloc: bv64, live: bv2) returns (MemEncoding) {
     mem_encoding->(alloc_live := mem_encoding->alloc_live[alloc := live])
   }
-  function {:extern } {:inline } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
+  function {:inline } {:extern } me_alloc_size(mem_encoding: MemEncoding, alloc: bv64) returns (bv64) {
     mem_encoding->alloc_size[alloc]
   }
-  function {:extern } {:inline } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) {
+  function {:inline } {:extern } me_alloc_size_update(mem_encoding: MemEncoding, alloc: bv64, size: bv64) returns (MemEncoding) {
     mem_encoding->(alloc_size := mem_encoding->alloc_size[alloc := size])
   }
-  function {:extern } {:inline } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) {
+  function {:inline } {:extern } me_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (MemEncoding) {
     me_alloc_size_update(
       me_alloc_live_update(mem_encoding, me_addr_alloc(mem_encoding, addr), 1bv2),
       me_addr_alloc(mem_encoding, addr),
       size
     )
   }
-  function {:extern } {:inline } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
+  function {:inline } {:extern } me_can_allocate(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
     ((((me_addr_is_heap(mem_encoding, addr)&&(me_alloc_base(mem_encoding, addr) == addr))&&(me_alloc_live(
           mem_encoding,
           me_addr_alloc(mem_encoding, addr)
@@ -287,7 +287,7 @@
        size
      ))
   }
-  function {:extern } {:inline } me_init_encoding(mem_encoding: MemEncoding) returns (bool) {
+  function {:inline } {:extern } me_init_encoding(mem_encoding: MemEncoding) returns (bool) {
     (((forall 
        i: bv64 :: 
        {me_addr_is_heap(mem_encoding, i)} 
@@ -299,7 +299,7 @@
       {me_alloc_live(mem_encoding, i)} 
       ((!(me_addr_is_heap(mem_encoding, i))) ==> (me_alloc_live(mem_encoding, i) == 2bv2))))
   }
-  function {:extern } {:inline } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
+  function {:inline } {:extern } me_valid_access(mem_encoding: MemEncoding, addr: bv64, size: bv64) returns (bool) {
     (me_addr_is_heap(mem_encoding, addr) ==> ((me_alloc_live(
          mem_encoding,
          me_alloc_base(mem_encoding, me_addr_alloc(mem_encoding, addr))
@@ -312,7 +312,7 @@
       )))
   }
   datatype MemEncoding {MemEncoding(alloc_live: [bv64]bv2, alloc_size: [bv64]bv64, addr_is_heap: [bv64]bool)}
-  function {:define } {:extern } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) {
+  function {:extern } {:define } store64_le(#memory: [bv64]bv8, #index: bv64, #value: bv64) returns ([bv64]bv8) {
     #memory[#index := #value[8:0]][bvadd_bv64(#index, 1bv64) := #value[16:8]][bvadd_bv64(
       #index,
       2bv64
@@ -324,10 +324,28 @@
       6bv64
     ) := #value[56:48]][bvadd_bv64(#index, 7bv64) := #value[64:56]]
   }
-  function {:define } {:extern } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) {
+  function {:extern } {:define } store8_le(#memory: [bv64]bv8, #index: bv64, #value: bv8) returns ([bv64]bv8) {
     #memory[#index := #value[8:0]]
   }
   
+  procedure p$free();
+    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
+    ensures ($mem_encoding == me_alloc_live_update(
+       old($mem_encoding),
+       me_addr_alloc(old($mem_encoding), $R0),
+       2bv2
+     ));
+    requires me_addr_is_heap($mem_encoding, $R0);
+    requires (0bv64 == me_addr_offset($mem_encoding, $R0));
+    requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2);
+  
+  procedure p$malloc();
+    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
+    ensures me_can_allocate(old($mem_encoding), $R0, old($R0));
+    ensures (me_addr_offset($mem_encoding, $R0) == 0bv64);
+    ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0);
+    ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0)));
+  
   procedure p$main();
     modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
     requires me_init_encoding($mem_encoding);
@@ -403,28 +421,10 @@
       assert true;
       return;
   }
-  
-  procedure p$malloc();
-    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
-    ensures me_can_allocate(old($mem_encoding), $R0, old($R0));
-    ensures (me_addr_offset($mem_encoding, $R0) == 0bv64);
-    ensures (me_alloc_base($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == $R0);
-    ensures ($mem_encoding == me_allocate(old($mem_encoding), $R0, old($R0)));
-  
-  procedure p$free();
-    modifies $mem_encoding, $mem, $stack, $R0, $R1, $R16, $R17, $R29, $R30, $R31;
-    ensures ($mem_encoding == me_alloc_live_update(
-       old($mem_encoding),
-       me_addr_alloc(old($mem_encoding), $R0),
-       2bv2
-     ));
-    requires me_addr_is_heap($mem_encoding, $R0);
-    requires (0bv64 == me_addr_offset($mem_encoding, $R0));
-    requires (me_alloc_live($mem_encoding, me_addr_alloc($mem_encoding, $R0)) == 1bv2);
 
   $ boogie ./bad.bpl
-  ./bad.bpl(158,5): Error: this assertion could not be proved
+  ./bad.bpl(176,5): Error: this assertion could not be proved
   Execution trace:
-      ./bad.bpl(128,3): b#main_entry
+      ./bad.bpl(146,3): b#main_entry
   
   Boogie program verifier finished with 0 verified, 1 error
diff --git a/test/cram/sva.sexp b/test/cram/sva.sexp
new file mode 100644
index 00000000..5c749b79
--- /dev/null
+++ b/test/cram/sva.sexp
@@ -0,0 +1,2 @@
+(load-il "../../examples/irreducible_loop_1.il")
+(run-transforms "sva")
diff --git a/test/cram/sva.t b/test/cram/sva.t
new file mode 100644
index 00000000..df3cea14
--- /dev/null
+++ b/test/cram/sva.t
@@ -0,0 +1,3 @@
+  $ bincaml script ./sva.sexp
+  (R31_in->(Stack(@puts_1584)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@puts_1584_{id=1 ; data=R30_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@puts_1584_{id=2 ; data=R29_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), _->⊥)
+  (R31_in->(Stack(@main_1876)->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R30_in->(Par(@main_1876_{id=1 ; data=R30_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), R29_in->(Par(@main_1876_{id=2 ; data=R29_in:bv64})->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $CF->(Loaded->⊤, _->⊥), $NF->(Loaded->⊤, _->⊥), $R0->(Constant->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $R1->(Loaded->⊤, _->⊥), $R29->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $R30->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), $VF->(Loaded->⊤, _->⊥), $ZF->(Loaded->⊤, _->⊥), load18->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), #5->(Loaded->⊤, _->⊥), load19->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), load21->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load22->(Loaded->⟦0x0:bv64, 0x0:bv64⟧, _->⊥), load20->(Loaded->⟦0x0:bv32, 0x0:bv32⟧, _->⊥), #6->(Loaded->⊤, _->⊥), _->⊥)
diff --git a/test/lang/test_value_soundness.ml b/test/lang/test_value_soundness.ml
index 88d7e0aa..67064ca3 100644
--- a/test/lang/test_value_soundness.ml
+++ b/test/lang/test_value_soundness.ml
@@ -108,6 +108,8 @@ module TestTnumWintReducedDom =
     (Analysis.Tnum_wint_reduced_product
      .TnumWintReducedProductValueAbstractionBasil)
 
+module TestSVADom = ValueAbstractionSoundness (Analysis.Sva.SVAAbstractionBasil)
+
 let _ =
   Alcotest.run "value domain abstract eval soundness"
     [