Clean-up

1 files changed, 64 insertions, 0 deletions

diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index a6ea27b..4285f96 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1498,3 +1498,67 @@ Section OCamlCompDec.
       x ++ y = a0::nil -> x = nil /\ y = a0::nil \/ x = a0::nil /\ y = nil.
   Proof. verit_no_check. Qed.
 End OCamlCompDec.
+
+
+Section TimeoutBool.
+  Variable P : Z -> bool.
+  Variable H0 : P 0.
+  Variable HInd : forall n, implb (P n) (P (n + 1)).
+
+  Goal P 3.
+  Proof.
+    verit_bool_base_auto_timeout (Some (H0, HInd)) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_base_auto_timeout (Some (H0, HInd)) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_timeout 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_timeout 10.
+  Qed.
+End TimeoutBool.
+
+
+Section TimeoutProp.
+  Variable P : Z -> bool.
+  Variable H0 : P 0.
+  Variable HInd : forall n, (P n) -> (P (n + 1)).
+
+  Goal P 3.
+  Proof.
+    verit_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_timeout 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_no_check_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_no_check_timeout 10.
+  Qed.
+End TimeoutProp.