2 files changed, 11 insertions, 0 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 56029c5f..753196a8 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -2032,6 +2032,14 @@ let compile env ast =
   let rmap = build_register_map CTMap.empty cdefs in
   cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap; ast = ast }
 
+let to_axiomatic_model name_file env ast =
+  let jib, ctx = compile env ast in
+  let out_chan = open_out name_file in
+  Marshal.to_channel out_chan jib [];
+  Marshal.to_channel out_chan (Type_check.Env.set_prover None ctx.tc_env) [];
+  Marshal.to_channel out_chan ctx.register_map [];
+  close_out out_chan
+
 let generate_smt props name_file env ast =
   try
     let cdefs, ctx = compile env ast in
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 2680f937..28d10fd3 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -139,6 +139,9 @@ module Make_optimizer(S : Sequence) : sig
   val optimize : smt_def Stack.t -> smt_def S.t
 end
 
+val to_axiomatic_model :
+  string -> Type_check.Env.t -> Type_check.tannot defs -> unit
+
 (** Generate SMT for all the $property and $counterexample pragmas in
    an AST, and write it to appropriately named files. *)
 val generate_smt :