diff --git a/tests/btv/btv.ml2mk.ml b/tests/btv/btv.ml2mk.ml
new file mode 100644
index 0000000..82b5859
--- /dev/null
+++ b/tests/btv/btv.ml2mk.ml
@@ -0,0 +1,44 @@
+open Peano
+
+let m1 = 1
+let m2 = 2
+let m3 = 5
+let m4 = 10
+let max_time = 17
+let same_side (left_group, _) a b = List.mem a left_group = List.mem b left_group
+
+let has_torch (left_group, torch_on_the_left) a =
+  List.mem a left_group = torch_on_the_left
+;;
+
+let member x = x = m1 || x = m2 || x = m3 || x = m4
+
+let can_move state = function
+  | [ a ] -> member a && has_torch state a
+  | [ a; b ] -> member a && member b && a < b && same_side state a b && has_torch state a
+  | [] | _ :: _ :: _ :: _ -> false
+;;
+
+let move (left_group, torch_on_the_left) a =
+  if List.mem a left_group
+  then List.filter (( <> ) a) left_group, false
+  else a :: left_group, true
+;;
+
+let verify moves =
+  let[@tabled] rec verify_rec time ((left_group, torch_on_the_left) as state) = function
+    | [] -> left_group = [] && (not torch_on_the_left) && time <= max_time
+    | m :: moves ->
+      time < max_time
+      && can_move state m
+      && verify_rec (time + List.fold_left max 0 m) (List.fold_left move state m) moves
+  in
+  verify_rec 0 ([ m1; m2; m3; m4 ], true) moves
+;;
+
+[@@@ocaml
+  Printf.printf "Functional: %b\n"
+  @@ verify [ [ 1; 2 ]; [ 2 ]; [ 5; 10 ]; [ 1 ]; [ 1; 2 ] ];
+  Printf.printf "Functional: %b\n" @@ verify [ [ 1; 2 ]; [ 1 ]; [ 1; 5 ]; [ 1 ] ];
+  Printf.printf "Functional: %b\n" @@ verify [ [ 1 ]; [ 2 ] ];
+  Printf.printf "Functional: %b\n" @@ verify [ [ 1; 2; 5; 10 ] ]]
diff --git a/tests/btv/btv.t b/tests/btv/btv.t
new file mode 100644
index 0000000..d132f0c
--- /dev/null
+++ b/tests/btv/btv.t
@@ -0,0 +1,7 @@
+  $ ./btv_run.exe
+  Functional: true
+  Functional: false
+  Functional: false
+  Functional: false
+  [ [ 1; 2]; [ 2]; [ 5; 10]; [ 1]; [ 1; 2]]
+  [ [ 1; 2]; [ 1]; [ 5; 10]; [ 2]; [ 1; 2]]
diff --git a/tests/btv/btv_run.ml b/tests/btv/btv_run.ml
new file mode 100644
index 0000000..2f5c182
--- /dev/null
+++ b/tests/btv/btv_run.ml
@@ -0,0 +1,23 @@
+open OCanren
+open Btv.FO
+
+let rec print_answers ~pp ppf stream =
+  let answ, stream = Stream.retrieve ~n:1 stream in
+  match answ with
+  | [] -> ()
+  | [ a ] ->
+    Format.fprintf ppf "%a\n%!" pp a;
+    print_answers ~pp ppf stream
+  | _ -> assert false
+;;
+
+let _ =
+  run
+    q
+    (fun q -> verify q !!true)
+    (fun rr ->
+      rr#reify
+        (Std.List.prj_exn
+           (Std.List.prj_exn (fun x y -> Std.Nat.to_int @@ Std.Nat.prj_exn x y))))
+  |> Format.printf "%a" (print_answers ~pp:[%fmt: GT.int GT.list GT.list])
+;;
diff --git a/tests/btv/dune b/tests/btv/dune
new file mode 100644
index 0000000..a09dfea
--- /dev/null
+++ b/tests/btv/dune
@@ -0,0 +1,31 @@
+(env
+ (_
+  (flags
+   (:standard -rectypes -w -27-33-39))))
+
+(rule
+ (targets btv.ml)
+ (deps
+  (:exec %{project_root}/src/noCanren.exe)
+  (:peano %{project_root}/std/.Peano.objs/byte/peano.cmi)
+  (:list %{project_root}/std/.List.objs/byte/list.cmi)
+  (:input btv.ml2mk.ml))
+ (action
+  (run
+   sh
+   -c
+   "%{exec} -w -8 %{input} -rectypes -o %{targets} | ocamlformat --enable-outside-detected-project --impl -")))
+
+(executable
+ (name btv_run)
+ (libraries GT OCanren OCanren.tester Peano List)
+ (modules btv btv_run)
+ (preprocess
+  (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_distrib
+   GT.ppx_all)))
+
+(cram
+ (deps ./btv_run.exe))