Email Gateway (Aug 22 2022 at 19:51): Email Gateway (Aug 22 2022 at 19:51):From: Peter Lammich <lammich@in.tum.de>
Hi,
I can't prove that with hard numbers, but it feels like the frequency
of messages "z3: A prover error occurred" (and also for cvc4) has
significantly increased.
Here are some example outputs:
Email Gateway (Aug 22 2022 at 19:52):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Peter,
I think I have found the problem for Z3, but I cannot explain why it would appear now.
SMT (directly or via Sledgehammer) starts z3 with a timeout of XXs. However, SMT sees the answer "timeout" (as given by Z3) an error. So basically, it a timing issue: if SMT kills the call to the solver, everything is fine. Otherwise, it fails.
I don't know what happens for CVC4, I have not managed to reproduce the issue.
Can you try the attached patch?
Thanks,
Mathias
support_timeout
Last updated: Apr 19 2024 at 16:20 UTC