give more facts to veriT -- it seems to be able to cope with them
authorblanchet
Tue, 30 Sep 2014 14:19:25 +0200
changeset 58496 2ba52ecc4996
parent 58495 aefcb244423f
child 58497 20aaa307c0ff
give more facts to veriT -- it seems to be able to cope with them
src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Tue Sep 30 14:18:07 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Tue Sep 30 14:19:25 2014 +0200
@@ -109,7 +109,7 @@
     "--disable-banner",
     "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]),
   smt_options = [],
-  default_max_relevant = 120 (* FUDGE *),
+  default_max_relevant = 200 (* FUDGE *),
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
     "warning : proof_done: status is still open"),
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),