use of anomaly for timeout

1 files changed, 28 insertions, 0 deletions

diff --git a/examples/foo.v b/examples/foo.v
new file mode 100644
index 0000000..c2162df
--- /dev/null
+++ b/examples/foo.v
@@ -0,0 +1,28 @@
+Add Rec LoadPath "../src" as SMTCoq.
+Require Import SMTCoq.SMTCoq.
+Require Import ZArith.
+
+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.
+Qed.
+
+Tactic Notation "verit_timeout2"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          lazymatch Hs with
+                          | Some ?Hs => idtac 1 ;
+                            prop2bool_hyps Hs; idtac 2 ;
+                            [ .. | idtac 3 ; verit_bool_base_auto_timeout (Some Hs) ]
+                          | None => idtac 4 ; verit_bool_base_auto_timeout (@None nat)
+                          end)
+  ].
+
+Goal true -> P 1000000000.
+intro H.
+verit_timeout2. constructor.
\ No newline at end of file