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:
- 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.
Last updated: Feb 27 2024 at 08:17 UTC