From 15ab2869ab700d21c59c5a272721b5bba1d2b8ee Mon Sep 17 00:00:00 2001
From: lduboisd <lduboisd@inria.fr>
Date: Fri, 10 Dec 2021 17:55:46 +0100
Subject: verit timeout

---
 src/Tactics.v       | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/g_smtcoq.mlg    |  6 +++--
 src/verit/verit.ml  | 14 ++++++++---
 src/verit/verit.mli |  4 +--
 4 files changed, 87 insertions(+), 8 deletions(-)

diff --git a/src/Tactics.v b/src/Tactics.v
index f79b253..e41b0f5 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -89,6 +89,31 @@ Tactic Notation "verit_bool_no_check" constr(h) :=
 Tactic Notation "verit_bool_no_check"           :=
   get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto Hs; vauto).
 
+(** Tactics in bool with timeout **)
+
+Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances.
+Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances.
+
+Tactic Notation "verit_bool_timeout" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs))
+                   | None => verit_bool_base_auto_timeout (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool_timeout"           :=
+  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto).
+
+Tactic Notation "verit_bool_no_check_timeout" constr(h) :=
+  get_hyps ltac:(fun Hs =>
+                   match Hs with
+                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs))
+                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                   end;
+                   vauto).
+Tactic Notation "verit_bool_no_check_timeout"           :=
+  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; vauto).
+
 
 (** Tactics in Prop **)
 
@@ -140,6 +165,52 @@ Tactic Notation "verit_no_check"           :=
                           end; vauto)
   ].
 
+Tactic Notation "verit_timeout" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) ]
+                                   | None => verit_bool_base_auto_timeout (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit_timeout"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_base_auto_timeout (Some Hs) ]
+                          | None => verit_bool_base_auto_timeout (@None nat)
+                          end; vauto)
+  ].
+Tactic Notation "verit_no_check_timeout" constr(h) :=
+  prop2bool;
+  [ .. | prop2bool_hyps h;
+         [ .. | get_hyps ltac:(fun Hs =>
+                                 match Hs with
+                                   | Some ?Hs =>
+                                     prop2bool_hyps Hs;
+                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) ]
+                                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                                 end; vauto)
+         ]
+  ].
+Tactic Notation "verit_no_check_timeout"           :=
+  prop2bool;
+  [ .. | get_hyps ltac:(fun Hs =>
+                          match Hs with
+                          | Some ?Hs =>
+                            prop2bool_hyps Hs;
+                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) ]
+                          | None => verit_bool_no_check_base_auto_timeout (@None nat)
+                          end; vauto)
+  ].
+
+
 Ltac cvc4            := prop2bool; [ .. | cvc4_bool; bool2prop ].
 Ltac cvc4_no_check   := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ].
 
diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg
index c8d38db..19298f4 100644
--- a/src/g_smtcoq.mlg
+++ b/src/g_smtcoq.mlg
@@ -113,8 +113,10 @@ END
 
 
 TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic lpl (get_lemmas ()) }
-| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check lpl (get_lemmas ()) }
+| [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) }
+| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) }
 END
 
 TACTIC EXTEND Tactic_cvc4
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index 7f89943..b0c75a7 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -169,7 +169,7 @@ let export out_channel rt ro lsmt =
 
 exception Unknown
 
-let call_verit _ rt ro ra_quant rf_quant first lsmt =
+let call_verit timeout _ rt ro ra_quant rf_quant first lsmt =
   let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in
   export outchan rt ro lsmt;
   close_out outchan;
@@ -177,6 +177,11 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
   let wname, woc = Filename.open_temp_file "warnings_verit" ".log" in
   close_out woc;
   let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename ^ " 2> " ^ wname in
+  let command = 
+    match timeout with
+      | Some i -> "timeout "^(string_of_int i)^" "^command
+      | None -> command
+  in
   Format.eprintf "%s@." command;
   let t0 = Sys.time () in
   let exit_code = Sys.command command in
@@ -202,7 +207,7 @@ let call_verit _ 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 ());
   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 ();
@@ -217,7 +222,7 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
 let verit_logic =
   SL.of_list [LUF; LLia]
 
