diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml
index 2f947e2..232daef 100644
--- a/model_with_structures/tests.ml
+++ b/model_with_structures/tests.ml
@@ -76,5 +76,3 @@ let%expect_test "simple synthesis test, reference forbidden write" = print_endli
 
 let%expect_test "simple synthesis test, reference forbidden write, no read write caps constraints" = print_endline(prog_cp_cap_synt_t_simple_call_ref_fbd_wr' ());
   [%expect {| [Cp; Cp; Cp; Cp] |}]
-
-(* TODO *)
diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml
index 5307742..80e009c 100644
--- a/model_with_structures/tests_f.ml
+++ b/model_with_structures/tests_f.ml
@@ -485,112 +485,3 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
                                                ReadS (DerefP (VarP yg)))) &
               prog_evalo prog st })
   (fun q -> q#reify (CopyCap.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)))) *)
-
-(* 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)]))) *)
-
-(* 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] *) *)
-
-(* 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 *) *)
-
-(* 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 *) *)
-
-(* 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)]))) *)
-
-(* 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)]))) *)
-
-(* 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)]))) *)