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 (* FUDGE *),
+    default_max_relevant = 150 (* 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 (* FUDGE *),
+  default_max_relevant = 150 (* FUDGE *),
   supports_filter = false,
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
   cex_parser = NONE,
   reconstruct = NONE }