-let tactic_gen vm_cast lcpl lcepl =
+let tactic_gen vm_cast timeout lcpl lcepl =
   (* Transform the tuple of lemmas given by the user into a list *)
   let lcpl =
     let lcpl = EConstr.Unsafe.to_constr lcpl in
@@ -235,6 +240,7 @@ let tactic_gen vm_cast lcpl lcepl =
   let rf = VeritSyntax.rf in
   let ra_quant = VeritSyntax.ra_quant in
   let rf_quant = VeritSyntax.rf_quant in
-  SmtCommands.tactic call_verit verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl
+  SmtCommands.tactic (call_verit timeout) verit_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl
 let tactic = tactic_gen vm_cast_true
 let tactic_no_check = tactic_gen (fun _ -> vm_cast_true_no_check)
+
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index f0acd0c..654de07 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -19,5 +19,5 @@ val parse_certif :
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
 val theorem : CoqInterface.id -> string -> string -> unit
-val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
-val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic_no_check : int option -> EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
-- 
cgit 


From 59be27207e4527661d219991728a1372335ceede Mon Sep 17 00:00:00 2001
From: lduboisd <lduboisd@inria.fr>
Date: Fri, 8 Apr 2022 17:11:50 +0200
Subject: use of anomaly for timeout

---
 examples/foo.v     | 28 ++++++++++++++++++++++++++++
 src/PropToBool.v   | 10 +++++-----
 src/Tactics.v      |  2 +-
 src/verit/verit.ml |  2 +-
 4 files changed, 35 insertions(+), 7 deletions(-)
 create mode 100644 examples/foo.v

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 ();
-- 
cgit 


From e61a54d7581b42259d726389250e1cb63682d8d8 Mon Sep 17 00:00:00 2001
From: lduboisd <lduboisd@inria.fr>
Date: Mon, 11 Apr 2022 11:29:23 +0200
Subject: verit_timeout takes an integer as parameter

---
 examples/Example.v | 23 ++++++++++++++++++++++-
 examples/foo.v     | 28 ----------------------------
 src/Tactics.v      | 48 ++++++++++++++++++++++++------------------------
 src/g_smtcoq.mlg   |  4 ++--
 4 files changed, 48 insertions(+), 55 deletions(-)
 delete mode 100644 examples/foo.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.
diff --git a/examples/foo.v b/examples/foo.v
deleted file mode 100644
index c2162df..0000000
--- a/examples/foo.v
+++ /dev/null
@@ -1,28 +0,0 @@
-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/Tactics.v b/src/Tactics.v
index c44af14..316fcc1 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -91,28 +91,28 @@ Tactic Notation "verit_bool_no_check"           :=
 
 (** Tactics in bool with timeout **)
 
-Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances.
-Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances.
+Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances.
+Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances.
 
-Tactic Notation "verit_bool_timeout" constr(h) :=
+Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) :=
   get_hyps ltac:(fun Hs =>
                    match Hs with
-                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs))
-                   | None => verit_bool_base_auto_timeout (Some h)
+                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
+                   | None => verit_bool_base_auto_timeout (Some h) timeout
                    end;
                    vauto).
-Tactic Notation "verit_bool_timeout"           :=
-  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; vauto).
+Tactic Notation "verit_bool_timeout"  int_or_var(timeout)         :=
+  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto).
 
-Tactic Notation "verit_bool_no_check_timeout" constr(h) :=
+Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) :=
   get_hyps ltac:(fun Hs =>
                    match Hs with
-                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs))
-                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
+                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
                    end;
                    vauto).
-Tactic Notation "verit_bool_no_check_timeout"           :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; vauto).
+Tactic Notation "verit_bool_no_check_timeout"   int_or_var(timeout)        :=
+  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto).
 
 
 (** Tactics in Prop **)
@@ -165,48 +165,48 @@ Tactic Notation "verit_no_check"           :=
                           end; vauto)
   ].
 
-Tactic Notation "verit_timeout" constr(h) :=
+Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
          [ .. | get_hyps ltac:(fun Hs =>
                                  match Hs with
                                    | Some ?Hs =>
                                      prop2bool_hyps Hs;
-                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) ]
-                                   | None => verit_bool_base_auto_timeout (Some h)
+                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout]
+                                   | None => verit_bool_base_auto_timeout (Some h) timeout
                                  end; vauto)
          ]
   ].
