diff --git a/src/language.ml b/src/language.ml
index b89e65b09a7d74e81d4e135aa0b16876e131d229..5814db488b9e24af90da8dc52644e9ffab8d517c 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -102,14 +102,17 @@ let register_svm_as_array env nb_inputs nb_classes filename mstr =
   in
   Wstdlib.Mstr.add name (Pmodule.close_module th_uc) mstr
 
-let nnet_parser env _ filename _ =
-  let model = Nnet.parse ~permissive:true filename in
-  match model with
-  | Error s -> Loc.errorm "%s" s
-  | Ok { n_inputs; n_outputs; _ } ->
-    Wstdlib.Mstr.empty
-    |> register_nn_as_tuple env n_inputs n_outputs filename
-    |> register_nn_as_array env n_inputs n_outputs filename
+let nnet_parser =
+  Env.Wenv.memoize 13 (fun env ->
+    let h = Hashtbl.create (module String) in
+    Hashtbl.findi_or_add h ~default:(fun filename ->
+      let model = Nnet.parse ~permissive:true filename in
+      match model with
+      | Error s -> Loc.errorm "%s" s
+      | Ok { n_inputs; n_outputs; _ } ->
+        Wstdlib.Mstr.empty
+        |> register_nn_as_tuple env n_inputs n_outputs filename
+        |> register_nn_as_array env n_inputs n_outputs filename))
 
 let onnx_parser env _ filename _ =
   let model = Onnx.parse filename in
@@ -137,7 +140,7 @@ let ovo_parser env _ filename _ =
 
 let register_nnet_support () =
   Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
-    "NNet" [ "nnet" ] nnet_parser
+    "NNet" [ "nnet" ] (fun env _ filename _ -> nnet_parser env filename)
 
 let register_onnx_support () =
   Env.register_format ~desc:"ONNX format" Pmodule.mlw_language "ONNX" [ "onnx" ]
diff --git a/src/language.mli b/src/language.mli
index 39453b44cd27434478bda373e22b03cc8955026e..f46f1887346aa2cb49350164080f1cb9f83343fc 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -50,3 +50,7 @@ val register_onnx_support : unit -> unit
 
 val register_ovo_support : unit -> unit
 (** Register OVO parser. *)
+
+val nnet_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
+(* [nnet_parser env filename] parses and creates the theories corresponding to
+   the given nnet [filename]. The result is memoized. *)
diff --git a/src/verification.ml b/src/verification.ml
index eeef52de9d03823cb31d6477add9fd9d09dd3700..cbe3b35f597c6cbc16d4416195b2130abd1f7d35 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -191,11 +191,14 @@ let call_prover ~limit config env prover config_prover driver dataset_csv task =
       Fmt.(option ~none:nop (any " " ++ string))
       additional_info)
 
-let mstr_theory_of_json_config env _json_config =
+let mstr_theory_of_json_config env (json_config : File.json_config) =
+  let pmod = Language.nnet_parser env json_config.model in
+  let th_pmod = (Wstdlib.Mstr.find "NNasArray" pmod).mod_theory in
   let name = "T" in
   let th_uc = Theory.create_theory (Ident.id_fresh name) in
   let th_real = Env.read_theory env [ "real" ] "Real" in
   let th_uc = Theory.use_export th_uc th_real in
+  let th_uc = Theory.use_export th_uc th_pmod in
   Wstdlib.Mstr.singleton name (Theory.close_theory th_uc)
 
 let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit prover