diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 10b74d7..84a7472 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -256,13 +256,14 @@ struct
   let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
                       (r' : read_cap) (w' : write_cap) (m : mode)
                       (c : copy_cap) : bool =
-    (* FIXME TMP
-    Printf.printf "%b %b %b %b %b\n"
-      (r != Rd || v == ZeroV)
-      (r != Rd || fst m == In)
-      (snd m != Out || w == AlwaysWr)
-      (((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
-      (is_trivial_v v); *)
+    (* FIXME TMP *)
+    (* Printf.printf "%b %b %b %b %b\n" *)
+      (* (r != Rd || v == ZeroV) *)
+      (* (r != Rd || fst m == In) *)
+      (* (snd m != Out || w == AlwaysWr) *)
+      (* (* TODO: FIXME: why always write ?? *) *)
+      (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
+      (* (is_trivial_v v); *)
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
@@ -399,13 +400,32 @@ struct
 
   let ( #. ) x y = SeqS (x, y)
 
-  let vx = VarP 0
-  let vy = VarP 1
-  let vz = VarP 2
+  let v0 = VarP 0
+  let v1 = VarP 1
+  let v2 = VarP 2
+  let v3 = VarP 3
+  let v4 = VarP 4
+  let v5 = VarP 5
+  let vg0 = VarP (globals_min_id)
+  let vg1 = VarP (globals_min_id + 1)
+  let vg2 = VarP (globals_min_id + 2)
+  let vg3 = VarP (globals_min_id + 3)
+  let vg4 = VarP (globals_min_id + 4)
+  let vg5 = VarP (globals_min_id + 5)
 
-  let vgx = VarP (globals_min_id)
-  let vgy = VarP (globals_min_id + 1)
-  let vgz = VarP (globals_min_id + 2)
+  let rf0E = RefE 0
+  let rf1E = RefE 1
+  let rf2E = RefE 2
+  let rf3E = RefE 3
+  let rf4E = RefE 4
+  let rf5E = RefE 5
+  let rfg0E = RefE globals_min_id
+  let rfg1E = RefE (globals_min_id + 1)
+  let rfg2E = RefE (globals_min_id + 2)
+  let rfg3E = RefE (globals_min_id + 3)
+  let rfg4E = RefE (globals_min_id + 4)
+  let rfg5E = RefE (globals_min_id + 5)
+  let pE p = PathE p
 
   let drf p = DerefP p
   let access p i = AccessP (p, i)
@@ -426,7 +446,12 @@ struct
 
   let moded t = ((In, NOut), t)
 
-  let defg t = VarD (t, UnitE)
+  let defgu t = VarD (t, UnitE)
+  let defg t e = VarD (t, e)
+
+  let wrS p = WriteS p 
+  let rdS p = ReadS p 
+  let callS f args = CallS (f, args)
 
   (* - utils tests *)
 
@@ -491,20 +516,174 @@ struct
 
   (* - basic call tests *)
 
-  let%expect_test "simple call with read" =
-    prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
-                      FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
-                     CallS (VarP (globals_min_id + 1),
-                            [PathE (VarP globals_min_id)]));
+  (* let%expect_test "simple call with read" = *)
+    (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
+                      (* FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], *)
+                     (* CallS (VarP (globals_min_id + 1), *)
+                            (* [PathE (VarP globals_min_id)])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* let%expect_test "simple call with write" = *)
+    (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
+                      (* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *)
+                      (* FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], *)
+                     (* CallS (VarP (globals_min_id + 2), *)
+                            (* [PathE (VarP (globals_min_id + 1))])); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  let%expect_test "simple call with read, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_mw;
+        defg (rfT uT_r_mw) rfg0E;
+        FunD (
+          [moded @@ cpT @@ uT_r],
+          rdS @@ drf @@ v0
+        )
+      ],
+      callS vg2 [pE vg1]
+    );
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  let%expect_test "simple call with write" =
-    prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
-                      VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
-                      FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
-                     CallS (VarP (globals_min_id + 2),
-                            [PathE (VarP (globals_min_id + 1))]));
+  let%expect_test "simple call with write, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_mw;
+        defg (rfT uT_r_mw) rfg0E;
+        FunD (
+          [moded @@ cpT @@ uT_r_mw],
+          wrS @@ drf @@ v0
+        )
+      ],
+      callS vg2 [pE vg1]
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with read after write, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_mw;
+        defg (rfT uT_r_mw) rfg0E;
+        FunD (
+          [moded @@ cpT @@ uT_mw],
+          (wrS @@ drf @@ v0) #.
+          (rdS @@ drf @@ v0)
+        )
+      ],
+      callS vg2 [pE vg1]
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with forbidden write, dsl" =
+    try (prog_eval_noret (
+      [
+        defgu uT_r_mw;
+        defg (rfT uT_r_mw) rfg0E;
+        FunD (
+          [moded @@ cpT @@ uT_r],
+          wrS @@ drf @@ v0
+        )
+      ],
+      callS vg2 [pE vg1]
+    );
+    [%expect.unreachable]);
+    with Eval_error msg -> Printf.printf "%s" msg;
+    [%expect {| write: write tag |}]
+
+  (* TODO: FIXME: why is condition on always write in parent ?? *)
+  let%expect_test "simple call with write to ref, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        FunD (
+          [moded @@ rfT @@ uT_aw],
+          wrS @@ drf @@ v0
+        )
+      ],
+      callS vg2 [pE vg1]
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with forbidden write to ref, dsl" =
+    try (prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        FunD (
+          [moded @@ rfT @@ uT_aw],
+          wrS @@ drf @@ v0
+        )
+      ],
+      (callS vg2 [pE vg1]) #.
+      (rdS @@ drf @@ vg1)
+    );
+    [%expect.unreachable]);
+    with Eval_error msg -> Printf.printf "%s" msg;
+    [%expect {| read |}]
+
+  (* let%expect_test "call inside call, dsl" = *)
+    (* prog_eval_noret ( *)
+      (* [ *)
+        (* defgu uT_r_aw; *)
+        (* defg (rfT uT_r_aw) rfg0E; *)
+        (* FunD ( *)
+          (* [moded @@ rfT @@ uT_aw], *)
+          (* wrS @@ drf @@ v0 *)
+        (* ); *)
+        (* FunD ( *)
+          (* [moded @@ cpT @@ uT_aw], *)
+          (* (callS vg2 [pE v0]) #. *)
+          (* (wrS @@ drf @@ v0) *)
+        (* ) *)
+      (* ], *)
+      (* (callS vg3 [pE vg1]) #. *)
+      (* (rdS @@ drf @@ vg1) *)
+    (* ); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  let%expect_test "simple call with global variable usage, dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        FunD (
+          [moded @@ cpT @@ uT_aw],
+          (wrS @@ vg0) #.
+          (rdS @@ drf @@ vg1)
+        )
+      ],
+      (callS vg2 [pE vg1]) #.
+      (rdS @@ drf @@ vg1)
+    );
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple call with read & write (2 args), dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg0E;
+        FunD (
+          [
+            moded @@ rfT @@ uT_r;
+            moded @@ rfT @@ uT_aw;
+          ],
+          (rdS @@ drf @@ v0) #.
+          (wrS @@ drf @@ v1)
+        )
+      ],
+      callS vg4 [pE vg1; pE vg3]
+    );
     Printf.printf "done!";
     [%expect {| done! |}]
 
