Re: [isabelle] Isabelle2021-1-RC3: smt (verit) behaves differently under Linux and Windows



Hi all,

On 15.11.21 17:34, Mathias Fleury wrote:
We have pinned the issue to a behavior difference between Windows and Linux in the "--inst-deletion" option in veriT itself. Hans-Jörg (in CC) is currently investigating the issue in the veriT source code.

Hans-Jörg and Mathias have been hard at work in the last days debugging this issue, finding a fix, and testing a new patched version 2021.06.2-rmx. The proof search heuristics changed as a result, but no failing smt calls were observed in the AFP.

The source code is available at the following address.

https://verit.loria.fr/download/2021.06.2/verit-2021.06.2-rmx.tar.gz

And it can now be built and added as default component for both the release candidate and the development version.

Cheers,
Martin




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.