Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce Z3 version switching #2995

Merged
merged 11 commits into from
Aug 3, 2023
7 changes: 6 additions & 1 deletion ocaml/fstar-lib/FStar_Compiler_Util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -93,6 +93,7 @@ type proc =
mutable killed : bool;
stop_marker: (string -> bool) option;
id : string;
prog : string;
start_time : time}

let all_procs : (proc list) ref = ref []
Expand Down Expand Up @@ -142,7 +143,9 @@ let start_process'
Unix.close stdin_r;
Unix.close stdout_w;
Unix.close stderr_w;
let proc = { pid = pid; id = prog ^ ":" ^ id;
let proc = { pid = pid;
id = prog ^ ":" ^ id;
prog = prog;
inc = Unix.in_channel_of_descr stdout_r;
errc = Unix.in_channel_of_descr stderr_r;
outc = Unix.out_channel_of_descr stdin_w;
Expand Down Expand Up @@ -186,6 +189,8 @@ let kill_process (p: proc) =
let kill_all () =
BatList.iter kill_process !all_procs

let proc_prog (p:proc) : string = p.prog

let process_read_all_output (p: proc) =
(* Pass cleanup:false because kill_process closes both fds already. *)
BatIO.read_all (BatIO.input_channel ~autoclose:true ~cleanup:false p.inc)
Expand Down
17 changes: 17 additions & 0 deletions ocaml/fstar-lib/generated/FStar_Compiler_Misc.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

14 changes: 13 additions & 1 deletion ocaml/fstar-lib/generated/FStar_Errors_Codes.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

38 changes: 22 additions & 16 deletions ocaml/fstar-lib/generated/FStar_Options.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 0 additions & 1 deletion ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

31 changes: 22 additions & 9 deletions ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading