src/HOL/Tools/SMT/smt_setup_solvers.ML

     name = make_name is_remote "cvc3",
     class = SMTLIB_Interface.smtlibC,
     avail = make_avail is_remote "CVC3",
     command = make_command is_remote "CVC3",
     options = cvc3_options,
-    default_max_relevant = 200,
+    default_max_relevant = 200 (* FUDGE *),
     supports_filter = false,
     outcome =
       on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
     cex_parser = NONE,
     reconstruct = NONE }

   avail = make_local_avail "YICES",
   command = make_local_command "YICES",
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--smtlib"]),
-  default_max_relevant = 200,
+  default_max_relevant = 200 (* FUDGE *),
   supports_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
   reconstruct = NONE }
 

     name = make_name is_remote "z3",
     class = Z3_Interface.smtlib_z3C,
     avail = make_avail is_remote "Z3",
     command = z3_make_command is_remote "Z3",
     options = z3_options,
-    default_max_relevant = 250,
+    default_max_relevant = 250 (* FUDGE *),
     supports_filter = true,
     outcome = z3_on_last_line,
     cex_parser = SOME Z3_Model.parse_counterex,
     reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
 in