# HG changeset patch # User blanchet # Date 1692955884 -7200 # Node ID 2baa77e37406ae53908bb81ac1363aa972c16653 # Parent ff86f10e54cd6a0ff96ea4385304311e3da078f4 avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer diff -r ff86f10e54cd -r 2baa77e37406 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Aug 25 13:56:00 2023 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Aug 25 11:31:24 2023 +0200 @@ -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 *)}