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.

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


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