# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1446721185 -3600
# Node ID c3974cd2d381dd317f2bd9a3a671816393e09e54
# Parent  5197a2ecb65850a97df9463e70274c98a4636a71
updating options to verit

diff -r 5197a2ecb658 -r c3974cd2d381 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 05 10:39:59 2015 +0100
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Nov 05 11:59:45 2015 +0100
@@ -101,13 +101,12 @@
   command = make_command "VERIT",
   options = (fn ctxt => [
     "--proof-version=1",
-    "--proof=-",
     "--proof-prune",
     "--proof-merge",
     "--disable-print-success",
     "--disable-banner",
     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
-  smt_options = [],
+  smt_options = [(":produce-proofs", "true")],
   default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
     "warning : proof_done: status is still open"),