Fix dummy z3 backend with compatible IO interface

CatalaLang · Dec 8, 2023 · 1d2d7a6 · 1d2d7a6
1 parent 4413af3
commit 1d2d7a6
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml
@@ -30,6 +30,15 @@ module Backend = struct
 
   type vc_encoding = unit
 
+  let print_encoding _ _ = dummy ()
+
+  type model = unit
+  type solver_result = ProvenTrue | ProvenFalse of model option | Unknown
+
+  let solve_vc_encoding _ _ = dummy ()
+  let print_model _ _ = dummy ()
+  let is_model_empty _ = dummy () 
+
   let translate_expr _ _ _ = dummy ()
   let encode_asserts _ _ _ = dummy ()
 end