diff --git a/simplest_model_with_mods/dune b/simplest_model_with_mods/dune
index 35cc40d..1e0a3d6 100644
--- a/simplest_model_with_mods/dune
+++ b/simplest_model_with_mods/dune
@@ -34,25 +34,24 @@
 ;  (preprocess
 ;   (pps ppx_expect ppx_inline_test)))
 
-; TODO: tmp, during change
-; (library
-;  (name tests_f_mods)
-;  (modules tests_f)
-;  (flags (-rectypes))
-;  (libraries OCanren OCanren.tester synthesizer_mods)
-;  (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_mods)
+ (modules tests_f)
+ (flags (-rectypes))
+ (libraries OCanren OCanren.tester synthesizer_mods)
+ (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_mods)
diff --git a/simplest_model_with_mods/tests_f.ml b/simplest_model_with_mods/tests_f.ml
index 18ea63f..30a5807 100644
--- a/simplest_model_with_mods/tests_f.ml
+++ b/simplest_model_with_mods/tests_f.ml
@@ -47,7 +47,7 @@ let st_add_arg_t _ = show(answer) (Stream.take (run q
     fresh s, s', cnt in
       empty_stateo s &
       empty_stateo s' &
-      st_add_argo s  s' Nat.o Val RValue q })
+      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
@@ -59,8 +59,8 @@ let write_eval_t1 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+      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))))
@@ -74,8 +74,8 @@ let write_eval_t2 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+      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))))
@@ -89,8 +89,8 @@ let writes_eval_t _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmts in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+      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))))
@@ -104,8 +104,8 @@ let call_eval_t1 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 0 0], [Unit], 1, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
+      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))))
@@ -119,8 +119,8 @@ let call_eval_t2 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
+      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))))
@@ -134,8 +134,8 @@ let call_eval_t3 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
+      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))))
@@ -149,8 +149,8 @@ let call_eval_t4 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+      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))))
@@ -164,8 +164,8 @@ let call_eval_t5 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             ocanren {
     fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
+      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))))
@@ -177,7 +177,7 @@ let mem_set_t1 _ = show(answer) (Stream.take (run q
             let open St in
             ocanren {
     fresh s in
-      s == St ([Std.pair 0 0], [Bot], 1, []) &
+      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))))
 
@@ -188,7 +188,7 @@ let mem_set_t2 _ = show(answer) (Stream.take (run q
             let open St in
             ocanren {
     fresh s in
-      s == St ([Std.pair 0 0], [Unit], 1, []) &
+      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))))
 
@@ -199,7 +199,7 @@ let meem_set_t3 _ = show(answer) (Stream.take (run q
             let open St in
             ocanren {
     fresh s in
-      s == St ([Std.pair 0 1], [Unit; Unit], 2, []) &
+      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))))
 
@@ -210,7 +210,7 @@ let add_arg_folder_t _ = show(answer) (Stream.take (run q
     fresh s, s', cnt in
       empty_stateo s &
       empty_stateo s' &
-      add_arg_foldero s (Std.pair s' Nat.o) Val RValue (Std.pair q cnt) })
+      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
@@ -218,7 +218,7 @@ let foldl2_t _ = show(answer) (Stream.take (run q
             let open Tag in
             ocanren {
     fresh s, s', cnt, arg_tags, args in
-      arg_tags == [Val] &
+      arg_tags == [rwi_val] &
       args == [RValue] &
       empty_stateo s &
       empty_stateo s' &
@@ -258,7 +258,7 @@ let fun_eval_t2 _ = show(answer) (Stream.take (run q
             ocanren { fresh s, p, d in
                         empty_stateo s &
                         p == [] &
-                        d == FunDecl ([Val], [Write 0; Read 0]) &
+                        d == FunDecl ([wi_val], [Write 0; Read 0]) &
                         eval_fun_empty_argso s p d q })
   (fun q -> q#reify (St.prj_exn))))
 
@@ -270,8 +270,8 @@ let fun_eval_t3 _ = show(answer) (Stream.take (run q
             let open Stmt in
             ocanren { fresh s, p, d in
                         empty_stateo s &
-                        p == [FunDecl ([Ref], [Write 0])] &
-                        d == FunDecl ([Val], [Call (0, [0]); Read 0]) &
+                        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))))
 
@@ -283,8 +283,8 @@ let fun_eval_t4 _ = show(answer) (Stream.take (run q
             let open Stmt in
             ocanren { fresh s, p, d in
                         empty_stateo s &
-                        p == [FunDecl ([Ref], [Write 0])] &
-                        d == FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]) &
+                        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))))
 
@@ -296,8 +296,8 @@ let fun_eval_t5 _ = show(answer) (Stream.take (run q
             let open Stmt in
             ocanren { fresh s, p, d in
                         empty_stateo s &
-                        p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-                        d == FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
+                        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))))
 
@@ -307,7 +307,7 @@ let prog_eval_t1 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             let open Tag in
             let open Stmt in
-            ocanren {eval_progo (Prog ([], FunDecl ([Val], [Write 0; Read 0]))) q})
+            ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
   (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
@@ -316,7 +316,8 @@ let prog_eval_t2 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             let open Tag in
             let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Val], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
+            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 *)
@@ -325,7 +326,8 @@ let prog_eval_t3 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             let open Tag in
             let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
+            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 *)
@@ -334,7 +336,8 @@ let prog_eval_t4 _ = show(answer) (Stream.take (run q
             let open FunDecl in
             let open Tag in
             let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) q})
+            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))))
 
 (* annotation gen prog test *)
@@ -344,7 +347,8 @@ let synt_t1 _ = show(answerTag) (Stream.take (run q
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))})
   (fun q -> q#reify (Tag.prj_exn))))
 
 (* annotation gen prog test *)
@@ -354,7 +358,8 @@ let synt_t2 _ = show(answerTag) (Stream.take (run q
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
   (fun q -> q#reify (Tag.prj_exn))))
 
 (* annotation gen prog test *)
@@ -364,7 +369,8 @@ let synt_t3 _ = show(answerTags) (Stream.take (run qr
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
 
 (* annotation gen prog test *)
@@ -374,7 +380,8 @@ let synt_t4 _ = show(answerTags) (Stream.take (run q
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))})
   (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
 
 (* annotation gen prog test *)
@@ -384,7 +391,8 @@ let synt_t5 _ = show(answerTags) (Stream.take (run qr
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
 
 (* annotation gen prog test *)
@@ -394,7 +402,8 @@ let synt_t6 _ = show(answerTags) (Stream.take (run qr
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))})
+            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
 
 (* annotation gen prog test *)
@@ -404,7 +413,8 @@ let synt_t7 _ = show(answerTags) (Stream.take (run qr
             let open Tag in
             let open Stmt in
             let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))})
+            ocanren {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, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
 
 (* annotation gen prog test *)
@@ -414,7 +424,8 @@ let synt_t8 _ = show(answerTags) (Stream.take (run qr
             let open Tag in
             let open Stmt in
             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, []))})
+            ocanren {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, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
 
 (* annotation gen prog test *)
@@ -424,15 +435,17 @@ let synt_t9 _ = show(answerTags) (Stream.take (run qr
             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, []))})
+            ocanren {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, []))})
   (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.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 ([Ref], [Write 0; Call (0, [0])])], FunDecl ([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 ([Ref], [Write 0; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
+  (* (fun q -> q#reify (St.prj_exn)))) *)