diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index e2c7734ff..318c805e8 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -308,6 +308,7 @@ let fpa_example ( ctx : context ) = ( let solver = (mk_solver ctx None) in (Solver.add solver [ c5 ]) ; + Printf.printf "Memory in use before `check`: %Lu bytes\n" (Statistics.get_estimated_alloc_size()); if (check solver []) != SATISFIABLE then raise (TestFailedException "") else diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 5bd554313..166e474d9 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1832,6 +1832,9 @@ struct let get (x:statistics) (key:string) = try Some(List.find (fun c -> Entry.get_key c = key) (get_entries x)) with | Not_found -> None + + let get_estimated_alloc_size = + Z3native.get_estimated_alloc_size end diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index bb3e70875..5320fc38e 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3224,6 +3224,9 @@ sig (** The value of a particular statistical counter. *) val get : statistics -> string -> Entry.statistics_entry option + + (** The estimated allocated memory in bytes. *) + val get_estimated_alloc_size : unit -> int64 end (** Solvers *)