Email Gateway (Jul 19 2022 at 12:01): Email Gateway (Jul 19 2022 at 12:01):From: Peter Lammich <lammich@in.tum.de>
Same example where smt (z3) fails with internal exception, smt (verit)
is no better: Here, the proof reconstruction seems to fail.
(Looks like my goal is very challenging for the sledgehammer
infrastructure, but it was not specially crafted, but just occurred
during my regular proof work)
Bug2.thy
Email Gateway (Jul 21 2022 at 16:56):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Peter,
Your example is actually triggering 3 (!) different bugs in the proof
reconstruction of veriT, all related to quantifiers.
I have debugged 2 so far.
Thank you a lot for your minimized example!
Mathias
Last updated: Apr 26 2024 at 04:17 UTC