On 5/25/2019 7:18 PM, Makarius wrote:
It is better now, but I still get 6-7 failures in 400 runs. (It was 20 failures with Isabelle2019-RC2)On 24/05/2019 20:59, Makarius wrote:On 24/05/2019 19:09, Mathias Fleury wrote:I managed to find an old windows machine and I can reproduce the bug (sometimes at least). And the results are just weird. smt works as follows: (exec 2>&1; z3 ‹input_file›)> ‹temporary_file›The "(exec ...) > ..." scheme goes back to the original version by Jasmin Blanchette from 2014: http://isabelle.in.tum.de/repos/isabelle/rev/624faeda77b5#l12.56 -- so the history does not say anything about the reasons for that. Maybe Jasmin can recall them. To robustify that bash script, I have made the following changes for the next release candidate: * Update of Cygwin: https://isabelle.sketis.net/repos/isabelle-release/rev/b0fd8167bb9b * Avoid extra subprocess: https://isabelle.sketis.net/repos/isabelle-release/rev/2e101846ad8f I will publish Isabelle2019-RC3 tomorrow, with all the other minor changes that have accumulated in the past 2 weeks.The above changes are already in Isabelle2019-RC3. Can you try if it makes a difference.
On 5/24/2019 7:09 PM, Mathias Fleury wrote:
Out of curiosity, do you have an SSD or a hard drive?
I have an SSD. Fabian
Description: S/MIME Cryptographic Signature