diff options
Diffstat (limited to 'src/jib/jib_smt.ml')
| -rw-r--r-- | src/jib/jib_smt.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index a380c518..6ace9d96 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -2032,7 +2032,7 @@ 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 file env ast = +let serialize_smt_model file env ast = let cdefs, ctx = compile env ast in let out_chan = open_out file in Marshal.to_channel out_chan cdefs []; @@ -2040,12 +2040,13 @@ let to_axiomatic_model file env ast = Marshal.to_channel out_chan ctx.register_map []; close_out out_chan -let from_axiomatic_model file = +let deserialize_smt_model file = let in_chan = open_in file in let cdefs = (Marshal.from_channel in_chan : cdef list) in let env = (Marshal.from_channel in_chan : Type_check.env) in let rmap = (Marshal.from_channel in_chan : id list CTMap.t) in - cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap } + close_in in_chan; + (cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap }) let generate_smt props name_file env ast = try |