Since updating to Isabelle2022 I frequently have sledgehammer finding multiple proofs with cvc4. Is this normal behavior?
Output looks like this image.png
This is the normal new behavior
Sledgehammer now tries several strategies with different slices, leading to several proofs (or several times the same)
@Mathias Fleury I see, thanks.
waynee95 has marked this topic as resolved.
From the NEWS file:
* Sledgehammer: - Redesigned multithreading to provide more fine grained prover schedules. The binary option 'slice' has been replaced by a numeric value 'slices' indicating the number of desired slices. Stronger provers can now be run by more than one thread simultaneously. The new option 'max_proofs' controls the number of proofs shown. INCOMPATIBILITY.
Last updated: Dec 07 2023 at 20:16 UTC