Stream: Beginner Questions

Topic: ✔ Multiple proofs found by cvc4 with sledgehammer


view this post on Zulip 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

view this post on Zulip Mathias Fleury (Nov 06 2022 at 13:28):

This is the normal new behavior

view this post on Zulip 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)

view this post on Zulip waynee95 (Nov 06 2022 at 13:29):

@Mathias Fleury I see, thanks.

view this post on Zulip Notification Bot (Nov 06 2022 at 13:29):

waynee95 has marked this topic as resolved.

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC