From e61a54d7581b42259d726389250e1cb63682d8d8 Mon Sep 17 00:00:00 2001 From: lduboisd Date: Mon, 11 Apr 2022 11:29:23 +0200 Subject: verit_timeout takes an integer as parameter --- examples/Example.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'examples/Example.v') 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. -- cgit From 65c185275f8c78908c1496c6665bc7fd50a4607b Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Thu, 14 Apr 2022 18:01:15 +0200 Subject: Clean-up --- examples/Example.v | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) (limited to 'examples/Example.v') 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. -- cgit