diff --git a/srk/src/arraylift.ml b/srk/src/arraylift.ml
new file mode 100644
index 00000000..8a6be72d
--- /dev/null
+++ b/srk/src/arraylift.ml
@@ -0,0 +1,178 @@
+open Syntax
+open Iteration
+
+(* bubble_sym is an internal helper function for lowering formulas in the skolem array fragment
+    to quantified numerical formulas. 
+    [bubble_sym srk form] returns a triple of the form (syms, fr, form') in which:
+        - form ==> \exists syms. \forall fr.  form' 
+        - form' contains no array terms
+*) 
+let bubble_sym (srk : 'a context) (form : 'a formula) : (symbol list * (symbol) * 'a formula) = 
+  (* rep_map : arr_var -> (index_term -> var) *)
+  let (rep_map : (symbol, ('a, Syntax.typ_arith, symbol) Expr.HT.t) Hashtbl.t) = Hashtbl.create 16 in 
+  let leading_existentials = ref [] in 
+  let forall_symbol = mk_symbol srk `TyInt ~name:"forall_index" in
+
+  let get_or_create_replacement array_symbol index_term = 
+    let replacement_map = Hashtbl.find rep_map array_symbol in 
+    match Expr.HT.mem replacement_map index_term with 
+      | true -> mk_const srk (Expr.HT.find replacement_map index_term)
+      | false -> (
+        let name = Format.asprintf "rep_%a_%a"
+          (pp_symbol srk) array_symbol
+          (ArithTerm.pp srk) index_term
+        in
+        let replacement = mk_symbol srk `TyInt ~name in
+        Expr.HT.add replacement_map index_term replacement;
+        leading_existentials := replacement :: !leading_existentials; (* Update the mutable list *)
+        mk_const srk replacement
+      )
+  in
+
+  (* All variables are turned into symbols as we recurse across the formula.
+    env maps from variable indices to symbols. 
+    qo is the index of the forall variable. 
+    Variables with index > qo are existentially quantified outside the forall.
+    Note that replace functions only get run after we have found the forall.
+  *)
+  (* [replace_access arr i env qo] returns a substitute term for arr[i] *)
+  let rec replace_access (arr : 'a arr_term) (index : 'a arith_term) (env : (symbol Env.t)) (qo : int) : 'a arith_term = 
+    match ArrTerm.destruct srk arr with 
+    | `Var (i, _) -> 
+        if (i <= qo) then (failwith "Array term is not quantified inside the forall") else ( 
+          let array_symbol = Env.find env (i - qo) in 
+          match ArithTerm.destruct srk index with 
+            | `Var (indi, _) -> 
+              ((if indi < qo then failwith "Array index variable is bound but should be free");
+              let index_symbol = Env.find env (indi - qo) in 
+              get_or_create_replacement array_symbol (mk_const srk index_symbol))
+            | `App (_, []) | `Real _ -> 
+              get_or_create_replacement array_symbol index
+            | _ -> failwith "Array index should be a variable, symbol, or constant"
+        ) 
+    | `App (_, _) -> failwith "Array applications not supported"
+    | `Ite (f, l, r) -> mk_ite srk f (replace_access l index env qo) (replace_access r index env qo)
+    | `Store (a, store_index, value) ->
+      let ae = replace_access a index env qo in 
+      mk_ite srk (mk_eq srk store_index index) value ae 
+    in
+  let replace env f = 
+    fold_rewrite srk 
+    ~down:(fun e qo -> match destruct srk e with | `Var (i, t) -> if i >= qo && t != `TyArr then (mk_const srk (Env.find env (i - qo))) else e | _ -> e)
+    ~up:(fun e qo -> match destruct srk e with | `Select (arr, index) -> replace_access arr index env qo | _ -> e)
+    ~combine:(fun e qo -> match destruct srk e with | `Quantify (`Exists, _, _, _) -> qo + 1 | `Quantify (`Forall, _, _, _) -> failwith "Nested foralls" | _ -> qo)
+    0 f
+  in
+
+  (* go contains the core "bubbling" logic of this algorithm: 
+    we process leading existentials, skolemizing them and adding them to env.
+    Once we reach a forall, we stop processing existentials and switch over to replace functions
+    to eliminate array terms.
+  *)
+  (* [go form env] considers the formula \exists env . form
+     and returns form' where
+        - form' contains no array terms
+        - \exists env . form ==> \exists syms. \forall forall_sym. form' 
+         *)
+  let rec go (f : 'a formula) (env : (symbol Env.t)): ('a formula) = 
+     match Formula.destruct srk f with 
+    | `Quantify (`Exists, name, typ, body) -> 
+      let new_sym = mk_symbol srk ~name (typ :> typ) in 
+      (if typ = `TyArr then (
+        Hashtbl.add rep_map new_sym (Expr.HT.create 16);
+        let name = Format.asprintf "rep_%a_univ"
+          (pp_symbol srk) new_sym
+        in
+        Expr.HT.add (Hashtbl.find rep_map new_sym) (mk_const srk forall_symbol) (mk_symbol srk `TyInt ~name);
+        let body' = go body (Env.push new_sym env) in 
+        let ai = get_or_create_replacement new_sym (mk_const srk forall_symbol) in 
+        let fc = BatEnum.fold (fun acc (index, replacement) ->
+            (mk_if srk (mk_eq srk index (mk_const srk forall_symbol)) (mk_eq srk (mk_const srk replacement) ai)) :: acc
+          ) [] (Expr.HT.enum (Hashtbl.find rep_map new_sym)) in 
+        let body'' = mk_exists_const srk (Expr.HT.find (Hashtbl.find rep_map new_sym) (mk_const srk forall_symbol)) 
+          (mk_and srk ((body') :: fc))
+      in 
+        body''
+      ) else (
+        leading_existentials := new_sym :: !leading_existentials; 
+        go body (Env.push new_sym env) 
+        ))
+    | `Quantify (`Forall, _, typ, body) -> 
+      assert (typ = `TyInt);
+      replace (Env.push forall_symbol env) body
+    | `And ls -> 
+      let (parts) = List.fold_left (fun parts f -> 
+         go f env :: parts
+      ) [] ls in 
+      (mk_and srk parts)
+    | `Or ls ->
+      let branch_var = mk_symbol srk ~name:"branch" `TyInt in 
+      (leading_existentials := branch_var :: !leading_existentials);
+      let (parts) = List.fold_left (fun parts f -> 
+          go f env :: parts  
+        ) [] ls in 
+      let parts = List.mapi (fun i part -> mk_and srk [part; mk_eq srk (mk_const srk branch_var) (mk_int srk i)]) parts in 
+      (mk_or srk parts)
+    | `Atom _ | `Proposition _ -> 
+      (* At this point, we want to run replace but cannot because we haven't yet seen a forall.
+        We use the equivalence f <=> \forall d. f where f is d-free
+        to map back to the forall case.
+      *)
+      let f' = substitute srk (fun (i, typ) -> mk_var srk (i + 1) typ) f in 
+      go (mk_forall srk `TyInt f') env 
+    | `Tru | `Fls -> (f)
+    | `Ite (f, l, r) -> 
+      let f' = mk_or srk [mk_and srk [f ; l]; mk_and srk [mk_not srk f; r]] in 
+      let f' = rewrite srk ~down:(pos_rewriter srk) f' in 
+      go f' env
+    | `Not _ -> failwith "Not is not supported in Skolem fragment"
+  in
+  let retf = go form Syntax.Env.empty in 
+  (!leading_existentials, forall_symbol, retf)
+
+
+
+(* array_exponentiate lifts exponentiation operator e to work over formulas with arrays. *)
+let array_exponentiate (srk : 'a context) (e : 'a exp_op) : ('a TransitionFormula.t -> 'a Syntax.arith_term -> 'a Syntax.formula) = 
+  fun (tf : 'a TransitionFormula.t) (k : 'a arith_term) ->
+    let f = TransitionFormula.formula tf in 
+    let array_symbols = List.filter (fun (s, s') -> typ_symbol srk s = `TyArr && typ_symbol srk s' = `TyArr) (TransitionFormula.symbols tf) in 
+    let zs = List.fold_left (fun acc (s, s') -> (s, mk_symbol srk `TyInt) :: (s', mk_symbol srk `TyInt) :: acc) [] array_symbols in 
+    let j = mk_symbol srk ~name:"j" `TyInt in 
+    let j' = mk_symbol srk ~name:"j'" `TyInt in 
+    let projected_formula = mk_and srk (f :: (mk_eq srk (mk_const srk j) (mk_const srk j')) :: (List.map (fun (a, z) -> mk_eq srk (mk_select srk (mk_const srk a) (mk_const srk j)) (mk_const srk z)) zs)) in 
+    let projected_formula = Symbol.Set.fold (fun s acc->
+      if typ_symbol srk s = `TyArr then mk_exists_const srk s acc else acc
+      ) (Syntax.symbols projected_formula) projected_formula in 
+
+    let existentials, forall, skol = bubble_sym srk projected_formula in
+    let with_universal = mk_forall_const srk forall skol in
+      
+    let with_everything = List.fold_left (fun acc s -> mk_exists_const srk s acc) with_universal existentials in 
+
+    let eliminated = SrkZ3.qe srk with_everything in 
+
+    let tf'_symbols = (j, j') :: List.map (fun (s, s') -> if (typ_symbol srk s = `TyArr) then (((List.find (fun (sym, _) -> sym = s') zs) |> snd), ((List.find (fun (sym, _) -> sym = s') zs) |> snd)) else (s, s')) (TransitionFormula.symbols tf) in 
+    let tf' = TransitionFormula.make ~exists:(fun sym -> (not (List.exists (fun (s, s') -> s = sym || s' = sym) tf'_symbols)) && TransitionFormula.exists tf sym) eliminated tf'_symbols in 
+    let solver' = Solver.make srk tf' in
+
+    let exponentiated = e solver' k in 
+
+    let ret = substitute_sym srk (fun s ->
+      match List.find_opt (fun (_, z) -> s = z) zs with 
+        | Some (a, _) -> mk_select srk (mk_const srk a) (mk_const srk j)
+        | None -> mk_const srk s
+      ) exponentiated in 
+    let ret = substitute_sym srk (fun s -> 
+        if s = j' then mk_const srk j else mk_const srk s) ret in 
+    
+    mk_forall_const srk j ret 
+
+
+  (* [map_elim ctx f] takes a formula in the array skolem fragment and returns an equivalent formula over numerical variables. *)
+  let map_elim (srk : 'a context) (f : 'a formula) : 'a formula = 
+    let syms, forall, f = bubble_sym srk f in 
+    let f = mk_forall_const srk forall f in
+    
+    let f = List.fold_left (fun acc sym -> mk_exists_const srk sym acc) f syms in 
+    f
diff --git a/srk/src/arraylift.mli b/srk/src/arraylift.mli
new file mode 100644
index 00000000..b1815c41
--- /dev/null
+++ b/srk/src/arraylift.mli
@@ -0,0 +1,17 @@
+open Syntax
+
+
+(** [array_exponentiate ctx exp_op] takes an exponentiation operation [exp_op]
+  , and returns an exponentiation operator which numerically abstracts the array variables
+  in the formula, applies exp_op, then reintroduces the array variables 
+*)
+val array_exponentiate :
+  'a context ->
+  'a Iteration.exp_op ->
+  ('a TransitionFormula.t -> 'a arith_term -> 'a formula)
+
+
+(** [map_elim ctx formula] computes an equisatisfiable formula to [formula]
+  in which all array variables are replaced with numerical abstractions.
+*)
+val map_elim : 'a context -> 'a formula -> 'a formula
\ No newline at end of file
diff --git a/srk/src/syntax.ml b/srk/src/syntax.ml
index 2f3d89a9..a0366c96 100644
--- a/srk/src/syntax.ml
+++ b/srk/src/syntax.ml
@@ -554,6 +554,7 @@ let destruct _srk sexpr =
   | Node (App func, args, _) -> `App (func, args)
   | Node (Var (v, `TyReal), [], _) -> `Var (v, `TyReal)
   | Node (Var (v, `TyInt), [], _) -> `Var (v, `TyInt)
+  | Node (Var (v, `TyArr), [], _) -> `Var (v, `TyArr)
   | Node (Var (v, `TyBool), [], _) -> `Proposition (`Var v)
   | Node (Add, sum, _) -> `Add sum
   | Node (Mul, product, _) -> `Mul product
@@ -1608,6 +1609,15 @@ let rec rewrite srk ?down:(down=fun x -> x) ?up:(up=fun x -> x) sexpr =
   let (Node (label, children, _)) = (down sexpr).obj in
   up (srk.mk label (List.map (rewrite srk ~down ~up) children))
 
+let fold_rewrite srk ?down:(down=fun x _ ->x) ?up:(up=fun x _ -> x) ?combine:(combine=fun _ a -> a) acc sexpr = 
+  let rec go acc e = 
+    let d = (down e acc) in 
+    let (Node (label, children, _)) = d.obj in
+    let acc' = combine d acc in 
+    up (srk.mk label (List.map (go acc') children)) acc 
+  in
+  go acc sexpr
+
 let mk_compare op =
   match op with
   | `Eq -> mk_eq
diff --git a/srk/src/syntax.mli b/srk/src/syntax.mli
index 386e3d9f..9a4d609d 100644
--- a/srk/src/syntax.mli
+++ b/srk/src/syntax.mli
@@ -227,6 +227,14 @@ type ('a, 'b) rewriter = ('a, 'b) expr -> ('a, 'b) expr
 val rewrite : 'a context -> ?down:(('a, 'b) rewriter) -> ?up:(('a, 'b) rewriter) ->
   ('a, 'typ) expr -> ('a, 'typ) expr
 
+(** Rewrite an expression while folding over the tree. The {i down} rewriter is applied to each
+    expression goign down the expression tree and the {i up} rewriter is
+    applied to each expression going up the tree. The accumulator is updated at each node after
+    the down rewrite.
+*)
+val fold_rewrite: 'a context -> ?down:(('a, 'b) expr -> 'c -> ('a, 'b) expr) -> ?up:(('a, 'b) expr -> 'c -> ('a, 'b) expr) -> 
+  ?combine:(('a, 'typ) expr -> 'c -> 'c) -> 'c -> ('a, 'typ) expr -> ('a, 'typ) expr
+
 (** Convert to negation normal form ({i down} pass). *)
 val nnf_rewriter : 'a context -> ('a, typ_fo) rewriter
 
diff --git a/srk/src/transitionFormula.ml b/srk/src/transitionFormula.ml
index e58fb302..8e8dc142 100644
--- a/srk/src/transitionFormula.ml
+++ b/srk/src/transitionFormula.ml
@@ -7,6 +7,14 @@ type 'a t =
 
 include Log.Make(struct let name = "srk.transitionFormula" end)
 
+let pp srk formatter tf =
+  let open Format in
+  let pp_symbol_pair formatter (s, s') =
+    fprintf formatter "%s -> %s" (show_symbol srk s) (show_symbol srk s')
+  in
+  fprintf formatter "TransitionFormula(@[<v 2>\n  symbols = [@[<hov>%a@]],@ formula = %a@])"
+    (pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt ",@ ") pp_symbol_pair) tf.symbols
+    (Formula.pp srk) tf.formula
 
 let identity srk symbols =
   let formula = 
diff --git a/srk/src/transitionFormula.mli b/srk/src/transitionFormula.mli
index 0450c3ee..ecbba29f 100644
--- a/srk/src/transitionFormula.mli
+++ b/srk/src/transitionFormula.mli
@@ -13,6 +13,7 @@ open Syntax
    as existentially quantified variables). *)
 type 'a t
 
+val show : 'a context -> 'a t -> string
 (** Construct a transition formula.  The [exists] predicate identifies
    Skolem constants ([exists s] fails if [s] is a Skolem constant),
    with the default behavior that no symbols are Skolem consntas; the
diff --git a/srk/test/test_arraylift.ml b/srk/test/test_arraylift.ml
new file mode 100644
index 00000000..0b42a183
--- /dev/null
+++ b/srk/test/test_arraylift.ml
@@ -0,0 +1,232 @@
+open Srk
+open OUnit2
+open Syntax
+open Iteration
+open Arraylift
+open Test_pervasives
+
+
+let noop_eop : 'a exp_op = 
+  let f solver _ = Solver.get_formula solver in 
+  f
+
+let ksym = Ctx.mk_symbol ~name:"k" `TyInt
+let ksym' = Ctx.mk_symbol ~name:"k'" `TyInt
+let nsym = Ctx.mk_symbol ~name:"n" `TyInt
+let nsym' = Ctx.mk_symbol ~name:"n'" `TyInt
+let asym = Ctx.mk_symbol ~name:"a" `TyArr
+let asym' = Ctx.mk_symbol ~name:"a'" `TyArr
+let bsym = Ctx.mk_symbol ~name:"b" `TyArr
+let bsym' = Ctx.mk_symbol ~name:"b'" `TyArr
+let dsym = Ctx.mk_symbol ~name:"d" `TyArr
+let dsym' = Ctx.mk_symbol ~name:"d'" `TyArr
+
+let k : 'a arith_term = Ctx.mk_const ksym
+let k' : 'a arith_term = Ctx.mk_const ksym'
+let n : 'a arith_term = Ctx.mk_const nsym
+let n' : 'a arith_term = Ctx.mk_const nsym'
+let a : 'a arr_term = Ctx.mk_const asym
+let a' : 'a arr_term = Ctx.mk_const asym'
+let b : 'a arr_term = Ctx.mk_const bsym
+let b' : 'a arr_term = Ctx.mk_const bsym'
+let d : 'a arr_term = Ctx.mk_const dsym
+let d' : 'a arr_term = Ctx.mk_const dsym'
+
+let strlen_test _ctxt = 
+  let open Infix in
+  let tf = TransitionFormula.make 
+    (forall ~name:"i" `TyInt 
+    (k' = k + (int 1) && n' = n && a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] && b'.%[(var 0 `TyInt)] = b.%[(var 0 `TyInt)]
+     && ((k = (var 0 `TyInt) && d'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] + b.%[(var 0 `TyInt)]) || 
+      (((k < (var 0 `TyInt)) || ((var 0 `TyInt) < k)) && d'.%[(var 0 `TyInt)] = d.%[(var 0 `TyInt)])
+    ))) 
+    [(asym, asym'); (bsym, bsym'); (ksym, ksym'); (dsym, dsym'); (nsym, nsym')] in 
+  let aeop = array_exponentiate srk noop_eop in
+
+  let eop_result = aeop tf k in
+
+  let expected = TransitionFormula.formula tf in 
+  assert_equiv_formula (expected) (eop_result)
+
+let subproblem _ctx = 
+  let open Infix in
+  let tf = TransitionFormula.make 
+    (forall ~name:"i" `TyInt 
+    (k' = k + (int 1)
+     && ((k = (var 0 `TyInt) && d'.%[(var 0 `TyInt)] = (int 1)) || 
+      (((k < (var 0 `TyInt)) || ((var 0 `TyInt) < k)) && d'.%[(var 0 `TyInt)] = (int 0))
+    ))) 
+    [(ksym, ksym'); (dsym, dsym')] in 
+  let aeop = array_exponentiate srk noop_eop in
+
+  let eop_result = aeop tf k in
+
+  let expected = TransitionFormula.formula tf in 
+  assert_equiv_formula (expected) (eop_result)
+
+
+let basic_test _ctx = 
+  let open Infix in 
+  let tf = TransitionFormula.make 
+      (forall ~name:"i" `TyInt 
+        (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] + (int 1))
+      ) [(asym, asym')] in
+  let aeop = array_exponentiate srk noop_eop in
+  let eop_result = aeop tf k in
+  let expected = (TransitionFormula.formula tf) in               
+  assert_equiv_formula ( expected) ( eop_result)
+
+let unsat_formula _ctx = 
+  let open Infix in 
+  let f = (forall ~name:"i" `TyInt 
+        (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] + (int 1) &&
+         a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] + (int 2)
+        )) in 
+  let f = mk_exists_const srk asym f in 
+  let f = mk_exists_const srk asym' f in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) f in
+  let equi_sat = Arraylift.map_elim srk pos in
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+
+let formula_test _ctx = 
+  let open Infix in 
+  let loop_summary = ((forall ~name:"j" `TyInt
+    (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] && 
+      b'.%[(var 0 `TyInt)] = b.%[(var 0 `TyInt)] &&
+      (((int 0) <= (var 0 `TyInt) && ((var 0 `TyInt) < k') && d'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] + b.%[(var 0 `TyInt)]) || 
+      ((var 0 `TyInt) < (int 0) && (k' <= (var 0 `TyInt)) && d'.%[(var 0 `TyInt)] = d.%[(var 0 `TyInt)]))
+  )) && 
+  (exists ~name:"i" `TyInt (n' = (var 0 `TyInt) && (int 0) <= (var 0 `TyInt) && (var 0 `TyInt) < k'))) in 
+  let verification_condition = d'.%[n'] = a.%[n'] + b.%[n'] in 
+  
+  let combined = mk_and srk [loop_summary; !verification_condition] in 
+  let quantified = List.fold_left 
+    (fun acc s -> mk_exists_const srk s acc) combined [asym; asym'; bsym; bsym'; dsym; dsym'; ksym; ksym'; nsym; nsym'] in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) quantified in 
+  let equi_sat = Arraylift.map_elim srk pos in 
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+
+let existential_index_test _ctx = 
+  let open Infix in 
+  let loop_summary = ((forall ~name:"j" `TyInt
+    (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] && 
+      b'.%[(var 0 `TyInt)] = b.%[(var 0 `TyInt)] &&
+      (((int 0) <= (var 0 `TyInt) && ((var 0 `TyInt) < k') && d'.%[(var 0 `TyInt)] = (var 0 `TyInt)) || 
+      ((var 0 `TyInt) < (int 0) && (k' <= (var 0 `TyInt)) && d'.%[(var 0 `TyInt)] = d.%[(var 0 `TyInt)]))
+  )) && 
+  (exists ~name:"i" `TyInt (n' = (var 0 `TyInt) && (int 0) <= (var 0 `TyInt) && (var 0 `TyInt) < k'))) in 
+  let error_condition = (exists ~name:"q" `TyInt ((int 0) <= (var 0 `TyInt) && (var 0 `TyInt) < k' && d'.%[(var 0 `TyInt)] = k' + (int 1))) in 
+  
+  let combined = mk_and srk [loop_summary; error_condition] in 
+  let quantified = List.fold_left 
+    (fun acc s -> mk_exists_const srk s acc) combined [asym; asym'; bsym; bsym'; dsym; dsym'; ksym; ksym'; nsym; nsym'] in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) quantified in 
+  let equi_sat = Arraylift.map_elim srk pos in 
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+
+let constant_index_test _ctx = 
+  let open Infix in 
+  let loop_summary = ((forall ~name:"j" `TyInt
+    (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)] && 
+      b'.%[(var 0 `TyInt)] = b.%[(var 0 `TyInt)] &&
+      (((int 0) <= (var 0 `TyInt) && ((var 0 `TyInt) < k') && d'.%[(var 0 `TyInt)] = (var 0 `TyInt)) || 
+      ((var 0 `TyInt) < (int 0) && (k' <= (var 0 `TyInt)) && d'.%[(var 0 `TyInt)] = d.%[(var 0 `TyInt)]))
+  )) && 
+  (exists ~name:"i" `TyInt (n' = (var 0 `TyInt) && (int 0) <= (var 0 `TyInt) && (var 0 `TyInt) < k'))) in 
+  let error_condition = ((k' < (int 10)) && !(d'.%[(int 10)] = d.%[(int 10)])) in 
+  
+  let combined = mk_and srk [loop_summary; error_condition] in 
+  let quantified = List.fold_left 
+    (fun acc s -> mk_exists_const srk s acc) combined [asym; asym'; bsym; bsym'; dsym; dsym'; ksym; ksym'; nsym; nsym'] in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) quantified in 
+  let equi_sat = Arraylift.map_elim srk pos in 
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+
+
+  let simple_store_test _ctx = 
+    let open Infix in 
+    let loop_summary = 
+    (forall ~name:"i" `TyInt 
+    (b'.%[(var 0 `TyInt)] = (a.%[(int 7)]<- (int 42)).%[var 0 `TyInt]
+    )) 
+     in
+    let error_condition = (forall ~name:"i" `TyInt 
+    (!(b'.%[(var 0 `TyInt)] = (int 42))
+    )) in 
+     let combined = mk_and srk [loop_summary; error_condition] in 
+    let quantified = List.fold_left 
+      (fun acc s -> mk_exists_const srk s acc) combined [asym; bsym';] in 
+    let pos = rewrite srk ~down:(pos_rewriter srk) quantified in 
+    let equi_sat = Arraylift.map_elim srk pos in 
+
+    match Quantifier.simsat srk equi_sat with
+    | `Sat -> failwith "Unexpected sat result"
+    | `Unsat -> ()
+    | `Unknown -> failwith "Unknown result from sat solver"
+
+
+
+
+  let store_test _ctx = 
+  let open Infix in 
+  let loop_summary = 
+    (forall ~name:"i" `TyInt 
+    (a'.%[(var 0 `TyInt)] = a.%[(var 0 `TyInt)]
+     && b'.%[(var 0 `TyInt)] = (a.%[(int 7)]<- (int 42)).%[var 0 `TyInt]
+    )) 
+     in 
+  let error_condition = exists ~name:"j" `TyInt
+    (!(b'.%[(var 0 `TyInt)] = a'.%[(var 0 `TyInt)]) && !((var 0 `TyInt) = (int 7))) in
+
+  let combined = mk_and srk [loop_summary; error_condition] in 
+  let quantified = List.fold_left 
+    (fun acc s -> mk_exists_const srk s acc) combined [asym; asym'; bsym; bsym'] in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) quantified in
+
+  let equi_sat = Arraylift.map_elim srk pos in 
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+  
+let formula_test2 _ctx = 
+  let open Infix in 
+  let f = (exists ~name:"n" `TyInt
+    (exists ~name:"m" `TyInt 
+      (exists ~name:"a" `TyArr 
+        ((var 1 `TyInt) = (var 2 `TyInt) && !((var 0 `TyArr).%[var 1 `TyInt] = (var 0 `TyArr).%[var 2 `TyInt]))
+      ))
+  ) in 
+  let pos = rewrite srk ~down:(pos_rewriter srk) f in
+  let equi_sat = Arraylift.map_elim srk pos in 
+  match Quantifier.simsat srk equi_sat with
+  | `Sat -> failwith "Unexpected sat result"
+  | `Unsat -> ()
+  | `Unknown -> failwith "Unknown result from sat solver"
+
+let suite = "Iteration" >::: [
+  "strlen_test" >:: strlen_test;
+  "subproblem" >:: subproblem;
+   "basic_test" >:: basic_test;
+  "formula_test" >:: formula_test;
+  "existential_index_test" >:: existential_index_test;
+  "constant_index_test" >:: constant_index_test;
+  "store_test" >:: store_test;
+  "simple_store_test" >:: simple_store_test;
+  "unsat_formula" >:: unsat_formula; 
+  "formula_test2" >:: formula_test2;
+]
+
+