Email Gateway (Aug 22 2022 at 18:32): Email Gateway (Aug 22 2022 at 18:32):From: Mark Wassell <mpwassell@gmail.com>
Hello,
Occasionally I get the message
"vampire": A prover error occurred:
User error: option splitting not known
when using sledgehammer. It often occurs when attempting to prove
non-lemmas so in these cases it isn't a problem. With other cases breaking
down the problem avoids the error message and I obtain proof(s) from
sledgehammer. Of course I don't know at the start which of these buckets my
problem falls into and it would good to avoid the wasted sledgehammer
attempt.
An example that will provoke the message is given below. I haven't been
able to reproduce the problem in a theory that isn't using Nominal2.
theory VampireSplitError
imports "Nominal2.Nominal2"
begin
sledgehammer_params[debug=true, timeout=600, provers= cvc4 spass e vampire
z3,isar_proofs=true,smt_proofs=false]
lemma
fixes G::"('a::fs set)"
assumes "finite G" and "G ⊆ G'"
shows "supp G ⊆ supp G'"
using supp_of_finite_sets assms sledgehammer
Cheers
Mark
Last updated: Apr 19 2024 at 04:17 UTC