-Tactic Notation "verit_timeout"           :=
+Tactic Notation "verit_timeout"   int_or_var(timeout)        :=
   prop2bool;
   [ .. | get_hyps ltac:(fun Hs =>
                           match Hs with
                           | Some ?Hs =>
                             prop2bool_hyps Hs;
-                            [ .. | verit_bool_base_auto_timeout (Some Hs) ]
-                          | None => verit_bool_base_auto_timeout (@None nat)
+                            [ .. | verit_bool_base_auto_timeout (Some Hs) timeout]
+                          | None => verit_bool_base_auto_timeout (@None nat) timeout
                           end; vauto)
   ].
-Tactic Notation "verit_no_check_timeout" constr(h) :=
+Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
          [ .. | get_hyps ltac:(fun Hs =>
                                  match Hs with
                                    | Some ?Hs =>
                                      prop2bool_hyps Hs;
-                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) ]
-                                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
+                                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
                                  end; vauto)
          ]
   ].
-Tactic Notation "verit_no_check_timeout"           :=
+Tactic Notation "verit_no_check_timeout"   int_or_var(timeout)        :=
   prop2bool;
   [ .. | get_hyps ltac:(fun Hs =>
                           match Hs with
                           | Some ?Hs =>
                             prop2bool_hyps Hs;
-                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) ]
-                          | None => verit_bool_no_check_base_auto_timeout (@None nat)
+                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
+                          | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
                           end; vauto)
   ].
 
diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg
index 19298f4..1d8f146 100644
--- a/src/g_smtcoq.mlg
+++ b/src/g_smtcoq.mlg
@@ -115,8 +115,8 @@ END
 TACTIC EXTEND Tactic_verit
 | [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) }
 | [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) }
-| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) }
-| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) }
+| [ "verit_bool_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic (Some timeout) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic_no_check (Some timeout) lpl (get_lemmas ()) }
 END
 
 TACTIC EXTEND Tactic_cvc4
-- 
cgit 


From deb9927455bcb3b506d17a63a9b7b5ec11fe9027 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Apr 2022 18:01:03 +0200
Subject: Port

---
 src/Tactics.v | 87 ++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 45 insertions(+), 42 deletions(-)

diff --git a/src/Tactics.v b/src/Tactics.v
index 727e0b7..6f2c7b1 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -94,30 +94,33 @@ Tactic Notation "verit_bool_no_check"           :=
   let Hs := get_hyps in
   fun Hs => verit_bool_no_check_base_auto Hs; vauto.
 
+
 (** Tactics in bool with timeout **)
 
 Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances.
 Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances.
 
 Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) :=
-  get_hyps ltac:(fun Hs =>
-                   match Hs with
-                   | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
-                   | None => verit_bool_base_auto_timeout (Some h) timeout
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout
+  | None => verit_bool_base_auto_timeout (Some h) timeout
+  end;
+  vauto.
 Tactic Notation "verit_bool_timeout"  int_or_var(timeout)         :=
-  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto).
+  let Hs := get_hyps in
+  verit_bool_base_auto_timeout Hs timeout; vauto.
 
 Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) :=
-  get_hyps ltac:(fun Hs =>
-                   match Hs with
-                   | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
-                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
-                   end;
-                   vauto).
+  let Hs := get_hyps in
+  match Hs with
+  | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout
+  | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+  end;
+  vauto.
 Tactic Notation "verit_bool_no_check_timeout"   int_or_var(timeout)        :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto).
+  let Hs := get_hyps in
+  verit_bool_no_check_base_auto_timeout Hs timeout; vauto.
 
 
 (** Tactics in Prop **)
@@ -173,46 +176,46 @@ Tactic Notation "verit_no_check"           :=
 Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout]
-                                   | None => verit_bool_base_auto_timeout (Some h) timeout
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                    prop2bool_hyps Hs;
+                    [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout ]
+                | None => verit_bool_base_auto_timeout (Some h) timeout
+                end; vauto
          ]
   ].
 Tactic Notation "verit_timeout"   int_or_var(timeout)        :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_base_auto_timeout (Some Hs) timeout]
