diff options
author | lduboisd <lduboisd@inria.fr> | 2022-04-11 11:29:23 +0200 |
---|---|---|
committer | lduboisd <lduboisd@inria.fr> | 2022-04-11 11:29:23 +0200 |
commit | e61a54d7581b42259d726389250e1cb63682d8d8 (patch) | |
tree | b2db484c1bac75ff46484a545b87a971a44c68b0 /examples/Example.v | |
parent | 59be27207e4527661d219991728a1372335ceede (diff) | |
download | smtcoq-e61a54d7581b42259d726389250e1cb63682d8d8.tar.gz smtcoq-e61a54d7581b42259d726389250e1cb63682d8d8.zip |
verit_timeout takes an integer as parameter
Diffstat (limited to 'examples/Example.v')
-rw-r--r-- | examples/Example.v | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v index b949740..9fcb555 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -14,7 +14,6 @@ If you are using native-coq instead of Coq 8.11, replace it with: Require Import SMTCoq. *) - Require Import SMTCoq.SMTCoq. Require Import Bool. @@ -425,3 +424,25 @@ Section CompCert. Qed. End CompCert. + + +(** The verit solver can be called with an integer (the timeout in seconds). +If the goal cannot be solved within timeout seconds, then an anomaly is raised **) + +Section test_timeout. + +Variable P : Z -> bool. +Variable H0 : P 0. +Variable HInd : forall n, implb (P n) (P (n + 1)). + +Goal P 3. +(* verit_timeout 3. *) verit. +Qed. + +Goal true -> P 1000000000. +intro H. +(* Fail verit_timeout 1. +Fail verit_timeout 5. *) +Abort. + +End test_timeout. |