diff --git a/doc/usage.rst b/doc/usage.rst
index 2386eb5a397742add7cf9977c9cfa4d37a77744d..9e00ec4c4d1f7670c3f5bfa4e0ccb2212bcd4e49 100644
--- a/doc/usage.rst
+++ b/doc/usage.rst
@@ -63,8 +63,9 @@ verbosity level allows logging with all tags enabled. To enable a particular
tag, use the option ``--ltag=TAG``, with ``TAG`` one of the following:
* ``Autodetect``: display the output of the autodetect routine of CAISAR described in :ref:`prover-registration`
-* ``Specification``: display the actual specification provided to the prover
-* ``CallProver``: display the actual command used to call the prover
+* ``ProverSpec``: display the actual specification provided to the prover
+* ``ProverCall``: display the actual command used to call the prover
+* ``StackTrace``: display the stack trace upon a CAISAR error
Built-in properties
-------------------
diff --git a/src/logging.ml b/src/logging.ml
index 2a2e4683972ec5c804f0fc2fd4a0cc7546423bc7..559260dad02f0314e6c04e53dde23a69200712c5 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -21,10 +21,16 @@
(**************************************************************************)
let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection"
-let src_spec = Logs.Src.create "Spec" ~doc:"Prover-tailored specification"
-let src_call = Logs.Src.create "Call" ~doc:"Call prover"
+
+let src_prover_spec =
+ Logs.Src.create "ProverSpec" ~doc:"Prover-tailored specification"
+
+let src_prover_call = Logs.Src.create "ProverCall" ~doc:"Prover call"
let src_stack_trace = Logs.Src.create "StackTrace" ~doc:"Print stack trace"
+let all_srcs () =
+ [ src_autodetect; src_prover_spec; src_prover_call; src_stack_trace ]
+
let is_debug_level src =
match Logs.Src.level src with Some Debug -> true | _ -> false
diff --git a/src/logging.mli b/src/logging.mli
index b957d9bb83b8dffdfc526b265d8147043e2e0d26..48e43c3b9e5caf1c36004dd8d25f6c58dea3d5e6 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -20,16 +20,19 @@
(* *)
(**************************************************************************)
-(** {2 Debug Tags} *)
-val src_autodetect : Logs.src
-
-val src_spec : Logs.src
-
-val src_call : Logs.src
+(** {2 Sources} *)
+val src_autodetect : Logs.src
+val src_prover_spec : Logs.src
+val src_prover_call : Logs.src
val src_stack_trace : Logs.src
+val all_srcs : unit -> Logs.src list
+(** @return all available sources. *)
+
(** {2 Logs} *)
val is_debug_level : Logs.src -> bool
-val setup : Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
+
+val setup :
+ Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit
diff --git a/src/main.ml b/src/main.ml
index 83d8014f166c48938a25871026e6398df421bf0f..ea8183c88a76f75d98ca87e414121255f09a8ab8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -37,7 +37,7 @@ let () =
(* -- Logs *)
let log_tags =
- let all_tags = Logs.Src.list () in
+ let all_tags = Logging.all_srcs () in
let doc =
Fmt.str "Logging tags. Available $(docv)s: %s."
(Arg.doc_alts
diff --git a/src/verification.ml b/src/verification.ml
index 2a2953b2ba468bf9c9c0d6dc38962b89018b3545..3aa186a85fd618af85a6e3538361b0d2d80580f9 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -22,7 +22,6 @@
open Why3
open Base
-module Filename = Caml.Filename
module File = struct
type t =
@@ -164,7 +163,7 @@ let build_command config_prover ~nn_filename =
let log_prover_task driver task =
let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
- Logs.debug ~src:Logging.src_spec (fun m ->
+ Logs.debug ~src:Logging.src_prover_spec (fun m ->
m "@[Prover-tailored specification:@.%a@]" print task)
let call_prover_on_task limit config command driver task =
@@ -302,7 +301,7 @@ let open_file ?format env file =
let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
file =
- let debug = Logging.(is_debug_level src_call) in
+ let debug = Logging.(is_debug_level src_prover_call) in
(if debug then Debug.(set_flag (lookup_flag "call_prover")));
let env, config = create_env loadpath in
let main = Whyconf.get_main config in
diff --git a/tests/cvc5.t b/tests/cvc5.t
index 7565e7c926ce3c48f372fdc510a8b09c9df4dc30..e55696f37171cd8dc25fa4c1a6da7d5c7d17c4d1 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --prover=CVC5 --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover=CVC5 --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory CVC5
> use TestNetworkONNX.AsTuple as TN
> use ieee_float.Float64
@@ -17,7 +17,7 @@ Test verify
> (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;; produced by cvc5.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
diff --git a/tests/dataset.t b/tests/dataset.t
index 4b2abb4da9e1f8bf2e9b9abd85e21d06aa663238..0e965840cde1604939d858d4ed9e0c710be4bd89 100644
--- a/tests/dataset.t
+++ b/tests/dataset.t
@@ -14,7 +14,7 @@ Test verify on dataset
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify -L . --format whyml --ltag=Spec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=PyRAT --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
> use ieee_float.Float64
@@ -27,7 +27,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -99,7 +99,7 @@ Test verify on dataset
(and (>= Y_4 Y_1))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -171,7 +171,7 @@ Test verify on dataset
(and (>= Y_4 Y_0))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -243,7 +243,7 @@ Test verify on dataset
(and (>= Y_4 Y_1))
))
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0
@@ -318,7 +318,7 @@ Test verify on dataset
Goal G: Unknown ()
Goal H: Unknown ()
- $ caisar verify -L . --format whyml --ltag=Spec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou --dataset=test_data.csv - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use TestNetwork.AsArray as TN
> use ieee_float.Float64
@@ -331,7 +331,7 @@ Test verify on dataset
> robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -344,7 +344,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -357,7 +357,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -370,7 +370,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y3 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.0
x1 >= 1.0
@@ -383,7 +383,7 @@ Test verify on dataset
x4 <= 0.776470588000000017103729987866245210170745849609375
+y4 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -396,7 +396,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -409,7 +409,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y2 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -422,7 +422,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y3 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.94117647100000001447739350624033249914646148681640625
x0 <= 0.94117647100000001447739350624033249914646148681640625
x1 >= 0.0
@@ -435,7 +435,7 @@ Test verify on dataset
x4 <= 0.0392156859999999996002628677160828374326229095458984375
+y4 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -448,7 +448,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -461,7 +461,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -474,7 +474,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y3 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.01000000000000000020816681711721685132943093776702880859375
x1 >= 0.9899999999999999911182158029987476766109466552734375
@@ -487,7 +487,7 @@ Test verify on dataset
x4 <= 0.7864705880000000259855141848674975335597991943359375
+y4 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -500,7 +500,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -513,7 +513,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y2 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
@@ -526,7 +526,7 @@ Test verify on dataset
x4 <= 0.049215686000000001543153160810106783173978328704833984375
+y3 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.93117647100000000559560930923908017575740814208984375
x0 <= 0.95117647100000002335917770324158482253551483154296875
x1 >= 0.0
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index af2dd1e2d2bf7eaf9bb3fd0560497f3ad2e62155..28695a744ada60305f2c3a18842df557ff5e74ce 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -7,7 +7,7 @@ Test interpret on acasxu
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -95,7 +95,7 @@ Test interpret on acasxu
> not (advises nn i clear_of_conflict)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
@@ -111,7 +111,7 @@ Test interpret on acasxu
x4 <= -0.450000000000000011102230246251565404236316680908203125
y0 <= 3.991125645861615112153231166303157806396484375
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
-0.328421367053318091766556108268559910356998443603515625 <= x0
x0 <= 0.67985927880386987087746319957659579813480377197265625
-0.499999999999967081887319864108576439321041107177734375 <= x1
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 2f0c09f69e9568f1d21997590e5124edb537149b..eb6ef3e756420ce07c278a303cb10e6e138722a2 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -11,7 +11,7 @@ Test interpret on dataset
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -53,7 +53,7 @@ Test interpret on dataset
> robust nn dataset eps
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -76,7 +76,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -99,7 +99,7 @@ Test interpret on dataset
x4 <= 1.151470588000000017103729987866245210170745849609375
+y2 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
@@ -122,7 +122,7 @@ Test interpret on dataset
x4 <= 1.159313725000000072640204962226562201976776123046875
+y1 -y0 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 1.0
x1 >= 0.0
diff --git a/tests/marabou.t b/tests/marabou.t
index f424b8e324b2c67bfc32f00c1a22fead2aae9dd6..8ded847e994ab771f5e3bf150ec3b166eaba270d 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=Marabou --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -41,17 +41,17 @@ Test verify
> (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 <= 0.0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
y0 >= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -59,21 +59,21 @@ Test verify
y0 <= 0.0
y0 <= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 <= 0.0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
x1 <= 1.0
y1 >= 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -81,7 +81,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.0
x0 <= 0.5
x1 >= 0.5
@@ -89,7 +89,7 @@ Test verify
+y1 -y0 >= 0
+y0 -y1 >= 0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
x0 >= 0.75
x0 <= 1.0
x1 >= 0.5
diff --git a/tests/pyrat.t b/tests/pyrat.t
index 20802e87f73209ee4e68af7944c5fad32e756e97..f34d87e691374242e9157fda35ac14909bdd0016 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT
> use TestNetwork.AsTuple
> use ieee_float.Float64
@@ -30,52 +30,52 @@ Test verify
> ((0.0:t) .< (nn@@i)[0] \/ (0.5:t) .< (nn@@i)[0]) /\ (0.0:t) .< (nn@@i)[1] .< (0.5:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.5 <= x1
x1 <= 1.0
y1 < 0.5
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
(0.0 < y0 or 0.5 < y0)
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
x1 <= 1.0
0.0 < y1
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.375 <= x0
x0 <= 0.75
0.5 <= x1
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index c0a18ae1f0a3d86d8d275f8dd5d6beba0a37a8fc..2c983e67eebfc3482421d316e73561bbd752c61a 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -6,7 +6,7 @@ Test verify
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify --format whyml --prover=PyRAT --ltag=Spec - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory PyRAT_ONNX
> use ieee_float.Float64
> use bool.Bool
@@ -23,12 +23,12 @@ Test verify
> (0.0:t) .< (nn@@i)[0] .< (0.5:t)
> end
> EOF
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
0.0 < y0
- [DEBUG]{Spec} Prover-tailored specification:
+ [DEBUG]{ProverSpec} Prover-tailored specification:
0.0 <= x0
x0 <= 0.5
y0 < 0.5
diff --git a/tests/verify_json.t b/tests/verify_json.t
index a0870299e3a848301559cfaef350e370b0e4747f..d34b2e3ddd27f695edcca33f6f12d661639dca02 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -14,8 +14,8 @@ Test verify-json
$ PATH=$(pwd)/bin:$PATH
- $ caisar verify-json --ltag=Spec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
- [DEBUG]{Spec} Prover-tailored specification:
+ $ caisar verify-json --ltag=ProverSpec config.json 2>&1 <<EOF | ./filter_tmpdir.sh
+ [DEBUG]{ProverSpec} Prover-tailored specification:
;;; produced by PyRAT/VNN-LIB driver
;;; produced by VNN-LIB driver
;; X_0