# HG changeset patch
# User paulson
# Date 1693046200 -3600
# Node ID af34c689bfdabe1367511d8ca304f809e6e5f261
# Parent  25f16c356dae0ff175e4f90b8147c1cf65660673# Parent  7ed1759fe1bdbefd82c6be7e381549589ece652f
merged

diff -r 7ed1759fe1bd -r af34c689bfda src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Aug 26 11:36:25 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Sat Aug 26 11:36:40 2023 +0100
@@ -390,15 +390,22 @@
    prem_role = Hypothesis,
    generate_isabelle_info = false,
    good_slices =
-     (* FUDGE *)
-     K [((2, false, false, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)),
-      ((2, false, false, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)),
-      ((2, false, false, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
-      ((2, false, false, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)),
-      ((2, false, false, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)),
-      ((2, false, false, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)),
-      ((2, false, false, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))],
+     let
+       (* Older versions of Vampire have unsound handling of Booleans. *)
+       val mono_native =
+         if string_ord (getenv "VAMPIRE_VERSION", "4.8") <> LESS then "mono_native_fool"
+         else "mono_native"
+     in
+       (* FUDGE *)
+       K [((2, false, false, 512, meshN), (TX1, mono_native, combsN, false, sosN)),
+        ((2, false, false, 1024, meshN), (TX1, mono_native, liftingN, false, sosN)),
+        ((2, false, false, 256, mashN), (TX1, mono_native, liftingN, false, no_sosN)),
+        ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)),
+        ((2, false, false, 16, meshN), (TX1, mono_native, liftingN, false, no_sosN)),
+        ((2, false, false, 32, meshN), (TX1, mono_native, combsN, false, no_sosN)),
+        ((2, false, false, 64, meshN), (TX1, mono_native, combs_or_liftingN, false, no_sosN)),
+        ((2, false, false, 128, meshN), (TX1, mono_native, liftingN, false, no_sosN))]
+      end,
    good_max_mono_iters = default_max_mono_iters,
    good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)}