diff --git a/model_with_structures/dune b/model_with_structures/dune
index 54383e4..eae17b8 100644
--- a/model_with_structures/dune
+++ b/model_with_structures/dune
@@ -13,34 +13,34 @@
  (preprocess
   (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
 
-; (library
-;  (name tests_st)
-;  (modules tests)
-;  (flags (-rectypes))
-;  (libraries synthesizer_st tests_f_st)
-;  (inline_tests)
-;  (wrapped false)
-;  (preprocess
-;   (pps ppx_expect ppx_inline_test)))
+(library
+ (name tests_st)
+ (modules tests)
+ (flags (-rectypes))
+ (libraries synthesizer_st tests_f_st)
+ (inline_tests)
+ (wrapped false)
+ (preprocess
+  (pps ppx_expect ppx_inline_test)))
 
-; (library
-;  (name tests_f_st)
-;  (modules tests_f)
-;  (flags (-rectypes))
-;  (libraries OCanren OCanren.tester synthesizer_st)
-;  (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
-;  (wrapped false)
-;  (preprocess
-;   (pps
-;    OCanren-ppx.ppx_repr
-;    OCanren-ppx.ppx_deriving_reify
-;    OCanren-ppx.ppx_fresh
-;    GT.ppx
-;    GT.ppx_all
-;    OCanren-ppx.ppx_distrib
-;    --
-;    -pp
-;    camlp5/pp5+gt+plugins+ocanren+dump.exe)))
+(library
+ (name tests_f_st)
+ (modules tests_f)
+ (flags (-rectypes))
+ (libraries OCanren OCanren.tester synthesizer_st)
+ (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
+ (wrapped false)
+ (preprocess
+  (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_deriving_reify
+   OCanren-ppx.ppx_fresh
+   GT.ppx
+   GT.ppx_all
+   OCanren-ppx.ppx_distrib
+   --
+   -pp
+   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
 
 (library
  (name synthesizer_st)
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 76424e1..2dd0bf1 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -995,7 +995,7 @@ $s in stmt, f in X, x in X, a in X$
      xarrow(s)
      cl types', vals', mu' cr$,
 
-    $cl vals, mu_0 cr tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
   )
 ))
 
@@ -1025,9 +1025,9 @@ $s in stmt, f in X, x in X, a in X$
     $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
     // NOTE: check that all the possible bodies are possible to eval
-    $cl vals, mu_0 cr tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
     $...$,
-    $cl vals, mu_0 cr tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
 
     // NOTE: thick arrow to "spoil" context
     $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml
index 8017884..674f35c 100644
--- a/model_with_structures/tests.ml
+++ b/model_with_structures/tests.ml
@@ -3,59 +3,59 @@ open Synthesizer
 open Relational
 
 (* type tests *)
-let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}]
-let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}]
-let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}]
-let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
-let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
-let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}]
-let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}]
-let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
+(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
+(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)
+(* let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}] *)
+(* let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *)
+(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}] *)
+(* let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}] *)
+(* let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}] *)
+(* let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *)
 
 (* function tests *)
