diff --git a/doc/usage.rst b/doc/usage.rst
index e7d339de274c4b58b9ae2c33ab37940c201ac559..9e00ec4c4d1f7670c3f5bfa4e0ccb2212bcd4e49 100644
--- a/doc/usage.rst
+++ b/doc/usage.rst
@@ -3,6 +3,15 @@
 Using CAISAR
 ============
 
+Commands summary
+----------------
+
+The CAISAR executable provide several subcommands, called
+using ``caisar [COMMAND]``. ``caisar --help`` provides a list of
+all available commands. Additionally, ``caisar [COMMAND] --help`` gives a synopsis for each available command.
+
+.. _prover-registration:
+
 Prover registration
 -------------------
 
@@ -10,37 +19,13 @@ CAISAR relies on external provers to work. You must install
 them first, then point CAISAR to their location. Please
 refer to each prover documentation to install them.
 
-Provers tend to be complex programs with multiple options.
-Some combination of options may be suited for one
-verification problem, while inefficient for another. As they
-also have different interface, it is also necessary to register
-their call in a way CAISAR can understand.
-To do so, you must register provers inside the ``config/caisar-detection-data.conf`` file.
-Each supported prover is registered by specifying the following fields:
-
-* ``name``: the name under which CAISAR will know the prover
-* ``exec``: the prover's executable name
-* ``alternative`` (optional): an alternative configuration for the
-  prover. To use it with CAISAR, use the option
-  ``--prover-altern``. Useful when you want to use the same
-  prover on different problems.
-* ``version_switch``: the command used to output the prover's
-  version
-* ``version_regexp``: a regular expression parsing the
-  output of ``version_switch``
-* ``version_ok``: CAISAR supported version of the prover.
-  Provers should only be used with their supported version.
-* ``command``: the actual command CAISAR will send to the prover. There are a few builtin expressions provided by CAISAR:
-
-  * ``%f``: the generated property file sent to the prover
-  * ``%t``: the timelimit value
-  * ``%{nnet-onnx}``: the name of the neural network file
-* ``driver``: location of the CAISAR driver for the prover, if any
-
-
-Assuming you have installed a prover and you filled the
+CAISAR
+already support several provers, listed in
+:ref:`overalldesign`.
+Assuming you have installed a prover with an entry in the
 ``caisar-detection.conf`` file, you can register the prover to CAISAR using the
 following command: ``PATH=$PATH:/path/to/solver/executable caisar config -d``.
+Your prover should be displayed with its relevant version.
 
 Property verification
 ---------------------
@@ -53,7 +38,7 @@ Example of WhyML are in the `source code <https://git.frama-c.com/pub/caisar/-/t
 You may also read the :ref:`examples` section of this
 documentation to get a first grasp on using WhyML.
 
-Provided a file `trust.why` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
+Provided a file ``trust.why`` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
 will verify the goals using the specified prover. A list of
 supported provers is available in :ref:`overalldesign`. The prover
 must already be registered by CAISAR. Currently, only one
@@ -64,6 +49,24 @@ Internally, CAISAR will translate the goals into a form that
 is acceptable by the targeted prover, generating a file (the
 ``%f`` defined in the previous section).
 
+Logging
+*******
+
+CAISAR provides different log verbosity levels. To change the log verbosity
+level, provide the option ``--verbosity`` to the ``verify`` command. Available
+levels are ``quiet``, ``error``, ``warning``, ``info`` and ``debug`` (defaults
+to ``warning``).
+
+CAISAR also provides log *tags*. Each tag adds additional information in the
+log, independently of the log verbosity level. However, note that the ``debug``
+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`
+* ``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
 -------------------
 In addition to all the theories provided by Why3, CAISAR
@@ -71,3 +74,36 @@ provide additional theories that model commonly desirable properties for machine
 All those predicates are located in the file ``stdlib/caisar.mlw``.
 Among them are theories to describe classification datasets,
 local and global robustness around a neighborhood.
+
+Advanced usage: registering a new prover
+----------------------------------------
+
+Provers tend to be complex programs with multiple options.
+Some combination of options may be suited for one
+verification problem, while inefficient for another. As they
+also have different interface, it is also necessary to register
+their call in a way CAISAR can understand.
+To do so, you must register provers inside the ``config/caisar-detection-data.conf`` file.
+Each supported prover is registered by specifying the following fields:
+
+* ``name``: the name under which CAISAR will know the prover
+* ``exec``: the prover's executable name
+* ``alternative`` (optional): an alternative configuration for the
+  prover. To use it with CAISAR, use the option
+  ``--prover-altern``. Useful when you want to use the same
+  prover on different problems.
+* ``version_switch``: the command used to output the prover's
+  version
+* ``version_regexp``: a regular expression parsing the
+  output of ``version_switch``
+* ``version_ok``: CAISAR supported version of the prover.
+  Provers should only be used with their supported version.
+* ``command``: the actual command CAISAR will send to the prover executable. There are a few builtin expressions provided by CAISAR:
+
+  * ``%f``: the generated property file sent to the prover
+  * ``%t``: the timelimit value
+  * ``%{nnet-onnx}``: the name of the neural network file
+* ``driver``: location of the CAISAR driver for the prover, if any
+
+If you add support for a new prover, consider opening a merge
+request on our `forge <https://git.frama-c.com/pub/caisar/-/merge_requests>`_!
diff --git a/src/autodetect.ml b/src/autodetect.ml
index a7f5c262e029882bcaa7a9c30240bb6900ddbe0e..3bc69960bba18c708226726b9fcb9b614745fbe2 100644
--- a/src/autodetect.ml
+++ b/src/autodetect.ml
@@ -23,8 +23,6 @@
 open Why3
 open Base
 
-let null = if Caml.Sys.unix then "/dev/null" else "NUL"
-
 let rec lookup_file dirs filename =
   match dirs with
   | [] -> raise Caml.Not_found
@@ -32,7 +30,8 @@ let rec lookup_file dirs filename =
     let file = Caml.Filename.concat dir filename in
     if Caml.Sys.file_exists file then file else lookup_file dirs filename
 
-let autodetection ?(debug = false) () =
+let autodetection () =
+  let debug = Logging.(is_debug_level src_autodetect) in
   if debug then Debug.set_flag Autodetection.debug;
   let caisar_conf =
     lookup_file Dirs.Sites.config "caisar-detection-data.conf"
@@ -50,6 +49,6 @@ let autodetection ?(debug = false) () =
       }
       :: acc)
   in
-  let config = Whyconf.init_config (Some null) in
+  let config = Whyconf.init_config (Some Caml.Filename.null) in
   let provers = Autodetection.compute_builtin_prover provers config data in
   Whyconf.set_provers config provers
