Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2021-1-RC3: verit errors

Email Gateway (Nov 14 2021 at 12:54):

From: Peter Lammich <lammich@in.tum.de>
I get a lot of verit errors from sledgehammer.

"verit": Prover error:
Solver "verit" failed -- enable tracing using the "smt_trace" option
for details

And there is no smt_trace option to sledgehammer, at least sledgehammer
[smt_trace] tells me so, and the sledgehammer manual does not contain
the string smt_trace!

Email Gateway (Nov 15 2021 at 12:30):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Peter,

It is a global option, not a sledgehammer-only option, so:

supply [[smt_trace]]

Do you have any example with a failure?

Mathias

Email Gateway (Nov 17 2021 at 09:20):

From: Peter Lammich <lammich@in.tum.de>
Hi Mathias.

On Mon, 2021-11-15 at 13:25 +0100, Mathias Fleury wrote:

supply [[smt_trace]]

Thanks.

Do you have any example with a failure?

Here you go.

Email Gateway (Nov 17 2021 at 09:31):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Peter,

I have a patch for that issue (isabelle build -a is torturing my
computer for now...).

The problems comes from the fact that veriT does not support
bit-vectors, but that they are generated by default by sledgehammer and smt.

Thanks for reporting,

Mathias

Last updated: Jan 04 2025 at 20:18 UTC