-let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
-let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
-let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
-let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
-let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
-let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
-let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
-let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
-let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
-let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
-let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
-let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
-let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
-let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
-let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
-let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}]
-let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}]
-let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}]
-let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}]
-let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}]
-let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}]
-let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}]
-let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
-let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
-let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}]
-let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}]
-let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}]
-let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}]
-let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
+(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *)
+(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *)
+(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] *)
+(* let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] *)
+(* let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] *)
+(* let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] *)
+(* let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
+(* let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *)
+(* let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *)
+(* let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] *)
+(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] *)
+(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] *)
+(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] *)
+(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
+(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
+(* let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *)
+(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *)
+(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}] *)
+(* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
+(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
+(* let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] *)
+(* let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] *)
+(* let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
+(* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *)
+(* let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] *)
+(* let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] *)
+(* let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] *)
+(* let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] *)
+(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
+(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] *)
+(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] *)
+(* let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] *)
+(* let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] *)
+(* let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] *)
+(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *)
+(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *)
+(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
+(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
+(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] *)
+(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] *)
+(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] *)
+(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] *)
+(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
 
-let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]
+(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
 
diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml
index 5427966..093ced7 100644
--- a/model_with_structures/tests_f.ml
+++ b/model_with_structures/tests_f.ml
@@ -4,506 +4,506 @@ open GT
 open OCanren
 open OCanren.Std
 
-@type answer  = St.ground GT.list with show
-@type answerArgs = (Arg.ground List.ground) GT.list with show
-@type answerValue = Value.ground GT.list with show
-@type answerNat = Nat.ground GT.list with show
-@type answerNats = (Nat.ground List.ground) GT.list with show
-@type answerTag = Tag.ground GT.list with show
-@type answerTags = (Tag.ground List.ground) GT.list with show
-@type answerCopyCap = CopyCap.ground GT.list with show
-@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show
+(* @type answer  = St.ground GT.list with show *)
+(* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
+(* @type answerValue = Value.ground GT.list with show *)
+(* @type answerNat = Nat.ground GT.list with show *)
+(* @type answerNats = (Nat.ground List.ground) GT.list with show *)
+(* @type answerTag = Tag.ground GT.list with show *)
+(* @type answerTags = (Tag.ground List.ground) GT.list with show *)
+(* @type answerCopyCap = CopyCap.ground GT.list with show *)
+(* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *)
 
-let inv_id_t _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 1 q })
-  (fun q -> q#reify Nat.prj_exn)))
+(* let inv_id_t _ = show(answerNat) (Stream.take (run q *)
+  (* (fun q -> ocanren { inv_ido 2 1 q }) *)
+  (* (fun q -> q#reify Nat.prj_exn))) *)
 
-let inv_id_t2 _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 0 q })
-  (fun q -> q#reify Nat.prj_exn)))
+(* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
+  (* (fun q -> ocanren { inv_ido 2 0 q }) *)
+  (* (fun q -> q#reify Nat.prj_exn))) *)
 
-let inv_id_t3 _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 q 0 })
-  (fun q -> q#reify Nat.prj_exn)))
+(* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
+  (* (fun q -> ocanren { inv_ido 2 q 0 }) *)
+  (* (fun q -> q#reify Nat.prj_exn))) *)
 
-let list_drop_t _ = show(answerNats) (Stream.take (run q
-  (fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
-  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+(* let list_drop_t _ = show(answerNats) (Stream.take (run q *)
+  (* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *)
+  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
 
-let list_replace_t  _ = show(answerNats) (Stream.take (run q
-  (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q })
-  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+(* let list_replace_t  _ = show(answerNats) (Stream.take (run q *)
+  (* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *)
+  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
 
-let arg_to_value_t _ = show(answerValue) (Stream.take (run q
-  (fun q -> let open Arg in
-            ocanren {
-    fresh s in
-      empty_stateo s &
-      arg_to_valueo s RValue q })
-  (fun q -> q#reify (Value.prj_exn))))
+(* let arg_to_value_t _ = show(answerValue) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* ocanren { *)
+    (* fresh s in *)
+      (* empty_stateo s & *)
+      (* arg_to_valueo s RValue q }) *)
+  (* (fun q -> q#reify (Value.prj_exn)))) *)
 
-let st_add_arg_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt in
-      empty_stateo s &
-      empty_stateo s' &
-      st_add_argo s  s' Nat.o rwi_val RValue q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let st_add_arg_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* ocanren { *)
+    (* fresh s, s', cnt in *)
+      (* empty_stateo s & *)
+      (* empty_stateo s' & *)
+      (* st_add_argo s  s' Nat.o rwi_val RValue q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let write_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
-      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-      stmt == Write 0 &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let write_eval_t1 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
+      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+      (* stmt == Write 0 & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let write_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
-      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-      stmt == Write 1 &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let write_eval_t2 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
+      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+      (* stmt == Write 1 & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let writes_eval_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmts in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
-      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-      stmts == [Write 0; Write 1] &
-      eval_bodyo s p stmts q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let writes_eval_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmts in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
+      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+      (* stmts == [Write 0; Write 1] & *)
+      (* eval_bodyo s p stmts q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let call_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
-      p == [FunDecl ([wi_ref], [Write 0])] &
-      stmt == Call (0, [0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let call_eval_t1 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
+      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
+      (* stmt == Call (0, [0]) & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let call_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
-      p == [FunDecl ([wi_ref], [Write 0])] &
-      stmt == Call (0, [0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let call_eval_t2 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
+      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
+      (* stmt == Call (0, [0]) & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let call_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
-      p == [FunDecl ([wi_ref], [Write 0])] &
-      stmt == Call (0, [1]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let call_eval_t3 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
+      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
+      (* stmt == Call (0, [1]) & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let call_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
-      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-      stmt == Call (0, [0; 1]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let call_eval_t4 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
+      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+      (* stmt == Call (0, [0; 1]) & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let call_eval_t5 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
-      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-      stmt == Call (0, [1; 0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let call_eval_t5 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* let open Stmt in *)
+            (* let open FunDecl in *)
+            (* ocanren { *)
+    (* fresh s, p, stmt in *)
+      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
+      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+      (* stmt == Call (0, [1; 0]) & *)
+      (* eval_stmto s p stmt q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let mem_set_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) &
-      mem_seto s 0 Unit q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let mem_set_t1 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* ocanren { *)
+    (* fresh s in *)
+      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) & *)
+      (* mem_seto s 0 Unit q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let mem_set_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
-      mem_seto s 0 Bot q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let mem_set_t2 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* ocanren { *)
+    (* fresh s in *)
+      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
+      (* mem_seto s 0 Bot q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let meem_set_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) &
-      mem_seto s 0 Bot q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let meem_set_t3 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* let open Value in *)
+            (* let open St in *)
+            (* ocanren { *)
+    (* fresh s in *)
+      (* s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) & *)
+      (* mem_seto s 0 Bot q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let add_arg_folder_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt in
-      empty_stateo s &
-      empty_stateo s' &
-      add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) })
-  (fun q -> q#reify (St.prj_exn))))
+(* let add_arg_folder_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* ocanren { *)
+    (* fresh s, s', cnt in *)
+      (* empty_stateo s & *)
+      (* empty_stateo s' & *)
+      (* add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
-let foldl2_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt, arg_tags, args in
-      arg_tags == [rwi_val] &
-      args == [RValue] &
-      empty_stateo s &
-      empty_stateo s' &
-      list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
-  (fun q -> q#reify (St.prj_exn))))
+(* let foldl2_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Arg in *)
+            (* let open Tag in *)
+            (* ocanren { *)
+    (* fresh s, s', cnt, arg_tags, args in *)
+      (* arg_tags == [rwi_val] & *)
+      (* args == [RValue] & *)
+      (* empty_stateo s & *)
+      (* empty_stateo s' & *)
+      (* list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 
-let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q
-  (fun q -> let open Arg in
-            ocanren {fresh v in List.mapo arg_to_rvalueo v q})
-  (fun q -> q#reify (List.prj_exn Arg.prj_exn))))
+(* let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q *)
+  (* (fun q -> let open Arg in *)
+            (* ocanren {fresh v in List.mapo arg_to_rvalueo v q}) *)
+  (* (fun q -> q#reify (List.prj_exn Arg.prj_exn)))) *)
 
 (* empty state test *)
-let empty_state_t _ = show(answer) (Stream.take (run q
-  (fun q -> ocanren {empty_stateo q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let empty_state_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> ocanren {empty_stateo q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [] &
-                        d == FunDecl ([], []) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t1 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [] & *)
+                        (* d == FunDecl ([], []) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [] &
-                        d == FunDecl ([wi_val], [Write 0; Read 0]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t2 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [] & *)
+                        (* d == FunDecl ([wi_val], [Write 0; Read 0]) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([wi_ref], [Write 0])] &
-                        d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t3 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [FunDecl ([wi_ref], [Write 0])] & *)
+                        (* d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([wi_ref], [Write 0])] &
-                        d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t4 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [FunDecl ([wi_ref], [Write 0])] & *)
+                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t5 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
-                        d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t5 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
+                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* fun eval test *)
-let fun_eval_t6 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([wi_val], [Write 0])] &
-                        d == FunDecl ([wi_val], [Call (0, [0])]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
+(* let fun_eval_t6 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> (* let open Prog in *) *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren { fresh s, p, d in *)
+                        (* empty_stateo s & *)
+                        (* p == [FunDecl ([wi_val], [Write 0])] & *)
+                        (* d == FunDecl ([wi_val], [Call (0, [0])]) & *)
+                        (* eval_fun_empty_argso s p d q }) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog eval test *)
-let prog_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t1 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog with func eval test *)
-let prog_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])],
-                                       FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t2 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])], *)
+                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog with func eval test *)
-let prog_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])],
-                                       FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t3 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])], *)
+                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog with func eval test *)
-let prog_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t4 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog with func eval test *)
-let prog_eval_t5 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t5 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* prog with func eval test *)
-let prog_eval_t6 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let prog_eval_t6 _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)
 
 (* annotation gen prog test *)
-let synt_t1 _ = show(answerTag) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {i_any q &
-                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))})
-  (fun q -> q#reify (Tag.prj_exn))))
+(* let synt_t1 _ = show(answerTag) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {i_any q & *)
+                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q -> q#reify (Tag.prj_exn)))) *)
 
 (* annotation gen prog test *)
-let synt_t2 _ = show(answerTag) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {i_any q & is_not_reado q &
-                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
-  (fun q -> q#reify (Tag.prj_exn))))
+(* let synt_t2 _ = show(answerTag) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {i_any q & is_not_reado q & *)
+                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q -> q#reify (Tag.prj_exn)))) *)
 
 (* annotation gen prog test *)
-let synt_t3 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r &
-                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
-                                       FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
+(* let synt_t3 _ = show(answerTags) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & *)
+                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
+                                       (* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *)
 
 (* annotation gen prog test *)
-let synt_t4 _ = show(answerTags) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {i_any q & is_not_reado q &
-                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
-  (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
+(* let synt_t4 _ = show(answerTags) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {i_any q & is_not_reado q & *)
+                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *)
 
 (* annotation gen prog test *)
-let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {fresh q', r' in
-                     i_any q' & is_not_reado q' &
-                     i_any r' & is_not_reado r' & is_never_writeo r' &
-                     eq_copyo q' q & eq_copyo r' r &
-                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
+(* let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {fresh q', r' in *)
+                     (* i_any q' & is_not_reado q' & *)
+                     (* i_any r' & is_not_reado r' & is_never_writeo r' & *)
+                     (* eq_copyo q' q & eq_copyo r' r & *)
+                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
 
 (* annotation gen prog test *)
-let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {fresh q', r' in
-                     i_any q' & is_not_reado q' &
-                     i_any r' & is_not_reado r' & is_never_writeo r' &
-                     eq_copyo q' q & eq_copyo r' r &
-                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
+(* let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {fresh q', r' in *)
+                     (* i_any q' & is_not_reado q' & *)
+                     (* i_any r' & is_not_reado r' & is_never_writeo r' & *)
+                     (* eq_copyo q' q & eq_copyo r' r & *)
+                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
 
 (* annotation gen prog test *)
-let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {fresh q', r' in
-                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
-                     eq_copyo q' q & eq_copyo r' r &
-                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+(* let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {fresh q', r' in *)
+                     (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
+                     (* eq_copyo q' q & eq_copyo r' r & *)
+                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
 
 (* annotation gen prog test *)
-let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {fresh q', r' in
-                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
-                     eq_copyo q' q & eq_copyo r' r &
-                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+(* let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {fresh q', r' in *)
+                     (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
+                     (* eq_copyo q' q & eq_copyo r' r & *)
+                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
 
 (* annotation gen prog test *)
-let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {fresh q', r' in
-                     i_any q' & is_not_reado q' &
-                     i_any r' & is_reado r' & is_never_writeo r' &
-                     eq_copyo q' q & eq_copyo r' r &
-                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
-                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})
-  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+(* let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr *)
+  (* (fun q r -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* let open St in *)
+            (* ocanren {fresh q', r' in *)
+                     (* i_any q' & is_not_reado q' & *)
+                     (* i_any r' & is_reado r' & is_never_writeo r' & *)
+                     (* eq_copyo q' q & eq_copyo r' r & *)
+                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *)
+                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
+  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
 
 (* TODO: FIXME: implement memoization cuts *)
 (* prog with recursive function call *)
-let rec_eval_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])],
-                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
+(* let rec_eval_t _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> let open Prog in *)
+            (* let open FunDecl in *)
+            (* let open Tag in *)
+            (* let open Stmt in *)
+            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])], *)
+                                       (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)