diff --git a/src/autodetect.mli b/src/autodetect.mli
index ccd02cb04380aeb0a6a8fa50d1cc4010f42c9a20..540f357fe60835f3f0843ae15cd5cb34c938e3d5 100644
--- a/src/autodetect.mli
+++ b/src/autodetect.mli
@@ -20,7 +20,5 @@
 (*                                                                        *)
 (**************************************************************************)
 
-val autodetection : ?debug:bool -> unit -> Why3.Whyconf.config
-(** Perform the autodetection of provers.
-
-    @param debug activates debug information. *)
+val autodetection : unit -> Why3.Whyconf.config
+(** Perform the autodetection of provers. *)
diff --git a/src/convert_xgboost.ml b/src/convert_xgboost.ml
index c6cc71c31fa766dc2e1ce768fcee237b59da8476..5e54ede75d076da6e4daaf9e07d93496a85411e6 100644
--- a/src/convert_xgboost.ml
+++ b/src/convert_xgboost.ml
@@ -258,7 +258,7 @@ let prove_and_print ?memlimit ?timelimit env config prover task =
   Fmt.pr "result: %a@." Why3.Call_provers.print_prover_answer answer.pr_answer
 
 let verify ?memlimit ?timelimit ~xgboost ~dataset ~prover () =
-  let env, config = Verification.create_env ~debug:false [] in
+  let env, config = Verification.create_env [] in
   let task = None in
   let th_real = Why3.Env.read_theory env [ "real" ] "Real" in
   let task = Why3.Task.use_export task th_real in
diff --git a/src/dune b/src/dune
index 9d7cf5b389c6ee9705358ddf0ebdbc96b395fa61..013aad1ad73f2872edafa7fb997432b281d29898 100644
--- a/src/dune
+++ b/src/dune
@@ -9,6 +9,7 @@
   logs.cli
   logs.fmt
   fmt.tty
+  fmt.cli
   base
   unix
   str
