diff --git a/simplest_model/synthesizer.ml b/simplest_model/synthesizer.ml
index 4c8f0bd..aa2e4da 100644
--- a/simplest_model/synthesizer.ml
+++ b/simplest_model/synthesizer.ml
@@ -380,7 +380,7 @@ struct
       decl == FunDecl (arg_tags, body) &
       state == St (env_before, mem_before, len_before, assignments_before) &
       state_clean == St (nil_env, mem_before, len_before, nil_assignments) &
-      list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
+      list_foldr2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
       eval_bodyo state_with_vars prog body state_evaled &
       st_spoil_assignmentso state_evaled state_spoiled &
       state_spoiled == St (_env, mem_spoiled, len, _assignments) &
diff --git a/simplest_model/tests.ml b/simplest_model/tests.ml
index 5da7fe0..2039036 100644
--- a/simplest_model/tests.ml
+++ b/simplest_model/tests.ml
@@ -2,48 +2,7 @@ open Tests_f
 open Synthesizer
 open Relational
 
-let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
-let%expect_test "some test" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
-let%expect_test "some test" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
-let%expect_test "some test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
-let%expect_test "some test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
-let%expect_test "some test" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "some test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "some test" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}]
-let%expect_test "some test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Unit], S (S (O)), [S (O); O])] |}]
-let%expect_test "some test" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}]
-let%expect_test "some test" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
-let%expect_test "some test" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "some test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
-let%expect_test "some test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eeal_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (synt_t1 ()); [%expect {| [Val] |}]
-let%expect_test "some test" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}]
-let%expect_test "some test" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}]
-let%expect_test "some test" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
-(* TODO: test with assymetric args order *)
-(* TODO: tests names *)
-
+(* type tests *)
 let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Ref] |}]
 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))])] |}]
@@ -53,9 +12,47 @@ let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {|
 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, 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, O)], [Unit], S (O), [])] |}]
+let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}]
+let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}]
+let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Unit], S (S (O)), [S (O); O])] |}]
+let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}]
+let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}]
+let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
+let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
+let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}]
+let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
+let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}]
+let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
+let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, 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 "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, [])] |}]
+let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}]
+let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
+let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}]
+let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}]
+let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
+let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}]
+let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}]
+let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}]
+let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
+let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
+let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
+(* TODO: test with assymetric args order *)
+(* TODO: tests names *)
 
diff --git a/simplest_model/tests_f.ml b/simplest_model/tests_f.ml
index 3c1a8a0..1da1256 100644
--- a/simplest_model/tests_f.ml
+++ b/simplest_model/tests_f.ml
@@ -311,7 +311,7 @@ let prog_eval_t1 _ = show(answer) (Stream.take (run q
   (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-let prog_eeal_t2 _ = show(answer) (Stream.take (run q
+let prog_eval_t2 _ = show(answer) (Stream.take (run q
   (fun q -> let open Prog in
             let open FunDecl in
             let open Tag in
@@ -416,3 +416,14 @@ let synt_t8 _ = show(answerTags) (Stream.take (run qr
             let open St in
             ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
+
+(* annotation gen prog test *)
+let synt_t9 _ = 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 {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Read 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))})
+  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
+