simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: in main, --dot forces --check

Browse source
This commit is contained in:
Simon Cruanes 2019-11-01 15:10:57 -05:00
parent 5b3cadf1e1
commit 2d1d6ee937
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/main/main.ml
View file

@ -100,6 +100,8 @@ let main () =
Arg.usage argspec usage; Arg.usage argspec usage;
exit 2 exit 2
); );
let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
check := !check || CCOpt.is_some dot_proof; (* dot requires a proof *)
let al = Gc.create_alarm check_limits in let al = Gc.create_alarm check_limits in
Util.setup_gc(); Util.setup_gc();
let tst = Term.create ~size:4_096 () in let tst = Term.create ~size:4_096 () in
@ -114,7 +116,6 @@ let main () =
(* might have to check conflicts *) (* might have to check conflicts *)
Solver.add_theory solver Process.Check_cc.theory; Solver.add_theory solver Process.Check_cc.theory;
); );
let dot_proof = if !p_dot_proof = "" then None else Some !p_dot_proof in
Sidekick_smtlib.parse !file >>= fun input -> Sidekick_smtlib.parse !file >>= fun input ->
(* process statements *) (* process statements *)
let res = let res =