src/HOL/Tools/SMT/smt_systems.ML

   command = make_command "CVC4",
   options = cvc4_options,
   smt_options = [(":produce-unsat-cores", "true")],
   good_slices =
     (* FUDGE *)
+    [((4, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((4, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((4, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((4, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((4, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((4, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((4, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
+  parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
+  replay = NONE }
+
+val cvc5: SMT_Solver.solver_config = {
+  name = "cvc5",
+  class = select_class,
+  avail = make_avail "CVC5",
+  command = make_command "CVC5",
+  options = cvc5_options,
+  smt_options = [(":produce-unsat-cores", "true")],
+  good_slices =
+    (* FUDGE *)
     [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
      ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
      ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
      ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
      ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),

      ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = NONE }
 
-val cvc5: SMT_Solver.solver_config = {
-  name = "cvc5",
-  class = select_class,
-  avail = make_avail "CVC5",
-  command = make_command "CVC5",
-  options = cvc5_options,
-  smt_options = [(":produce-unsat-cores", "true")],
-  good_slices =
-    (* FUDGE *)
-    [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
-  outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
-  parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
-  replay = NONE }
-
 (*
 We need different options for alethe proof production by cvc5 and the smt_options
 cannot be changed, so different configuration.
 *)
 val cvc5_proof: SMT_Solver.solver_config = {

   command = make_command "CVC5",
   options = cvc5_options,
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
-     ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
-     ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
-     ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
-     ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
-     ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
-     ((2, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+    [((4, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+     ((4, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+     ((4, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+     ((4, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+     ((4, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+     ((4, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+     ((4, false, false, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
   replay = SOME CVC5_Replay.replay }
 
 end

   command = the o check_tool "ISABELLE_VERIT",
   options = veriT_options,
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, false, false, 1024, meshN), []),
-     ((2, false, false, 512, mashN), []),
-     ((2, false, true, 128, meshN), []),
-     ((2, false, false, 64, meshN), []),
-     ((2, false, false, 256, mepoN), []),
-     ((2, false, false, 32, meshN), [])],
+    [((4, false, false, 1024, meshN), []),
+     ((4, false, false, 512, mashN), []),
+     ((4, false, true, 128, meshN), []),
+     ((4, false, false, 64, meshN), []),
+     ((4, false, false, 256, mepoN), []),
+     ((4, false, false, 32, meshN), [])],
   outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"),
   parse_proof = SOME (K Lethe_Proof_Parse.parse_proof),
   replay = SOME Verit_Replay.replay }
 
 end

   command = fn () => [getenv "Z3_SOLVER", "-in"],
   options = z3_options,
   smt_options = [(":produce-proofs", "true")],
   good_slices =
     (* FUDGE *)
-    [((2, false, false, 1024, meshN), []),
-     ((2, false, false, 512, mepoN), []),
-     ((2, false, false, 64, meshN), []),
-     ((2, false, true, 256, meshN), []),
-     ((2, false, false, 128, mashN), []),
-     ((2, false, false, 32, meshN), [])],
+    [((4, false, false, 1024, meshN), []),
+     ((4, false, false, 512, mepoN), []),
+     ((4, false, false, 64, meshN), []),
+     ((4, false, true, 256, meshN), []),
+     ((4, false, false, 128, mashN), []),
+     ((4, false, false, 32, meshN), [])],
   outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
   parse_proof = SOME Z3_Replay.parse_proof,
   replay = SOME Z3_Replay.replay }
 
 end