waynee95 (Nov 06 2022 at 13:26): waynee95 (Nov 06 2022 at 13:26):Since updating to Isabelle2022 I frequently have sledgehammer finding multiple proofs with cvc4. Is this normal behavior?
Output looks like this image.png
Mathias Fleury (Nov 06 2022 at 13:28):This is the normal new behavior
Mathias Fleury (Nov 06 2022 at 13:28):Sledgehammer now tries several strategies with different slices, leading to several proofs (or several times the same)
waynee95 (Nov 06 2022 at 13:29):@Mathias Fleury I see, thanks.
Notification Bot (Nov 06 2022 at 13:29):waynee95 has marked this topic as resolved.
Mathias Fleury (Nov 06 2022 at 13:30):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 21 2024 at 12:33 UTC