diff options
Diffstat (limited to 'unit-tests')
-rw-r--r-- | unit-tests/Makefile | 2 | ||||
-rw-r--r-- | unit-tests/Tests_verit_tactics.v | 64 |
2 files changed, 65 insertions, 1 deletions
diff --git a/unit-tests/Makefile b/unit-tests/Makefile index b042078..bd271b3 100644 --- a/unit-tests/Makefile +++ b/unit-tests/Makefile @@ -53,4 +53,4 @@ clean: cleanvo cleanvo: - rm -rf *~ *.vo *.glob *.vio .*.aux .lia.cache + rm -rf *~ *.vo *.glob *.vio .*.aux .lia.cache *.vok *.vos 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. |