Project

General

Profile

« Previous | Next » 

Revision 57d61d67

Added by Pierre-Loïc Garoche over 6 years ago

New option to select github version of Z3
Added Yojson dependency in lustrev
Some progress on Cex generation

View differences:

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