diff --git a/bin/dune b/bin/dune
index 18e0574a8c28cc0c4eb8d697d271739782a0dd7e..8f91fcbadba80e6da9e447b4dab8cfb2cc12dc17 100644
--- a/bin/dune
+++ b/bin/dune
@@ -4,5 +4,5 @@
  (files
   (dummyversion.py as dummyversion.py)
   (nnenum.sh as nnenum.sh)
-  (marabou_eval.py as marabou_eval.py)
+  (runMarabou.py as runMarabou.py)
   (abcrown.sh as abcrown.sh)))
diff --git a/bin/marabou_eval.py b/bin/runMarabou.py
similarity index 62%
rename from bin/marabou_eval.py
rename to bin/runMarabou.py
index 2683464293326a398d4c8c97a34fc0c0426812f4..079565ff356916475af2cd37eafaff7d49b47101 100755
--- a/bin/marabou_eval.py
+++ b/bin/runMarabou.py
@@ -1,6 +1,9 @@
 #!/usr/bin/env python3
 """
-Adapted for quick evaluation of Marabou for CAISAR
+Modified by the AISER team, Software Safety and Security Laboratory, CEA-List.
+
+This file is part of CAISAR.
+This file is used for integrating Marabou, via its Python interface, in CAISAR.
 
 Top contributors (to current version):
     - Andrew Wu
@@ -12,33 +15,46 @@ All rights reserved. See the file COPYING in the top-level source
 directory for licensing information.
 """
 
-
-class WrongNetFormat(Exception):
-    def __init__(self, networkPath):
-        self.message = f"Network {networkPath} not in onnx, pb or nnet format!"
-        super().__init__(self.message)
-
-
 import argparse
-from importlib.metadata import version
 import os
 import pathlib
 import shutil
 import subprocess
 import sys
 import tempfile
+from importlib.metadata import version
+
+from maraboupy import Marabou, MarabouCore  # type: ignore
+
 
-from maraboupy import Marabou
-from maraboupy import MarabouCore
+class WrongNetFormat(Exception):
+    def __init__(self, networkPath):
+        self.message = (
+            f"Network {networkPath} has an unrecognized extension."
+            f"The network must be in .pb, .nnet or .onnx format."
+        )
+        super().__init__(self.message)
 
 
 sys.path.insert(0, os.path.join(str(pathlib.Path(__file__).parent.absolute()), "../"))
 
 
+def maraboupy_version(marabou_binary: str):
+    result = subprocess.run([marabou_binary, "--version"], capture_output=True, text=True)
+    if result.returncode != 0:
+        print(f"Error running {marabou_binary} --version")
+        sys.exit(1)
+
+    maraboupy_version = version("maraboupy")
+    output = result.stdout.strip()
+    if maraboupy_version in output:
+        return f"maraboupy {maraboupy_version}"
+
+    return sys.exit(1)
+
+
 def arguments():
-    parser = argparse.ArgumentParser(
-        description="Thin wrapper around Maraboupy executable"
-    )
+    parser = argparse.ArgumentParser(description="Thin wrapper around Maraboupy executable")
     parser.add_argument(
         "network",
         type=str,
@@ -46,15 +62,9 @@ def arguments():
         default=None,
         help="The network file name, the extension can be only .pb, .nnet, and .onnx",
     )
-    parser.add_argument(
-        "prop", type=str, nargs="?", default=None, help="The property file name"
-    )
-    parser.add_argument(
-        "-t", "--timeout", type=int, default=10, help="Timeout in seconds"
-    )
-    parser.add_argument(
-        "--temp-dir", type=str, default="/tmp/", help="Temporary directory"
-    )
+    parser.add_argument("prop", type=str, nargs="?", default=None, help="The property file name")
+    parser.add_argument("-t", "--timeout", type=int, default=10, help="Timeout in seconds")
+    parser.add_argument("--temp-dir", type=str, default="/tmp/", help="Temporary directory")
     marabou_path = shutil.which("Marabou")
     parser.add_argument(
         "--marabou-binary",
@@ -74,15 +84,17 @@ def arguments():
 
 def main():
     args, unknown = arguments().parse_known_args()
+
     marabou_binary = args.marabou_binary
     if not os.access(marabou_binary, os.X_OK):
         sys.exit('"{}" does not exist or is not executable'.format(marabou_binary))
     else:
         if args.version:
-            print(f"Maraboupy version {version('maraboupy')}")
+            print(f"{maraboupy_version(marabou_binary)}")
         else:
+            assert args.network is not None
+            assert args.prop is not None
 
-            assert args.prop != None
             networkPath = args.network
             suffix = networkPath.split(".")[-1]
             if suffix == "nnet":
@@ -93,18 +105,17 @@ def main():
                 network = Marabou.read_onnx(networkPath)
             else:
                 raise WrongNetFormat(networkPath)
+
             query = network.getInputQuery()
             MarabouCore.loadProperty(query, args.prop)
             temp = tempfile.NamedTemporaryFile(dir=args.temp_dir, delete=False)
             name = temp.name
             timeout = args.timeout
             MarabouCore.saveQuery(query, name)
+
             print("Running Marabou with the following arguments: ", unknown)
             subprocess.run(
-                [marabou_binary]
-                + ["--input-query={}".format(name)]
-                + ["--timeout={}".format(timeout)]
-                + unknown
+                [marabou_binary] + ["--input-query={}".format(name)] + ["--timeout={}".format(timeout)] + unknown
             )
             os.remove(name)
 
diff --git a/caisar.opam b/caisar.opam
index 9a8115d8bf1b763f900a28deb4f32ff17eb427e0..0db7513743e77c37597920752ecb47f3aa1e5b76 100644
--- a/caisar.opam
+++ b/caisar.opam
@@ -3,10 +3,8 @@ opam-version: "2.0"
 version: "1.0"
 synopsis:
   "A platform for characterizing the safety and robustness of artificial intelligence based software"
-maintainer: [
-  "LAISER team, Software Safety and Security Laboratory, CEA-List"
-]
-authors: ["LAISER team, Software Safety and Security Laboratory, CEA-List"]
+maintainer: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
+authors: ["AISER team, Software Safety and Security Laboratory, CEA-List"]
 license: "LGPL-2.1-only"
 homepage: "https://git.frama-c.com/pub/caisar"
 doc: "https://git.frama-c.com/pub/caisar"
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index daa570a3a03f218d29be38bb16cea554f4c406f1..b46330fd9bba706431dd50344ff226420da4298e 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -54,12 +54,12 @@ driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP maraboupy]
-name = "Maraboupy"
-exec = "marabou_eval.py"
+name = "maraboupy"
+exec = "runMarabou.py"
 version_switch = "--version"
