diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 01bee760bc64463e08ad5866aea4f2186bc94c59..b14e66f3b6df9ac3a7ce701f76552016040a3c54 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -18,7 +18,7 @@ version_switch = "--version"
 version_regexp = "\\([0-9.+]+\\)"
 version_ok  = "1.0.+"
 command = "%e --timeout %t %f"
-driver = "drivers/marabou"
+driver = "caisar_drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP pyrat]
diff --git a/src/main.ml b/src/main.ml
index c4ea8291114014035fd962818d426c2b233ef26f..d41168ea032f9d104099e6e56e6b845e28ac4dbb 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -59,8 +59,8 @@ let config detect () =
         provers)
   end
 
-let verify format loadpath files prover =
-  List.iter ~f:(fun x -> Verification.verify format loadpath x prover) files
+let verify format loadpath prover files =
+  List.iter ~f:(Verification.verify format loadpath prover) files
 
 let exec_cmd cmdname cmd =
   Logs.debug (fun m -> m "Command `%s'." cmdname);
@@ -114,16 +114,16 @@ let verify_cmd =
     Arg.(value & pos_all string [] & info [] ~doc)
   in
   let format =
-    let doc = "format" in
+    let doc = "File format" in
     Arg.(value & opt (some string) None & info [ "format" ] ~doc)
   in
   let loadpath =
-    let doc = "additional loadpath" in
+    let doc = "Additional loadpath" in
     Arg.(value & opt_all string [] & info [ "L" ] ~doc)
   in
   let prover =
     let doc = "Prover to use" in
-    Arg.(required & opt (some string) None & info [ "prover" ] ~doc)
+    Arg.(required & opt (some string) None & info [ "p"; "prover" ] ~doc)
   in
   let doc = "Property verification of neural networks." in
   let exits = Term.default_exits in
@@ -134,10 +134,10 @@ let verify_cmd =
   in
   ( Term.(
       ret
-        (const (fun format loadpath files prover ->
+        (const (fun format loadpath prover files ->
            `Ok
-             (exec_cmd cmdname (fun () -> verify format loadpath files prover)))
-        $ format $ loadpath $ files $ prover)),
+             (exec_cmd cmdname (fun () -> verify format loadpath prover files)))
+        $ format $ loadpath $ prover $ files)),
     Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
 
 let default_cmd =
diff --git a/src/verification.ml b/src/verification.ml
index 54088494542baef589c6ff8e8d60a4ecf226a556..851dac507a7c540dc89a00407c1ac0698bfca381 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -12,15 +12,12 @@ let () = Language.register ()
 let create_env loadpath =
   let config = Autodetection.autodetect ~debug:true () in
   let stdlib = Dirs.Sites.stdlib in
-
   let open Why3 in
   ( Env.create_env
       (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
     config )
 
-let mkfilter prover = Why3.Whyconf.mk_filter_prover prover
-
-let verify format loadpath file prover =
+let verify format loadpath prover file =
   let open Why3 in
   let env, config = create_env loadpath in
   let _, mstr_theory =
@@ -34,7 +31,9 @@ let verify format loadpath file prover =
   Wstdlib.Mstr.iter
     (fun _ theory ->
       let tasks = Task.split_theory theory None None in
-      let prover = Whyconf.filter_one_prover config (mkfilter prover) in
+      let prover =
+        Whyconf.filter_one_prover config (Why3.Whyconf.mk_filter_prover prover)
+      in
       let driver =
         match String.chop_prefix ~prefix:"caisar_drivers/" prover.driver with
         | None -> Whyconf.(load_driver (get_main config) env prover)
diff --git a/tests/simple.t b/tests/simple.t
index 56a0a7502052c0afdb26e826bb70fec3f101e6c4..9796780f441044111b635f2c23ebc792cb8ba313 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -6,11 +6,19 @@ Test verify
   > echo "PyRAT 1.0"
   > EOF
 
-  $ chmod u+x bin/pyrat.py
+  $ cat - > bin/Marabou << EOF
+  > #!/bin/sh
+  > echo "1.0.+"
+  > EOF
+
+  $ chmod u+x bin/pyrat.py bin/Marabou
 
   $ bin/pyrat.py
   PyRAT 1.0
 
+  $ bin/Marabou
+  1.0.+
+
   $ PATH=$(pwd)/bin:$PATH
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9./]*/$TMPFILE/'
@@ -28,9 +36,6 @@ Test verify
   <autodetect>0 prover(s) added
   <autodetect>Generating strategies:
   <autodetect>Run: (Marabou --version) > $TMPFILE 2>&1
-  <autodetect>command 'Marabou --version' failed. Output:
-  sh: 1: Marabou: not found
-  
   <autodetect>Run: (alt-ergo --version) > $TMPFILE 2>&1
   <autodetect>Run: (alt-ergo-2.4.0 --version) > $TMPFILE 2>&1
   <autodetect>command 'alt-ergo-2.4.0 --version' failed. Output:
@@ -38,8 +43,9 @@ Test verify
   
   <autodetect>Run: (pyrat.py --version) > $TMPFILE 2>&1
   <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+  <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.0, OK.
-  <autodetect>2 prover(s) added
+  <autodetect>3 prover(s) added
   (* this is a prelude for Alt-Ergo integer arithmetic *)
   (* this is a prelude for Alt-Ergo real arithmetic *)
   type string