From 65c185275f8c78908c1496c6665bc7fd50a4607b Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Apr 2022 18:01:15 +0200
Subject: Clean-up

---
 unit-tests/Tests_verit_tactics.v | 64 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

(limited to 'unit-tests')

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.
-- 
cgit