-                          | None => verit_bool_base_auto_timeout (@None nat) timeout
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+             prop2bool_hyps Hs;
+             [ .. | verit_bool_base_auto_timeout (Some Hs) timeout ]
+         | None => verit_bool_base_auto_timeout (@None nat) timeout
+         end; vauto
   ].
 Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) :=
   prop2bool;
   [ .. | prop2bool_hyps h;
-         [ .. | get_hyps ltac:(fun Hs =>
-                                 match Hs with
-                                   | Some ?Hs =>
-                                     prop2bool_hyps Hs;
-                                     [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
-                                   | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
-                                 end; vauto)
+         [ .. | let Hs := get_hyps in
+                match Hs with
+                | Some ?Hs =>
+                    prop2bool_hyps Hs;
+                    [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ]
+                | None => verit_bool_no_check_base_auto_timeout (Some h) timeout
+                end; vauto
          ]
   ].
 Tactic Notation "verit_no_check_timeout"   int_or_var(timeout)        :=
   prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          match Hs with
-                          | Some ?Hs =>
-                            prop2bool_hyps Hs;
-                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
-                          | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
-                          end; vauto)
+  [ .. | let Hs := get_hyps in
+         match Hs with
+         | Some ?Hs =>
+             prop2bool_hyps Hs;
+             [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout ]
+         | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
+         end; vauto
   ].
 
 
-- 
cgit 


From 65c185275f8c78908c1496c6665bc7fd50a4607b Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Thu, 14 Apr 2022 18:01:15 +0200
Subject: Clean-up

---
 examples/Example.v               | 30 +++++++++++--------
 src/trace/coqInterface.ml        |  1 +
 src/trace/coqInterface.mli       |  1 +
 src/verit/verit.ml               |  2 +-
 unit-tests/Tests_verit_tactics.v | 64 ++++++++++++++++++++++++++++++++++++++++
 5 files changed, 84 insertions(+), 14 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.
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml
index a8af566..8b91225 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -150,6 +150,7 @@ let set_evars_tac noc =
 (* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
 let error s = CErrors.user_err (Pp.str s)
+let anomaly s = CErrors.anomaly (Pp.str s)
 let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s
 
 let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c)
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli
index 86fdd95..453bce1 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -98,6 +98,7 @@ val set_evars_tac : constr -> tactic
 (* Other differences between the two versions of Coq *)
 type constr_expr = Constrexpr.constr_expr
 val error : string -> 'a
+val anomaly : string -> 'a
 val warning : string -> string -> unit
 val extern_constr : constr -> constr_expr
 val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index eb8c5cc..33f9b4c 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 _ = CErrors.anomaly (Pp.str "veriT timed out") in ()) ;
+  if exit_code = 124 (*code for timeout*) then (close_in win; Sys.remove wname; let _ = CoqInterface.anomaly "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 ();
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index a6ea27b..4285f96 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1498,3 +1498,67 @@ Section OCamlCompDec.
       x ++ y = a0::nil -> x = nil /\ y = a0::nil \/ x = a0::nil /\ y = nil.
   Proof. verit_no_check. Qed.
 End OCamlCompDec.
+
+
+Section TimeoutBool.
+  Variable P : Z -> bool.
+  Variable H0 : P 0.
+  Variable HInd : forall n, implb (P n) (P (n + 1)).
+
+  Goal P 3.
+  Proof.
+    verit_bool_base_auto_timeout (Some (H0, HInd)) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_base_auto_timeout (Some (H0, HInd)) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_timeout 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_bool_no_check_timeout 10.
+  Qed.
+End TimeoutBool.
+
+
+Section TimeoutProp.
+  Variable P : Z -> bool.
+  Variable H0 : P 0.
+  Variable HInd : forall n, (P n) -> (P (n + 1)).
+
+  Goal P 3.
+  Proof.
+    verit_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_timeout 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_no_check_timeout (H0, HInd) 10.
+  Qed.
+
+  Goal P 3.
+  Proof.
+    verit_no_check_timeout 10.
+  Qed.
+End TimeoutProp.
-- 
cgit