-version_regexp = "Maraboupy version \\([0-9.]+\\)"
+version_regexp = "maraboupy \\([0-9.]+\\)"
 version_ok  = "2.0.0"
-command = "%e %{nnet-onnx} %f "
+command = "%e %{nnet-onnx} %f --timeout %t"
 driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
diff --git a/dune-project b/dune-project
index bcb9f6e06396a4c3a2ac4f39cec65ea5851dc970..55284aa1581c8a2c0bd544f41e9a0c4269072919 100644
--- a/dune-project
+++ b/dune-project
@@ -10,8 +10,8 @@
 (generate_opam_files true)
 
 (license LGPL-2.1-only)
-(authors "LAISER team, Software Safety and Security Laboratory, CEA-List")
-(maintainers "LAISER team, Software Safety and Security Laboratory, CEA-List")
+(authors "AISER team, Software Safety and Security Laboratory, CEA-List")
+(maintainers "AISER team, Software Safety and Security Laboratory, CEA-List")
 (source (uri "git+https://git.frama-c.com/pub/caisar.git"))
 (bug_reports https://git.frama-c.com/pub/caisar/issues)
 (homepage https://git.frama-c.com/pub/caisar)
diff --git a/src/prover.ml b/src/prover.ml
index 9aaebd4105fe584a14b2f2140f8fe74eb9e75ff5..ae5a1df29df5fafad197258a63c10e572d6663f9 100644
--- a/src/prover.ml
+++ b/src/prover.ml
@@ -22,7 +22,7 @@
 
 type t =
   | Marabou
-  | Maraboupy [@name "Maraboupy"]
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]
@@ -38,6 +38,7 @@ let of_string prover =
   let prover = String.lowercase_ascii prover in
   match prover with
   | "marabou" -> Some Marabou
+  | "maraboupy" -> Some Maraboupy
   | "pyrat" -> Some Pyrat
   | "saver" -> Some Saver
   | "aimos" -> Some Aimos
@@ -48,7 +49,7 @@ let of_string prover =
 
 let to_string = function
   | Marabou -> "Marabou"
-  | Maraboupy -> "Maraboupy"
+  | Maraboupy -> "maraboupy"
   | Pyrat -> "PyRAT"
   | Saver -> "SAVer"
   | Aimos -> "AIMOS"
diff --git a/src/prover.mli b/src/prover.mli
index c2eb3d4b9dd795ac92571b36b2f97a0fc293777d..35f47727044c83f1a837e76d68abcc5308bd4907 100644
--- a/src/prover.mli
+++ b/src/prover.mli
@@ -22,7 +22,7 @@
 
 type t = private
   | Marabou
-  | Maraboupy [@name "Maraboupy"]
+  | Maraboupy [@name "maraboupy"]
   | Pyrat [@name "PyRAT"]
   | Saver [@name "SAVer"]
   | Aimos [@name "AIMOS"]
diff --git a/src/verification.ml b/src/verification.ml
index 30ef4fe66f24201b9225439a23fc714709982c13..7f636a5e88bcdea9e59977d9a7f61d8a7badd0ab 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -237,7 +237,7 @@ let answer_dataset limit config env prover config_prover driver dataset task =
   in
   let dataset_answers =
     match prover with
-    | Prover.Marabou ->
+    | Prover.Marabou | Maraboupy ->
       (* We turn each task in [dataset_tasks] into a list (ie, conjunction) of
          disjunctions of tasks. *)
       let tasks = List.map ~f:(Trans.apply Split.split_all) dataset_tasks in
@@ -345,7 +345,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         (* Turn [task] into a list (ie, conjunction) of disjunctions of
            tasks. *)
         match prover with
-        | Prover.Marabou -> Trans.apply Split.split_all task
+        | Prover.Marabou | Maraboupy -> Trans.apply Split.split_all task
         | Pyrat | Nnenum | ABCrown -> Trans.apply Split.split_premises task
         | _ -> [ task ]
       in
@@ -368,7 +368,8 @@ let call_prover ~cwd ~limit config env prover config_prover driver ?dataset
       let proof_strategy = Proof_strategy.apply_svm_prover_strategy in
       answer_saver limit config env config_prover ~proof_strategy task
     | Aimos -> answer_aimos limit config env config_prover dataset task
-    | (Marabou | Pyrat | Nnenum | ABCrown) when Option.is_some dataset ->
+    | (Marabou | Maraboupy | Pyrat | Nnenum | ABCrown)
+      when Option.is_some dataset ->
       let dataset = Unix.realpath (Option.value_exn dataset) in
       answer_dataset limit config env prover config_prover driver dataset task
     | Marabou | Maraboupy | Pyrat | Nnenum | ABCrown ->
diff --git a/tests/autodetect.t b/tests/autodetect.t
index eadc0747b19b3b99dddc8d77b99fa7e5d8d58936..b146b2ec5ce2ef331b5800a67c9c38fcc6b77cc8 100644
--- a/tests/autodetect.t
+++ b/tests/autodetect.t
@@ -30,15 +30,14 @@ Test autodetect
   $ bin/abcrown.sh --version
   dummy-version
 
-  $ bin/marabou_eval.py --version
-  Maraboupy version 2.0.0
+  $ bin/runMarabou.py --version
+  maraboupy 2.0.0
 
   $ caisar config -d
   AIMOS 1.0
   Alt-Ergo 2.4.0
   CVC5 1.0.2
   Marabou 1.0.+
-  Maraboupy 2.0.0
   PyRAT 1.1
   PyRAT 1.1 (ACAS)
   PyRAT 1.1 (ACASd)
@@ -47,4 +46,5 @@ Test autodetect
   SAVer v1.0
   alpha-beta-CROWN dummy-version
   alpha-beta-CROWN dummy-version (ACAS)
+  maraboupy 2.0.0
   nnenum dummy-version
diff --git a/tests/bin/marabou_eval.py b/tests/bin/marabou_eval.py
deleted file mode 100755
index 4ba5fbd8125758a81063b086bcdde7bf2f5c3bac..0000000000000000000000000000000000000000
--- a/tests/bin/marabou_eval.py
+++ /dev/null
@@ -1,14 +0,0 @@
-#!/bin/sh -e
-
-case $1 in
-    --version)
-        echo "Maraboupy version 2.0.0"
-        ;;
-    *)
-        echo "PWD: $(pwd)"
-        echo "NN: $2"
-        test -e $2 || (echo "Cannot find the NN file" && exit 1)
-        echo "Goal:"
-        cat $4
-        echo "Result = Unknown"
-esac
diff --git a/tests/bin/runMarabou.py b/tests/bin/runMarabou.py
new file mode 100755
index 0000000000000000000000000000000000000000..c17b176196afa5c7be2e5b2c0cc22ea07b16b815
--- /dev/null
+++ b/tests/bin/runMarabou.py
@@ -0,0 +1,14 @@
+#!/bin/sh -e
+
+case $1 in
+    --version)
+        echo "maraboupy 2.0.0"
+        ;;
+    *)
+        echo "PWD: $(pwd)"
+        echo "NN: $1"
+        test -e $1 || (echo "Cannot find the NN file" && exit 1)
+        echo "Goal:"
+        cat $2
+        echo "Unknown"
+esac
diff --git a/tests/marabou.t b/tests/marabou.t
index 877caabd60842bcca9082a97e8c29b9667c87b66..e693ada48541a39650d591382de2c99e0c068d91 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -4,7 +4,7 @@ Test verify
   $ bin/Marabou --version
   1.0.+
 
-  $ caisar verify --format whyml --prover=Marabou --ltag=ProverSpec - <<EOF
+  $ cat > file.mlw <<EOF
   > theory T
   >   use ieee_float.Float64
   >   use caisar.types.Vector
@@ -38,6 +38,70 @@ Test verify
   >       (nn @@ i)[1] .< (nn @@ i)[0] \/ (nn @@ i)[0] .< (nn @@ i)[1]
   > end
   > EOF
+
+  $ caisar verify --prover=Marabou --ltag=ProverSpec file.mlw
+  [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 ()
+
+  $ caisar verify --prover=maraboupy --ltag=ProverSpec file.mlw
   [DEBUG]{ProverSpec} Prover-tailored specification:
   x0 >= 0.0
   x0 <= 0.5