diff options
| author | Alasdair Armstrong | 2019-06-06 18:01:40 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-06-06 18:02:09 +0100 |
| commit | cebf08acc9a278b1b9652a56bd0c506d2f6268f6 (patch) | |
| tree | 8f92ccbaa8ec1f9f72049855ff9a913415dc69d6 /src/jib/jib_smt.mli | |
| parent | 110bef3571a77fd8f1059827ea0bb29935ed785d (diff) | |
SMT: Rename some functions to make usage clearer
Diffstat (limited to 'src/jib/jib_smt.mli')
| -rw-r--r-- | src/jib/jib_smt.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli index 98b4b1c9..cdaf7e39 100644 --- a/src/jib/jib_smt.mli +++ b/src/jib/jib_smt.mli @@ -139,10 +139,10 @@ module Make_optimizer(S : Sequence) : sig val optimize : smt_def Stack.t -> smt_def S.t end -val to_axiomatic_model : +val serialize_smt_model : string -> Type_check.Env.t -> Type_check.tannot defs -> unit -val from_axiomatic_model : +val deserialize_smt_model : string -> cdef list * ctx (** Generate SMT for all the $property and $counterexample pragmas in |