diff --git a/src/logging.ml b/src/logging.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f15df62bc1de0e489d51a0b76536c93762f5895f
--- /dev/null
+++ b/src/logging.ml
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+let src_autodetect = Logs.Src.create "Autodetect" ~doc:"Prover autodetection"
+
+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
+
+let reporter =
+  let report src level ~over k msgf =
+    let k _ =
+      over ();
+      k ()
+    in
+    msgf @@ fun ?header ?tags:_ fmt ->
+    let ppf = if level = Logs.App then Fmt.stdout else Fmt.stderr in
+    let pp_src fmt src =
+      if Logs.Src.equal Logs.default src
+      then (if level <> Logs.App then Fmt.pf fmt " ")
+      else Fmt.pf fmt "@[{%s}@] " (Logs.Src.name src)
+    in
+    Format.kfprintf k ppf
+      ("%a%a@[" ^^ fmt ^^ "@]@.")
+      Logs_fmt.pp_header (level, header) pp_src src
+  in
+  { Logs.report }
+
+let setup style_renderer level srcs =
+  Logs.set_level ~all:true level;
+  List.iter (fun src -> Logs.Src.set_level src (Some Debug)) srcs;
+  Fmt_tty.setup_std_outputs ?style_renderer ();
+  Logs.set_reporter reporter
diff --git a/src/logging.mli b/src/logging.mli
new file mode 100644
index 0000000000000000000000000000000000000000..48e43c3b9e5caf1c36004dd8d25f6c58dea3d5e6
--- /dev/null
+++ b/src/logging.mli
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(*  Copyright (C) 2022                                                    *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  You can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** {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
diff --git a/src/main.ml b/src/main.ml
index 7498e10547a2fbc93ed902020d09bbdadc09a669..ea8183c88a76f75d98ca87e414121255f09a8ab8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -34,49 +34,37 @@ let () =
   Marabou.init ();
   Vnnlib.init ()
 
-(* -- Logs. *)
+(* -- Logs *)
 
-let pp_header =
-  let x =
-    match Array.length Caml.Sys.argv with
-    | 0 -> Caml.(Filename.basename Sys.executable_name)
-    | _ -> Caml.(Filename.basename Sys.argv.(0))
+let log_tags =
+  let all_tags = Logging.all_srcs () in
+  let doc =
+    Fmt.str "Logging tags. Available $(docv)s: %s."
+      (Arg.doc_alts
+         (List.map
+            ~f:(fun src ->
+              Fmt.str "%s (%s)" (Logs.Src.name src) (Logs.Src.doc src))
+            all_tags))
   in
-  let pp_h ppf style h = Fmt.pf ppf "[%s][%a] " x Fmt.(styled style string) h in
-  fun ppf (l, h) ->
-    let open Logs_fmt in
-    match l with
-    | Logs.App -> Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x
-    | Logs.Error ->
-      pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
-    | Logs.Warning ->
-      pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
-    | Logs.Info ->
-      pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
-    | Logs.Debug ->
-      pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
-
-let setup_logs =
-  let setup_log level =
-    Fmt_tty.setup_std_outputs ~style_renderer:`Ansi_tty ();
-    Logs.set_level level;
-    Logs.set_reporter (Logs_fmt.reporter ~pp_header ())
+  let enum_log_tags =
+    Arg.enum (List.map ~f:(fun c -> (Logs.Src.name c, c)) all_tags)
   in
-  Term.(const setup_log $ Logs_cli.level ())
+  Arg.(
+    value & opt_all enum_log_tags []
+    & info [ "log-tag"; "ltag" ] ~doc ~docv:"TAG")
 
-let log_level_is_debug () =
-  match Logs.level () with Some Debug -> true | _ -> false
+let setup_logs =
+  Term.(
+    const Logging.setup $ Fmt_cli.style_renderer () $ Logs_cli.level ()
+    $ log_tags)
 
-(* -- Commands. *)
+(* -- Commands *)
 
 let config detect () =
   if detect
   then (
     Logs.debug (fun m -> m "Automatic detection");
-    let config =
-      let debug = log_level_is_debug () in
-      Autodetect.autodetection ~debug ()
-    in
+    let config = Autodetect.autodetection () in
     let open Why3 in
     let provers = Whyconf.get_provers config in
     if not (Whyconf.Mprover.is_empty provers)
@@ -137,14 +125,13 @@ let log_theory_answer =
 
 let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
   files =
-  let debug = log_level_is_debug () in
   let memlimit = Option.map memlimit ~f:memlimit_of_string in
   let timelimit = Option.map timelimit ~f:timelimit_of_string in
   let theory_answers =
     List.map files
       ~f:
-        (Verification.verify ~debug ?format ~loadpath ?memlimit ?timelimit
-           ?dataset prover ?prover_altern)
+        (Verification.verify ?format ~loadpath ?memlimit ?timelimit ?dataset
+           prover ?prover_altern)
   in
   List.iter theory_answers ~f:log_theory_answer;
   theory_answers
@@ -438,5 +425,5 @@ let () =
     Cmd.group ~default:default_cmd default_info
       [ config_cmd; verify_cmd; verify_json_cmd; verify_xgboost_cmd ]
     |> Cmd.eval ~catch:false |> Caml.exit
-  with exn when not (log_level_is_debug ()) ->
+  with exn when not Logging.(is_debug_level src_stack_trace) ->
     Logs.err (fun m -> m "@[%a@]" Why3.Exn_printer.exn_printer exn)
diff --git a/src/verification.ml b/src/verification.ml
index 93df264486663c0db38594686c0586074025a705..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 =
@@ -74,8 +73,8 @@ let () =
   Language.register_onnx_support ();
   Language.register_ovo_support ()
 
-let create_env ?(debug = false) loadpath =
-  let config = Autodetect.autodetection ~debug () in
+let create_env loadpath =
+  let config = Autodetect.autodetection () in
   let config =
     let main = Whyconf.get_main config in
     let dft_timelimit = 20.0 (* 20 seconds *) in
@@ -162,7 +161,13 @@ let build_command config_prover ~nn_filename =
   in
   Re__Core.replace_string re_config ~by:config_site command
 
+let log_prover_task driver task =
+  let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
+  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 =
+  log_prover_task driver task;
   let prover_call =
     Driver.prove_task_prepared ~command ~config ~limit driver task
   in
@@ -294,10 +299,11 @@ let open_file ?format env file =
     let th = Json.theory_of_input env jin in
     (Unix.getcwd () (* TODO *), Wstdlib.Mstr.singleton th.th_name.id_string th)
 
-let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
-  prover ?prover_altern file =
-  if debug then Debug.set_flag (Debug.lookup_flag "call_prover");
-  let env, config = create_env ~debug loadpath in
+let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
+  file =
+  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
   let limit =
     let memlimit = Option.value memlimit ~default:(Whyconf.memlimit main) in
diff --git a/src/verification.mli b/src/verification.mli
index 645834243a14eae1befe979ff7e0083f3fc8656a..b6da390487261aa64221d12fbb7f76e7ff9d9f38 100644
--- a/src/verification.mli
+++ b/src/verification.mli
@@ -47,7 +47,6 @@ and additional_info = private
       (** A prover answer per data point. *)
 
 val verify :
-  ?debug:bool ->
   ?format:string ->
   loadpath:string list ->
   ?memlimit:int ->
@@ -61,7 +60,6 @@ val verify :
     launches a verification of the given [file] with the provided [prover] and
     [dataset].
 
-    @param debug when set, enables debug information.
     @param format is the [file] format.
     @param loadpath is the additional loadpath.
     @param memlimit
@@ -75,5 +73,4 @@ val verify :
       for each theory, an [answer] for each goal of the theory, respecting the
       order of appearance. *)
 
-val create_env :
-  ?debug:bool -> string list -> Why3.Env.env * Why3.Whyconf.config
+val create_env : string list -> Why3.Env.env * Why3.Whyconf.config
diff --git a/tests/aimos.t b/tests/aimos.t
index 1d53b28be70d30bd8d289b5c4a8806518ca8a475..0ac820383c49c20deff4bb1dbcc441a94ab251a2 100644
--- a/tests/aimos.t
+++ b/tests/aimos.t
@@ -22,4 +22,4 @@ Test verify
   >   goal G: meta_robust model dataset (1.0:t) ("reluplex_rotation":string) ("config/custom_transformations.py":string) ("classif_min":string) (0:int) (0:int) (0:int)
   > end
   > EOF
-  [caisar] Goal G: Valid
+  Goal G: Valid
diff --git a/tests/autodetect.t b/tests/autodetect.t
index cd2e8efe01d966b015262f540b62f7773338cf02..5fee7ec434876b149122756fbe86229d36456e81 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -32,9 +32,7 @@ Test autodetect
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar config -d -vv 2>&1 | ./filter_tmpdir.sh
-  [caisar][DEBUG] Execution of command 'config'
-  [caisar][DEBUG] Automatic detection
+  $ caisar config -d --ltag=Autodetect -v 2>&1 | ./filter_tmpdir.sh
   <autodetect>Run: ($TESTCASE_ROOT/bin/nnenum.sh --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Run: ($TESTCASE_ROOT/bin/saver --version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)) > $TMPFILE 2>&1
@@ -57,14 +55,14 @@ Test autodetect
   <autodetect>Found prover SAVer version v1.0, OK.
   <autodetect>Found prover AIMOS version 1.0, OK.
   <autodetect>11 prover(s) added
-  [caisar] AIMOS 1.0
-           Alt-Ergo 2.4.0
-           CVC5 1.0.2
-           Marabou 1.0.+
-           PyRAT 1.1
-           PyRAT 1.1 (ACAS)
-           PyRAT 1.1 (VNNLIB)
-           SAVer v1.0
-           alpha-beta-CROWN dummy-version
-           alpha-beta-CROWN dummy-version (ACAS)
-           nnenum dummy-version
+  AIMOS 1.0
+  Alt-Ergo 2.4.0
+  CVC5 1.0.2
+  Marabou 1.0.+
+  PyRAT 1.1
+  PyRAT 1.1 (ACAS)
+  PyRAT 1.1 (VNNLIB)
+  SAVer v1.0
+  alpha-beta-CROWN dummy-version
+  alpha-beta-CROWN dummy-version (ACAS)
+  nnenum dummy-version
diff --git a/tests/cvc5.t b/tests/cvc5.t
index bfca315af103b8232b3293d9914386d7a0841d60..e55696f37171cd8dc25fa4c1a6da7d5c7d17c4d1 100644
--- a/tests/cvc5.t
+++ b/tests/cvc5.t
@@ -6,8 +6,8 @@ Test verify
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover=CVC5 - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
+  $ 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,4 +17,218 @@ Test verify
   >      (0.0:t) .< y1 .< (0.5:t) /\ (0.0:t) .< y2 .< (1.0:t)
   > end
   > EOF
-  [caisar] Goal G: Unknown (unknown)
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;; produced by cvc5.drv ;;
+  (set-logic ALL)
+  (set-info :smt-lib-version 2.6)
+  ;;; generated by SMT-LIB2 driver
+  ;;; SMT-LIB2 driver: bit-vectors, common part
+  ;;; SMT-LIB2: integer arithmetic
+  ;;; SMT-LIB2: real arithmetic
+  (define-fun fp.isFinite64 ((x Float64)) Bool (not (or (fp.isInfinite x) (fp.isNaN x))))
+  (define-fun fp.isIntegral64 ((x Float64)) Bool (or (fp.isZero x) (and (fp.isNormal x) (= x (fp.roundToIntegral RNE x)))))
+  (declare-sort uni 0)
+  
+  (declare-sort ty 0)
+  
+  ;; "sort"
+  (declare-fun sort (ty
+    uni) Bool)
+  
+  ;; "witness"
+  (declare-fun witness (ty) uni)
+  
+  ;; "witness_sort"
+  (assert (forall ((a ty)) (sort a (witness a))))
+  
+  ;; "int"
+  (declare-fun int () ty)
+  
+  ;; "real"
+  (declare-fun real () ty)
+  
+  ;; "t"
+  (declare-fun t () ty)
+  
+  ;; "mode"
+  (declare-fun mode () ty)
+  
+  ;; "add_div"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=> (not (= z 0.0)) (= (/ (+ x y) z) (+ (/ x z) (/ y z))))))
+  
+  ;; "sub_div"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=> (not (= z 0.0)) (= (/ (- x y) z) (- (/ x z) (/ y z))))))
+  
+  ;; "neg_div"
+  (assert
+    (forall ((x Real) (y Real))
+      (=> (not (= y 0.0)) (= (/ (- x) y) (- (/ x y))))))
+  
+  ;; "assoc_mul_div"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=> (not (= z 0.0)) (= (/ (* x y) z) (* x (/ y z))))))
+  
+  ;; "assoc_div_mul"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=>
+        (and (not (= y 0.0)) (not (= z 0.0)))
+        (= (/ (/ x y) z) (/ x (* y z))))))
+  
+  ;; "assoc_div_div"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=>
+        (and (not (= y 0.0)) (not (= z 0.0)))
+        (= (/ x (/ y z)) (/ (* x z) y)))))
+  
+  ;; "CompatOrderMult"
+  (assert
+    (forall ((x Real) (y Real) (z Real))
+      (=> (<= x y) (=> (<= 0.0 z) (<= (* x z) (* y z))))))
+  
+  ;; "max_real"
+  (declare-fun max_real () Real)
+  
+  ;; "max_int"
+  (declare-fun max_int () Int)
+  
+  ;; "sqr"
+  (declare-fun sqr (Real) Real)
+  
+  ;; "sqr'def"
+  (assert (forall ((x Real)) (= (sqr x) (* x x))))
+  
+  ;; "sqrt"
+  (declare-fun sqrt1 (Real) Real)
+  
+  ;; "Sqrt_positive"
+  (assert (forall ((x Real)) (=> (<= 0.0 x) (<= 0.0 (sqrt1 x)))))
+  
+  ;; "Sqrt_square"
+  (assert (forall ((x Real)) (=> (<= 0.0 x) (= (sqr (sqrt1 x)) x))))
+  
+  ;; "Square_sqrt"
+  (assert (forall ((x Real)) (=> (<= 0.0 x) (= (sqrt1 (* x x)) x))))
+  
+  ;; "Sqrt_mul"
+  (assert
+    (forall ((x Real) (y Real))
+      (=>
+        (and (<= 0.0 x) (<= 0.0 y))
+        (= (sqrt1 (* x y)) (* (sqrt1 x) (sqrt1 y))))))
+  
+  ;; "Sqrt_le"
+  (assert
+    (forall ((x Real) (y Real))
+      (=> (and (<= 0.0 x) (<= x y)) (<= (sqrt1 x) (sqrt1 y)))))
+  
+  ;; "relu"
+  (declare-fun relu (Float64) Float64)
+  
+  ;; "relu'def"
+  (assert
+    (forall ((a Float64))
+      (ite (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) a)
+        (= (relu a) a)
+        (= (relu a) (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)))))
+  
+  (declare-datatypes ((tuple2 2))
+    ((par (a a1) ((Tuple2 (Tuple2_proj a)(Tuple2_proj1 a1))))))
+  
+  ;; "tuple2"
+  (declare-fun tuple21 (ty
+    ty) ty)
+  
+  ;; "Tuple2"
+  (declare-fun Tuple21 (ty
+    ty
+    uni
+    uni) uni)
+  
+  ;; "Tuple2_sort"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((x uni) (x1 uni)) (sort (tuple21 a3 a2) (Tuple21 a3 a2 x x1)))))
+  
+  ;; "Tuple2_proj_1"
+  (declare-fun Tuple2_proj_1 (ty
+    ty
+    uni) uni)
+  
+  ;; "Tuple2_proj_1_sort"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((x uni)) (sort a3 (Tuple2_proj_1 a3 a2 x)))))
+  
+  ;; "Tuple2_proj_1'def"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((u uni) (u1 uni))
+        (=> (sort a3 u) (= (Tuple2_proj_1 a3 a2 (Tuple21 a3 a2 u u1)) u)))))
+  
+  ;; "Tuple2_proj_2"
+  (declare-fun Tuple2_proj_2 (ty
+    ty
+    uni) uni)
+  
+  ;; "Tuple2_proj_2_sort"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((x uni)) (sort a2 (Tuple2_proj_2 a3 a2 x)))))
+  
+  ;; "Tuple2_proj_2'def"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((u uni) (u1 uni))
+        (=> (sort a2 u1) (= (Tuple2_proj_2 a3 a2 (Tuple21 a3 a2 u u1)) u1)))))
+  
+  ;; "tuple2_inversion"
+  (assert
+    (forall ((a2 ty) (a3 ty))
+      (forall ((u uni))
+        (=>
+          (sort (tuple21 a3 a2) u)
+          (= u (Tuple21 a3 a2 (Tuple2_proj_1 a3 a2 u) (Tuple2_proj_2 a3 a2 u)))))))
+  
+  ;; Goal "G"
+  ;; File "stdin", line 5, characters 7-8
+  (assert
+    (not
+    (forall ((x1 Float64) (x2 Float64) (x3 Float64))
+      (=>
+        (and
+          (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x1)
+          (fp.lt x1 (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
+        (match (let ((n_id_1_2 x3))
+                 (let ((n_id_1_1 x2))
+                   (let ((n_id_1_0 x1))
+                     (let ((n_id_2_1 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
+                       (let ((n_id_2_0 (fp.add RNE (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_1_0 (fp #b1 #b01111111100 #b0010110110101110110001100000000000000000000000000000))) (fp.mul RNE n_id_1_1 (fp #b0 #b01111111100 #b0001010101101010011100100000000000000000000000000000))) (fp.mul RNE n_id_1_2 (fp #b1 #b01111111100 #b0001110001000101101000100000000000000000000000000000)))))
+                         (let ((n_id_3_1 (fp.add RNE n_id_2_1 (fp #b1 #b01111111110 #b0001011011111110000011100000000000000000000000000000))))
+                           (let ((n_id_3_0 (fp.add RNE n_id_2_0 (fp #b0 #b01111111101 #b0110010010001010001001100000000000000000000000000000))))
+                             (let ((n_id_4_1 (relu n_id_3_1)))
+                               (let ((n_id_4_0 (relu n_id_3_0)))
+                                 (let ((n_id_5_1 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
+                                   (let ((n_id_5_0 (fp.add RNE (fp.add RNE (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) (fp.mul RNE n_id_4_0 (fp #b1 #b01111111101 #b0111110011110010111010000000000000000000000000000000))) (fp.mul RNE n_id_4_1 (fp #b0 #b01111111110 #b0100011001000110100010000000000000000000000000000000)))))
+                                     (let ((n_id_6_1 (fp.add RNE n_id_5_1 (fp #b1 #b01111111110 #b0011101101010011010001100000000000000000000000000000))))
+                                       (let ((n_id_6_0 (fp.add RNE n_id_5_0 (fp #b0 #b01111111110 #b0011000001100111100001000000000000000000000000000000))))
+                                         (let ((y2 n_id_6_1))
+                                           (let ((y1 n_id_6_0)) (Tuple2 y1 y2)))))))))))))))) (
+          ((Tuple2 x x4) (and
+                           (and
+                             (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x)
+                             (fp.lt x (fp #b0 #b01111111110 #b0000000000000000000000000000000000000000000000000000)))
+                           (and
+                             (fp.lt (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000) x4)
+                             (fp.lt x4 (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000)))))))))))
+  
+  (check-sat)
+  (get-info :reason-unknown)
+  
+  Goal G: Unknown (unknown)
diff --git a/tests/dataset.t b/tests/dataset.t
index 33e886ed577adfb7608d5b9dbdf8277ac72c1e18..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 --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,10 +27,298 @@ Test verify on dataset
   >    robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
   > end
   > EOF
-  [caisar] Goal G: Unknown ()
-  [caisar] Goal H: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; axiom_ge_x0
+  (assert (>= X_0 0.0))
+  
+  ;; axiom_le_x0
+  (assert (<= X_0 0.0))
+  
+  ;; axiom_ge_x1
+  (assert (>= X_1 1.0))
+  
+  ;; axiom_le_x1
+  (assert (<= X_1 1.0))
+  
+  ;; axiom_ge_x2
+  (assert (>= X_2 0.78431372499999996161790249971090815961360931396484375))
+  
+  ;; axiom_le_x2
+  (assert (<= X_2 0.78431372499999996161790249971090815961360931396484375))
+  
+  ;; axiom_ge_x3
+  (assert (>= X_3 0.01960784299999999980013143385804141871631145477294921875))
+  
+  ;; axiom_le_x3
+  (assert (<= X_3 0.01960784299999999980013143385804141871631145477294921875))
+  
+  ;; axiom_ge_x4
+  (assert (>= X_4 0.776470588000000017103729987866245210170745849609375))
+  
+  ;; axiom_le_x4
+  (assert (<= X_4 0.776470588000000017103729987866245210170745849609375))
+  
+  ;; Goal correct_record0_y1
+  (assert
+    (or
+      (and (>= Y_0 Y_1))
+      (and (>= Y_2 Y_1))
+      (and (>= Y_3 Y_1))
+      (and (>= Y_4 Y_1))
+      ))
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; axiom_ge_x0
+  (assert (>= X_0 0.94117647100000001447739350624033249914646148681640625))
+  
+  ;; axiom_le_x0
+  (assert (<= X_0 0.94117647100000001447739350624033249914646148681640625))
+  
+  ;; axiom_ge_x1
+  (assert (>= X_1 0.0))
+  
+  ;; axiom_le_x1
+  (assert (<= X_1 0.0))
+  
+  ;; axiom_ge_x2
+  (assert (>= X_2 0.0))
+  
+  ;; axiom_le_x2
+  (assert (<= X_2 0.0))
+  
+  ;; axiom_ge_x3
+  (assert (>= X_3 0.01176470599999999977480769075555144809186458587646484375))
+  
+  ;; axiom_le_x3
+  (assert (<= X_3 0.01176470599999999977480769075555144809186458587646484375))
+  
+  ;; axiom_ge_x4
+  (assert (>= X_4 0.0392156859999999996002628677160828374326229095458984375))
+  
+  ;; axiom_le_x4
+  (assert (<= X_4 0.0392156859999999996002628677160828374326229095458984375))
+  
+  ;; Goal correct_record1_y0
+  (assert
+    (or
+      (and (>= Y_1 Y_0))
+      (and (>= Y_2 Y_0))
+      (and (>= Y_3 Y_0))
+      (and (>= Y_4 Y_0))
+      ))
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; axiom_ge_x0
+  (assert (>= X_0 0.0))
+  
+  ;; axiom_le_x0
+  (assert (<= X_0 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; axiom_ge_x1
+  (assert (>= X_1 0.9899999999999999911182158029987476766109466552734375))
+  
+  ;; axiom_le_x1
+  (assert (<= X_1 1.0))
+  
+  ;; axiom_ge_x2
+  (assert (>= X_2 0.77431372499999995273611830270965583622455596923828125))
+  
+  ;; axiom_le_x2
+  (assert (<= X_2 0.79431372499999997049968669671216048300266265869140625))
+  
+  ;; axiom_ge_x3
+  (assert (>= X_3 0.00960784299999999959196461674082456738688051700592041015625))
+  
+  ;; axiom_le_x3
+  (assert (<= X_3 0.029607843000000001743021726952065364457666873931884765625))
+  
+  ;; axiom_ge_x4
+  (assert (>= X_4 0.7664705880000000082219457908649928867816925048828125))
+  
+  ;; axiom_le_x4
+  (assert (<= X_4 0.7864705880000000259855141848674975335597991943359375))
+  
+  ;; Goal robust_record0_y1
+  (assert
+    (or
+      (and (>= Y_0 Y_1))
+      (and (>= Y_2 Y_1))
+      (and (>= Y_3 Y_1))
+      (and (>= Y_4 Y_1))
+      ))
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  ;;; produced by PyRAT/VNN-LIB driver
+  ;;; produced by VNN-LIB driver
+  ;; X_0
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; axiom_ge_x0
+  (assert (>= X_0 0.93117647100000000559560930923908017575740814208984375))
+  
+  ;; axiom_le_x0
+  (assert (<= X_0 0.95117647100000002335917770324158482253551483154296875))
+  
+  ;; axiom_ge_x1
+  (assert (>= X_1 0.0))
+  
+  ;; axiom_le_x1
+  (assert (<= X_1 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; axiom_ge_x2
+  (assert (>= X_2 0.0))
+  
+  ;; axiom_le_x2
+  (assert (<= X_2 0.01000000000000000020816681711721685132943093776702880859375))
+  
+  ;; axiom_ge_x3
+  (assert (>= X_3 0.00176470599999999956664087363833459676243364810943603515625))
+  
+  ;; axiom_le_x3
+  (assert (<= X_3 0.021764706000000001717697983849575393833220005035400390625))
+  
+  ;; axiom_ge_x4
+  (assert (>= X_4 0.029215685999999997657372574622058891691267490386962890625))
+  
+  ;; axiom_le_x4
+  (assert (<= X_4 0.049215686000000001543153160810106783173978328704833984375))
+  
+  ;; Goal robust_record1_y0
+  (assert
+    (or
+      (and (>= Y_1 Y_0))
+      (and (>= Y_2 Y_0))
+      (and (>= Y_3 Y_0))
+      (and (>= Y_4 Y_0))
+      ))
+  
+  Goal G: Unknown ()
+  Goal H: Unknown ()
 
-  $ caisar verify -L . --format whyml --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
@@ -43,5 +331,213 @@ Test verify on dataset
   >    robust TN.model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
   > end
   > EOF
-  [caisar] Goal G: Unknown ()
-  [caisar] Goal H: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.0
+  x1 >= 1.0
+  x1 <= 1.0
+  x2 >= 0.78431372499999996161790249971090815961360931396484375
+  x2 <= 0.78431372499999996161790249971090815961360931396484375
+  x3 >= 0.01960784299999999980013143385804141871631145477294921875
+  x3 <= 0.01960784299999999980013143385804141871631145477294921875
+  x4 >= 0.776470588000000017103729987866245210170745849609375
+  x4 <= 0.776470588000000017103729987866245210170745849609375
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.0
+  x1 >= 1.0
+  x1 <= 1.0
+  x2 >= 0.78431372499999996161790249971090815961360931396484375
+  x2 <= 0.78431372499999996161790249971090815961360931396484375
+  x3 >= 0.01960784299999999980013143385804141871631145477294921875
+  x3 <= 0.01960784299999999980013143385804141871631145477294921875
+  x4 >= 0.776470588000000017103729987866245210170745849609375
+  x4 <= 0.776470588000000017103729987866245210170745849609375
+  +y2 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.0
+  x1 >= 1.0
+  x1 <= 1.0
+  x2 >= 0.78431372499999996161790249971090815961360931396484375
+  x2 <= 0.78431372499999996161790249971090815961360931396484375
+  x3 >= 0.01960784299999999980013143385804141871631145477294921875
+  x3 <= 0.01960784299999999980013143385804141871631145477294921875
+  x4 >= 0.776470588000000017103729987866245210170745849609375
+  x4 <= 0.776470588000000017103729987866245210170745849609375
+  +y3 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.0
+  x1 >= 1.0
+  x1 <= 1.0
+  x2 >= 0.78431372499999996161790249971090815961360931396484375
+  x2 <= 0.78431372499999996161790249971090815961360931396484375
+  x3 >= 0.01960784299999999980013143385804141871631145477294921875
+  x3 <= 0.01960784299999999980013143385804141871631145477294921875
+  x4 >= 0.776470588000000017103729987866245210170745849609375
+  x4 <= 0.776470588000000017103729987866245210170745849609375
+  +y4 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.94117647100000001447739350624033249914646148681640625
+  x0 <= 0.94117647100000001447739350624033249914646148681640625
+  x1 >= 0.0
+  x1 <= 0.0
+  x2 >= 0.0
+  x2 <= 0.0
+  x3 >= 0.01176470599999999977480769075555144809186458587646484375
+  x3 <= 0.01176470599999999977480769075555144809186458587646484375
+  x4 >= 0.0392156859999999996002628677160828374326229095458984375
+  x4 <= 0.0392156859999999996002628677160828374326229095458984375
+  +y1 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.94117647100000001447739350624033249914646148681640625
+  x0 <= 0.94117647100000001447739350624033249914646148681640625
+  x1 >= 0.0
+  x1 <= 0.0
+  x2 >= 0.0
+  x2 <= 0.0
+  x3 >= 0.01176470599999999977480769075555144809186458587646484375
+  x3 <= 0.01176470599999999977480769075555144809186458587646484375
+  x4 >= 0.0392156859999999996002628677160828374326229095458984375
+  x4 <= 0.0392156859999999996002628677160828374326229095458984375
+  +y2 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.94117647100000001447739350624033249914646148681640625
+  x0 <= 0.94117647100000001447739350624033249914646148681640625
+  x1 >= 0.0
+  x1 <= 0.0
+  x2 >= 0.0
+  x2 <= 0.0
+  x3 >= 0.01176470599999999977480769075555144809186458587646484375
+  x3 <= 0.01176470599999999977480769075555144809186458587646484375
+  x4 >= 0.0392156859999999996002628677160828374326229095458984375
+  x4 <= 0.0392156859999999996002628677160828374326229095458984375
+  +y3 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.94117647100000001447739350624033249914646148681640625
+  x0 <= 0.94117647100000001447739350624033249914646148681640625
+  x1 >= 0.0
+  x1 <= 0.0
+  x2 >= 0.0
+  x2 <= 0.0
+  x3 >= 0.01176470599999999977480769075555144809186458587646484375
+  x3 <= 0.01176470599999999977480769075555144809186458587646484375
+  x4 >= 0.0392156859999999996002628677160828374326229095458984375
+  x4 <= 0.0392156859999999996002628677160828374326229095458984375
+  +y4 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x1 >= 0.9899999999999999911182158029987476766109466552734375
+  x1 <= 1.0
+  x2 >= 0.77431372499999995273611830270965583622455596923828125
+  x2 <= 0.79431372499999997049968669671216048300266265869140625
+  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
+  x3 <= 0.029607843000000001743021726952065364457666873931884765625
+  x4 >= 0.7664705880000000082219457908649928867816925048828125
+  x4 <= 0.7864705880000000259855141848674975335597991943359375
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x1 >= 0.9899999999999999911182158029987476766109466552734375
+  x1 <= 1.0
+  x2 >= 0.77431372499999995273611830270965583622455596923828125
+  x2 <= 0.79431372499999997049968669671216048300266265869140625
+  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
+  x3 <= 0.029607843000000001743021726952065364457666873931884765625
+  x4 >= 0.7664705880000000082219457908649928867816925048828125
+  x4 <= 0.7864705880000000259855141848674975335597991943359375
+  +y2 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x1 >= 0.9899999999999999911182158029987476766109466552734375
+  x1 <= 1.0
+  x2 >= 0.77431372499999995273611830270965583622455596923828125
+  x2 <= 0.79431372499999997049968669671216048300266265869140625
+  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
+  x3 <= 0.029607843000000001743021726952065364457666873931884765625
+  x4 >= 0.7664705880000000082219457908649928867816925048828125
+  x4 <= 0.7864705880000000259855141848674975335597991943359375
+  +y3 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x1 >= 0.9899999999999999911182158029987476766109466552734375
+  x1 <= 1.0
+  x2 >= 0.77431372499999995273611830270965583622455596923828125
+  x2 <= 0.79431372499999997049968669671216048300266265869140625
+  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
+  x3 <= 0.029607843000000001743021726952065364457666873931884765625
+  x4 >= 0.7664705880000000082219457908649928867816925048828125
+  x4 <= 0.7864705880000000259855141848674975335597991943359375
+  +y4 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.93117647100000000559560930923908017575740814208984375
+  x0 <= 0.95117647100000002335917770324158482253551483154296875
+  x1 >= 0.0
+  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x2 >= 0.0
+  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
+  x3 <= 0.021764706000000001717697983849575393833220005035400390625
+  x4 >= 0.029215685999999997657372574622058891691267490386962890625
+  x4 <= 0.049215686000000001543153160810106783173978328704833984375
+  +y1 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.93117647100000000559560930923908017575740814208984375
+  x0 <= 0.95117647100000002335917770324158482253551483154296875
+  x1 >= 0.0
+  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x2 >= 0.0
+  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
+  x3 <= 0.021764706000000001717697983849575393833220005035400390625
+  x4 >= 0.029215685999999997657372574622058891691267490386962890625
+  x4 <= 0.049215686000000001543153160810106783173978328704833984375
+  +y2 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.93117647100000000559560930923908017575740814208984375
+  x0 <= 0.95117647100000002335917770324158482253551483154296875
+  x1 >= 0.0
+  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x2 >= 0.0
+  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
+  x3 <= 0.021764706000000001717697983849575393833220005035400390625
+  x4 >= 0.029215685999999997657372574622058891691267490386962890625
+  x4 <= 0.049215686000000001543153160810106783173978328704833984375
+  +y3 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.93117647100000000559560930923908017575740814208984375
+  x0 <= 0.95117647100000002335917770324158482253551483154296875
+  x1 >= 0.0
+  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x2 >= 0.0
+  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
+  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
+  x3 <= 0.021764706000000001717697983849575393833220005035400390625
+  x4 >= 0.029215685999999997657372574622058891691267490386962890625
+  x4 <= 0.049215686000000001543153160810106783173978328704833984375
+  +y4 -y0 >= 0
+  
+  Goal G: Unknown ()
+  Goal H: Unknown ()
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 8591192094f156eba26c4a530922313d44a4557f..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 -L . --format whyml --prover PyRAT - 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,5 +95,41 @@ Test interpret on acasxu
   >       not (advises nn i clear_of_conflict)
   > end
   > EOF
-  [caisar] Goal P1: Unknown ()
-  [caisar] Goal P3: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  -0.328421367053318091766556108268559910356998443603515625 <= x0
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  -0.499999999999967081887319864108576439321041107177734375 <= x1
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  -0.499999999999967081887319864108576439321041107177734375 <= x2
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  -0.5 <= x3
+  x3 <= 0.5
+  -0.5 <= x4
+  x4 <= 0.5
+  0.60000151009774149724051994780893437564373016357421875 <= x0
+  0.450000000000000011102230246251565404236316680908203125 <= x3
+  x4 <= -0.450000000000000011102230246251565404236316680908203125
+  y0 <= 3.991125645861615112153231166303157806396484375
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  -0.328421367053318091766556108268559910356998443603515625 <= x0
+  x0 <= 0.67985927880386987087746319957659579813480377197265625
+  -0.499999999999967081887319864108576439321041107177734375 <= x1
+  x1 <= 0.499999999999967081887319864108576439321041107177734375
+  -0.499999999999967081887319864108576439321041107177734375 <= x2
+  x2 <= 0.499999999999967081887319864108576439321041107177734375
+  -0.5 <= x3
+  x3 <= 0.5
+  -0.5 <= x4
+  x4 <= 0.5
+  -0.303529646039727207806890874053351581096649169921875 <= x0
+  x0 <= -0.298551301837009008810497334707179106771945953369140625
+  -0.0095492965855130916563719978285007528029382228851318359375 <= x1
+  x1 <= 0.0095492965855130916563719978285007528029382228851318359375
+  0.493380323584843072382000173092819750308990478515625 <= x2
+  0.299999999999999988897769753748434595763683319091796875 <= x3
+  0.299999999999999988897769753748434595763683319091796875 <= x4
+  (((y0 >= y1 or y0 >= y2) or y0 >= y3) or y0 >= y4)
+  
+  Goal P1: Unknown ()
+  Goal P3: Unknown ()
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 9996b4544ebb90ec070a0730f800f908427f9a1e..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 -L . --format whyml --prover Marabou - 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,4 +53,96 @@ Test interpret on dataset
   >     robust nn dataset eps
   > end
   > EOF
-  [caisar] Goal G: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.375
+  x0 <= 0.375
+  x1 >= 0.625
+  x1 <= 1.375
+  x2 >= 0.40931372499999996161790249971090815961360931396484375
+  x2 <= 1.159313725000000072640204962226562201976776123046875
+  x3 >= -0.355392156999999986322080758327501825988292694091796875
+  x3 <= 0.394607843000000013677919241672498174011707305908203125
+  x4 >= 0.401470588000000017103729987866245210170745849609375
+  x4 <= 1.151470588000000017103729987866245210170745849609375
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= -0.375
+  x0 <= 0.375
+  x1 >= 0.625
+  x1 <= 1.375
+  x2 >= 0.40931372499999996161790249971090815961360931396484375
+  x2 <= 1.159313725000000072640204962226562201976776123046875
+  x3 >= -0.355392156999999986322080758327501825988292694091796875
+  x3 <= 0.394607843000000013677919241672498174011707305908203125
+  x4 >= 0.401470588000000017103729987866245210170745849609375
+  x4 <= 1.151470588000000017103729987866245210170745849609375
+  +y2 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= 0.625
+  x0 <= 1.375
+  x1 >= -0.375
+  x1 <= 0.375
+  x2 >= -0.355392156999999986322080758327501825988292694091796875
+  x2 <= 0.394607843000000013677919241672498174011707305908203125
+  x3 >= 0.401470588000000017103729987866245210170745849609375
+  x3 <= 1.151470588000000017103729987866245210170745849609375
+  x4 >= 0.40931372499999996161790249971090815961360931396484375
+  x4 <= 1.159313725000000072640204962226562201976776123046875
+  +y1 -y0 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 1.0
+  x1 >= 0.0
+  x1 <= 1.0
+  x2 >= 0.0
+  x2 <= 1.0
+  x3 >= 0.0
+  x3 <= 1.0
+  x4 >= 0.0
+  x4 <= 1.0
+  x0 >= 0.625
+  x0 <= 1.375
+  x1 >= -0.375
+  x1 <= 0.375
+  x2 >= -0.355392156999999986322080758327501825988292694091796875
+  x2 <= 0.394607843000000013677919241672498174011707305908203125
+  x3 >= 0.401470588000000017103729987866245210170745849609375
+  x3 <= 1.151470588000000017103729987866245210170745849609375
+  x4 >= 0.40931372499999996161790249971090815961360931396484375
+  x4 <= 1.159313725000000072640204962226562201976776123046875
+  +y2 -y0 >= 0
+  
+  Goal G: Unknown ()
diff --git a/tests/marabou.t b/tests/marabou.t
index 77ba163cb9b56bbb617b773ef0e6d43e230fd398..8ded847e994ab771f5e3bf150ec3b166eaba270d 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -6,7 +6,7 @@ Test verify
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover=Marabou - 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,7 +41,63 @@ Test verify
   >       (nn@@i)[1] .< (nn@@i)[0] \/ (nn@@i)[0] .< (nn@@i)[1]
   > end
   > EOF
-  [caisar] Goal G: Unknown ()
-  [caisar] Goal H: Unknown ()
-  [caisar] Goal I: Unknown ()
-  [caisar] Goal J: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  y0 <= 0.0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  y0 >= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y0 <= 0.0
+  y0 <= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y1 <= 0.0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  y1 >= 0.5
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.0
+  x0 <= 0.5
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  x0 >= 0.75
+  x0 <= 1.0
+  x1 >= 0.5
+  x1 <= 1.0
+  +y1 -y0 >= 0
+  +y0 -y1 >= 0
+  
+  Goal G: Unknown ()
+  Goal H: Unknown ()
+  Goal I: Unknown ()
+  Goal J: Unknown ()
diff --git a/tests/pyrat.t b/tests/pyrat.t
index a59926ecb618a534ee79a8641c9b2308895ea5d7..f34d87e691374242e9157fda35ac14909bdd0016 100644
--- a/tests/pyrat.t
+++ b/tests/pyrat.t
@@ -6,8 +6,9 @@ Test verify
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
+  $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
+  > theory PyRAT
+  >   use TestNetwork.AsTuple
   >   use ieee_float.Float64
   >   use bool.Bool
   >   use int.Int
@@ -29,5 +30,57 @@ 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
-  [caisar] Goal G: Unknown ()
-  [caisar] Goal H: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  0.0 <  y0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  y0 <  0.5
+  
+  [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]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  0.5 <= x1
+  x1 <= 1.0
+  0.0 <  y1
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  0.5 <= x1
+  x1 <= 1.0
+  y1 <  0.5
+  
+  [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]{ProverSpec} Prover-tailored specification:
+  0.375 <= x0
+  x0 <= 0.75
+  0.5 <= x1
+  x1 <= 1.0
+  0.0 <  y1
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.375 <= x0
+  x0 <= 0.75
+  0.5 <= x1
+  x1 <= 1.0
+  y1 <  0.5
+  
+  Goal G: Unknown ()
+  Goal H: Unknown ()
diff --git a/tests/pyrat_onnx.t b/tests/pyrat_onnx.t
index 168624e46fc7bc5a52b255cd871d286a4bbe9f1b..2c983e67eebfc3482421d316e73561bbd752c61a 100644
--- a/tests/pyrat_onnx.t
+++ b/tests/pyrat_onnx.t
@@ -6,8 +6,8 @@ Test verify
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
+  $ caisar verify --format whyml --prover=PyRAT --ltag=ProverSpec - 2>&1 <<EOF | ./filter_tmpdir.sh
+  > theory PyRAT_ONNX
   >   use ieee_float.Float64
   >   use bool.Bool
   >   use int.Int
@@ -23,4 +23,14 @@ Test verify
   >       (0.0:t) .< (nn@@i)[0] .< (0.5:t)
   > end
   > EOF
-  [caisar] Goal G: Unknown ()
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  0.0 <  y0
+  
+  [DEBUG]{ProverSpec} Prover-tailored specification:
+  0.0 <= x0
+  x0 <= 0.5
+  y0 <  0.5
+  
+  Goal G: Unknown ()
diff --git a/tests/saver.t b/tests/saver.t
index 56387c8ebdf9ac41f0bf45865f3295c16f63fad1..a05fc8d70b7392ac79a4251c7a461197041700d3 100644
--- a/tests/saver.t
+++ b/tests/saver.t
@@ -23,6 +23,6 @@ Test verify
   >   goal I: cond_robust model dataset (8.0:t)
   > end
   > EOF
-  [caisar] Goal G: Valid (2/2)
-  [caisar] Goal H: Invalid (1/2)
-  [caisar] Goal I: Unknown (0/2)
+  Goal G: Valid (2/2)
+  Goal H: Invalid (1/2)
+  Goal I: Unknown (0/2)
diff --git a/tests/verify_json.t b/tests/verify_json.t
index b625f989323acebc668bc912b62e1080cbce1655..d34b2e3ddd27f695edcca33f6f12d661639dca02 100644
--- a/tests/verify_json.t
+++ b/tests/verify_json.t
@@ -14,5 +14,77 @@ Test verify-json
 
   $ PATH=$(pwd)/bin:$PATH
 
-  $ caisar verify-json config.json 2>&1 <<EOF | ./filter_tmpdir.sh
-  [caisar] Goal property: Unknown ()
+  $ 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
+  (declare-const X_0 Real)
+  
+  ;; X_1
+  (declare-const X_1 Real)
+  
+  ;; X_2
+  (declare-const X_2 Real)
+  
+  ;; X_3
+  (declare-const X_3 Real)
+  
+  ;; X_4
+  (declare-const X_4 Real)
+  
+  ;; Y_0
+  (declare-const Y_0 Real)
+  
+  ;; Y_1
+  (declare-const Y_1 Real)
+  
+  ;; Y_2
+  (declare-const Y_2 Real)
+  
+  ;; Y_3
+  (declare-const Y_3 Real)
+  
+  ;; Y_4
+  (declare-const Y_4 Real)
+  
+  ;; axiom_ge_x0
+  (assert (>= X_0 0.0))
+  
+  ;; axiom_le_x0
+  (assert (<= X_0 0.299999999999999988897769753748434595763683319091796875))
+  
+  ;; axiom_ge_x1
+  (assert (>= X_1 0.6999999999999999555910790149937383830547332763671875))
+  
+  ;; axiom_le_x1
+  (assert (<= X_1 1.0))
+  
+  ;; axiom_ge_x2
+  (assert (>= X_2 0.484313724999999972720132745962473563849925994873046875))
+  
+  ;; axiom_le_x2
+  (assert (<= X_2 1.0))
+  
+  ;; axiom_ge_x3
+  (assert (>= X_3 0.0))
+  
+  ;; axiom_le_x3
+  (assert (<= X_3 0.319607843000000002575688995420932769775390625))
+  
+  ;; axiom_ge_x4
+  (assert (>= X_4 0.476470588000000028205960234117810614407062530517578125))
+  
+  ;; axiom_le_x4
+  (assert (<= X_4 1.0))
+  
+  ;; Goal robust_record0_y1
+  (assert
+    (or
+      (and (>= Y_0 Y_1))
+      (and (>= Y_2 Y_1))
+      (and (>= Y_3 Y_1))
+      (and (>= Y_4 Y_1))
+      ))
+  
+  Goal property: Unknown ()