Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] R: Isabelle2019-RC2 sporadic smt failures

Email Gateway (Aug 22 2022 at 19:51):

From: marco caminati via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Not sure if this helps: you can try to use the sledgehammer "overlord" option, then manually feed
the .in z3 file this generates to z3, maybe prepending a "(set-option :verbose xxx)" line,
in order to investigate what's happening.

Cheers,
Marco

Last updated: Apr 26 2024 at 04:17 UTC