diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 18:08:53 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-27 18:29:50 +0200 |
| commit | 4e6129afb9aab53d14f16ac74a5a4e80323b5813 (patch) | |
| tree | 7037708e3ae50407842b8216117d0edb47e71c60 /src/verit/verit.ml | |
| parent | a2e8b2f68fa82ca96468cb0613710c07b27192da (diff) | |
| download | smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.tar.gz smtcoq-4e6129afb9aab53d14f16ac74a5a4e80323b5813.zip | |
formatting
Diffstat (limited to 'src/verit/verit.ml')
| -rw-r--r-- | src/verit/verit.ml | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/verit/verit.ml b/src/verit/verit.ml index e7ad9b1..643ce8f 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -53,10 +53,10 @@ let import_trace filename first = raise VeritLexer.Eof with | VeritLexer.Eof -> - close_in chan; - let first = - let aux = VeritSyntax.get_clause !first_num in - match first, aux.value with + close_in chan; + let first = + let aux = VeritSyntax.get_clause !first_num in + match first, aux.value with | Some (root,l), Some (fl::nil) -> if Form.equal l fl then aux @@ -132,17 +132,16 @@ let call_verit rt ro fl root = let (filename, outchan) = Filename.open_temp_file "verit_coq" ".smt2" in export outchan rt ro fl; close_out outchan; - let logfilename = (Filename.chop_extension filename)^".vtlog" in - - let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof="^logfilename^" "^filename in + let logfilename = Filename.chop_extension filename ^ ".vtlog" in + let command = "veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-ackermann --input=smtlib2 --proof=" ^ logfilename ^ " " ^ filename in Format.eprintf "%s@." command; let t0 = Sys.time () in let exit_code = Sys.command command in let t1 = Sys.time () in Format.eprintf "Verit = %.5f@." (t1-.t0); if exit_code <> 0 then - failwith ("Verit.call_verit: command "^command^ - " exited with code "^(string_of_int exit_code)); + failwith ("Verit.call_verit: command " ^ command ^ + " exited with code " ^ string_of_int exit_code); try import_trace logfilename (Some root) with |