Revision 57d61d67
Added by Pierre-Loïc Garoche over 6 years ago
src/utils.ml | ||
---|---|---|
380 | 380 |
| _ -> assert false |
381 | 381 |
in |
382 | 382 |
run 0 l1 l2 |
383 |
|
|
384 |
let rec extract l fst last = |
|
385 |
if last < fst then assert false else |
|
386 |
match l, fst with |
|
387 |
| hd::tl, 0 -> if last = 0 then [] else hd::(extract tl 0 (last-1)) |
|
388 |
| _::tl, _ -> extract tl (fst-1) (last-1) |
|
389 |
| [], 0 -> if last=0 then [] else assert false (* List too short *) |
|
390 |
| _ -> assert false |
|
391 |
|
|
383 | 392 |
end |
384 | 393 |
|
385 |
|
|
394 |
let get_date () = |
|
395 |
let tm = Unix.localtime (Unix.time ()) in |
|
396 |
let fmt = Format.str_formatter in |
|
397 |
let open Unix in |
|
398 |
let _ = |
|
399 |
Format.fprintf fmt |
|
400 |
"%i/%i/%i %ih%i:%i" |
|
401 |
tm.tm_year |
|
402 |
tm.tm_mon |
|
403 |
tm.tm_mday |
|
404 |
tm.tm_hour |
|
405 |
tm.tm_min |
|
406 |
tm.tm_sec |
|
407 |
in |
|
408 |
Format.flush_str_formatter () |
|
409 |
|
|
386 | 410 |
(* Local Variables: *) |
387 | 411 |
(* compile-command:"make -C .." *) |
388 | 412 |
(* End: *) |
Also available in: Unified diff
New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation