Merge remote-tracking branch 'origin/sail2' into separate_bv

1 files changed, 6 insertions, 0 deletions

diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 2680f937..cdaf7e39 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -139,6 +139,12 @@ module Make_optimizer(S : Sequence) : sig
   val optimize : smt_def Stack.t -> smt_def S.t
 end
 
+val serialize_smt_model :
+  string -> Type_check.Env.t -> Type_check.tannot defs -> unit
+
+val deserialize_smt_model :
+  string -> cdef list * ctx
+
 (** Generate SMT for all the $property and $counterexample pragmas in
    an AST, and write it to appropriately named files. *)
 val generate_smt :