diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:01:15 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-04-14 18:01:15 +0200 |
commit | 65c185275f8c78908c1496c6665bc7fd50a4607b (patch) | |
tree | 3d68caf8b482563c01ada2cf426f7f96d6fda76a /examples | |
parent | deb9927455bcb3b506d17a63a9b7b5ec11fe9027 (diff) | |
download | smtcoq-65c185275f8c78908c1496c6665bc7fd50a4607b.tar.gz smtcoq-65c185275f8c78908c1496c6665bc7fd50a4607b.zip |
Clean-up
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Example.v | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/examples/Example.v b/examples/Example.v index 0cd1477..5e12e74 100644 --- a/examples/Example.v +++ b/examples/Example.v @@ -426,23 +426,27 @@ Section CompCert. 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 **) +(** 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)). + 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 P 3. + Proof. + (* verit_timeout 3. *) verit. + Qed. -Goal true -> P 1000000000. -intro H. -(* Fail verit_timeout 1. -Fail verit_timeout 5. *) -Abort. + Goal true -> P 1000000000. + Proof. + intro H. + (* verit_timeout 5. *) + Abort. End test_timeout. |