From 2d1d6ee937d3da8ac41fa08dfc63f5013f2cc3bf Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 1 Nov 2019 15:10:57 -0500 Subject: [PATCH] feat: in main, --dot forces --check --- src/main/main.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/main.ml b/src/main/main.ml index 361bece7..de413e02 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -100,6 +100,8 @@ let main () = Arg.usage argspec usage; 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 Util.setup_gc(); let tst = Term.create ~size:4_096 () in @@ -114,7 +116,6 @@ let main () = (* might have to check conflicts *) 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 -> (* process statements *) let res =