use of anomaly for timeout

4 files changed, 35 insertions, 7 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
diff --git a/src/PropToBool.v b/src/PropToBool.v
index bbe1967..e06b336 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -164,10 +164,10 @@ Ltac prop2bool_hyp H :=
     destruct HFalse
   | ];
   clear H';
-  match (eval compute in prop2bool_comp) with
+  lazymatch (eval compute in prop2bool_comp) with
   | true =>
     let A := eval cbv in prop2bool_t in
-    match goal with
+    lazymatch goal with
     | [ _ : CompDec A |- _ ] => idtac
     | _ =>
       let Hcompdec := fresh "Hcompdec" in
@@ -195,7 +195,7 @@ Ltac prop2bool_hyp H :=
           | _ => prop2bool
           end in
       tac_rec;
-      match goal with
+      lazymatch goal with
       | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g
       end;
       destruct HFalse
@@ -213,9 +213,9 @@ Ltac prop2bool_hyp H :=
 
 Ltac remove_compdec_hyp H :=
   let TH := type of H in
-  match TH with
+  lazymatch TH with
   | forall p : CompDec ?A, _ =>
-    match goal with
+    lazymatch goal with
     | [ p' : CompDec A |- _ ] =>
       let H1 := fresh in
       assert (H1 := H p'); clear H; assert (H := H1); clear H1;
diff --git a/src/Tactics.v b/src/Tactics.v
index e41b0f5..c44af14 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -29,7 +29,7 @@ Ltac get_hyps_acc acc k :=
       | id _ => fail
       | _ =>
         change P with (id P) in H;
-        match acc with
+        lazymatch acc with
         | Some ?t => get_hyps_acc (Some (H, t)) k
         | None => get_hyps_acc (Some H) k
         end
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index b0c75a7..12efcc9 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -207,7 +207,7 @@ let call_verit timeout _ rt ro ra_quant rf_quant first lsmt =
           CoqInterface.error ("veriT failed with the error: " ^ l)
       done
     with End_of_file -> () in
-  if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = failwith "veriT timed out" in ());
+  if exit_code = 124 (*code for timeout*) then (Printf.printf "bar" ; flush stdout ; close_in win; Sys.remove wname; let _ = CErrors.anomaly (Pp.str "veriT timed out") in ()) ;
   try
     if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();