diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:06:08 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:06:08 +0200 |
commit | 1f21e1f95d43f5e76e38e1737de9a2a0322fd71c (patch) | |
tree | 68192813dab5806dcfd608d1c474b4030b0006f6 /examples/Example.v | |
parent | 965520037392fa6c523348e3ff9dff5b9d5c2313 (diff) | |
parent | 65c185275f8c78908c1496c6665bc7fd50a4607b (diff) | |
download | smtcoq-1f21e1f95d43f5e76e38e1737de9a2a0322fd71c.tar.gz smtcoq-1f21e1f95d43f5e76e38e1737de9a2a0322fd71c.zip |
Merge remote-tracking branch 'origin/coq-8.11' into coq-8.12
Diffstat (limited to 'examples/Example.v')
-rw-r--r-- | examples/Example.v | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/examples/Example.v b/examples/Example.v index cd53212..5e12e74 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,29 @@ Section CompCert. Qed. End CompCert. + + +(** The verit solver can be called with a timeout (a positive integer, + in seconds). If the goal cannot be solved within this given time, + then an anomaly is raised. + To test, one can uncomment the following examples. +**) + +Section test_timeout. + + Variable P : Z -> bool. + Variable H0 : P 0. + Variable HInd : forall n, implb (P n) (P (n + 1)). + + Goal P 3. + Proof. + (* verit_timeout 3. *) verit. + Qed. + + Goal true -> P 1000000000. + Proof. + intro H. + (* verit_timeout 5. *) + Abort. + +End test_timeout. |