File tree Expand file tree Collapse file tree 3 files changed +7
-0
lines changed
Expand file tree Collapse file tree 3 files changed +7
-0
lines changed Original file line number Diff line number Diff line change @@ -308,6 +308,7 @@ let fpa_example ( ctx : context ) =
308308 (
309309 let solver = (mk_solver ctx None ) in
310310 (Solver. add solver [ c5 ]) ;
311+ Printf. printf " Memory in use before `check`: %Lu bytes\n " (Statistics. get_estimated_alloc_size() );
311312 if (check solver [] ) != SATISFIABLE then
312313 raise (TestFailedException " " )
313314 else
Original file line number Diff line number Diff line change @@ -1832,6 +1832,9 @@ struct
18321832 let get (x :statistics ) (key :string ) =
18331833 try Some (List. find (fun c -> Entry. get_key c = key) (get_entries x)) with
18341834 | Not_found -> None
1835+
1836+ let get_estimated_alloc_size =
1837+ Z3native. get_estimated_alloc_size
18351838end
18361839
18371840
Original file line number Diff line number Diff line change @@ -3224,6 +3224,9 @@ sig
32243224
32253225 (* * The value of a particular statistical counter. *)
32263226 val get : statistics -> string -> Entry .statistics_entry option
3227+
3228+ (* * The estimated allocated memory in bytes. *)
3229+ val get_estimated_alloc_size : unit -> int64
32273230end
32283231
32293232(* * Solvers *)
You can’t perform that action at this time.
0 commit comments