diff --git a/config/drivers/pyrat.drv b/config/drivers/pyrat.drv
index 6c21b2b1c93ad95f30422e0fba2a26ad54d6685b..ec70c5839c35a75e1cc259b2c72ec082f6fcf5da 100644
--- a/config/drivers/pyrat.drv
+++ b/config/drivers/pyrat.drv
@@ -1,5 +1,7 @@
 (* Why3 drivers for PyRAT *)
 
+prelude "(* this is the prelude for PyRAT *)"
+
 (* additional regexp for detection of answers, needed for alt-ergo <= 0.99 *)
 valid "^Inconsistent assumption$"
 
diff --git a/nnet.opam b/nnet.opam
index 4871796a4c568e4a3339f8a81b43c26d01c74ccd..ea6f2c5285c00613bc4df4880b74b71fc723ad96 100644
--- a/nnet.opam
+++ b/nnet.opam
@@ -9,7 +9,7 @@ depends: [
   "odoc" {with-doc}
 ]
 build: [
-  ["dune" "subst" "--root" "."] {dev}
+  ["dune" "subst"] {dev}
   [
     "dune"
     "build"
@@ -17,8 +17,7 @@ build: [
     name
     "-j"
     jobs
-    "--promote-install-files"
-    "false"
+    "--promote-install-files=false"
     "@install"
     "@runtest" {with-test}
     "@doc" {with-doc}
diff --git a/src/dune b/src/dune
index 3d9b62cc15be31725720c7cf92474d8f1110e275..a8874d6ff1d5b9540ee9aa6eefeef5751a2643a0 100644
--- a/src/dune
+++ b/src/dune
@@ -6,6 +6,8 @@
   (package caisar)
 )
 
+(copy_files printer/*)
+
 (generate_sites_module
   (module dirs)
   (sites caisar))
diff --git a/src/printer/pyrat.ml b/src/printer/pyrat.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5ec59fe8d69e511d0760840c0b89a4411f03cd14
--- /dev/null
+++ b/src/printer/pyrat.ml
@@ -0,0 +1,13 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of CAISAR.                                          *)
+(*                                                                        *)
+(**************************************************************************)
+
+let print_task args ?old:_ fmt _task =
+  let open Why3 in
+  Printer.print_prelude fmt args.Printer.prelude
+
+let () =
+  Why3.Printer.register_printer ~desc:"Printer for the PyRAT prover." "pyrat"
+    print_task
diff --git a/src/verification.ml b/src/verification.ml
index 1fa659152b89ef0be7f666d5670a3842fd184b3d..74d0fd55c4ec90c7e24cdab27fd01eea85580c94 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -6,6 +6,7 @@
 
 open Base
 module Format = Caml.Format
+module Filename = Caml.Filename
 
 let () = Language.register ()
 
@@ -24,23 +25,23 @@ let verify format loadpath prover file =
     match file with
     | "-" ->
       ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
-    | filename ->
-      let mlw_files, _ = Env.(read_file ?format base_language env filename) in
-      (filename, mlw_files)
+    | file ->
+      let mlw_files, _ = Env.(read_file ?format base_language env file) in
+      (file, mlw_files)
   in
   Wstdlib.Mstr.iter
     (fun _ theory ->
       let tasks = Task.split_theory theory None None in
       let prover =
-        Whyconf.filter_one_prover config (Why3.Whyconf.mk_filter_prover prover)
+        Whyconf.(filter_one_prover config (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)
         | Some file ->
           let file =
-            Caml.Filename.concat
-              (Caml.Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
+            Filename.concat
+              (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
               file
           in
           Driver.load_driver_absolute env file prover.extra_drivers
diff --git a/tests/simple.t b/tests/simple.t
index 9796780f441044111b635f2c23ebc792cb8ba313..2f22cd593564a0dee407d00725de98f6d9818a05 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -46,6 +46,7 @@ Test verify
   <autodetect>Found prover Marabou version 1.0.+, OK.
   <autodetect>Found prover PyRAT version 1.0, OK.
   <autodetect>3 prover(s) added
+  (* this is the prelude for PyRAT *)
   (* this is a prelude for Alt-Ergo integer arithmetic *)
   (* this is a prelude for Alt-Ergo real arithmetic *)
   type string