diff --git a/compiler/verification/dune b/compiler/verification/dune
index 459abfed..0584a6c2 100644
--- a/compiler/verification/dune
+++ b/compiler/verification/dune
@@ -1,7 +1,17 @@
 (library
  (name verification)
  (public_name catala.verification)
- (libraries bindlib utils dcalc runtime z3 calendar))
+ (libraries
+  bindlib
+  utils
+  dcalc
+  runtime
+  calendar
+  (select
+   z3backend.ml
+   from
+   (z3 -> z3backend.real.ml)
+   (-> z3backend.dummy.ml))))
 
 (documentation
  (package catala)
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
new file mode 100644
index 00000000..90beed67
--- /dev/null
+++ b/compiler/verification/z3backend.dummy.ml
@@ -0,0 +1,42 @@
+(* This file is part of the Catala compiler, a specification language for tax
+   and social benefits computation rules. Copyright (C) 2022 Inria, contributor:
+   Aymeric Fromherz <aymeric.fromherz@inria.fr>
+
+   Licensed under the Apache License, Version 2.0 (the "License"); you may not
+   use this file except in compliance with the License. You may obtain a copy of
+   the License at
+
+   http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+   WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+   License for the specific language governing permissions and limitations under
+   the License. *)
+
+(** Replicating the interface, with no actual implementation for compiling
+    without the expected backend. All functions print an error message and exit *)
+
+let dummy () =
+  Utils.Cli.error_print
+    "This instance of Catala was compiled without Z3 support.";
+  exit 124
+
+module Io = struct
+  let init_backend () = dummy ()
+
+  type backend_context = unit
+
+  let make_context _ _ = dummy ()
+
+  type vc_encoding = unit
+
+  let translate_expr _ _ = dummy ()
+
+  type model = unit
+  type vc_encoding_result = Success of model * model | Fail of string
+
+  let print_positive_result _ = dummy ()
+  let print_negative_result _ _ _ = dummy ()
+  let encode_and_check_vc _ _ = dummy ()
+end
diff --git a/compiler/verification/z3backend.ml b/compiler/verification/z3backend.real.ml
similarity index 100%
rename from compiler/verification/z3backend.ml
rename to compiler/verification/z3backend.real.ml