Re: [isabelle] Troubleshooting a nondeterministic SMT failure



Hi Mathias,

Thanks for the quick reply. I actually have already tried setting high timeouts as well (e.g. declare[[smt_timeout=10000]]) but did not mention that explicitly in my first email because all of the successful smt calls and all of the failing smt calls complete quite quickly (e.g. 0.2 seconds). Note that things are failing on my faster machine and succeeding on my slower machine.

By the way, I also tried declare[[smt_timeout=0]] right now, just in case (on the Isabelle2021 release, not an RC). The result was that it set the timeout to 0 seconds rather than infinity, so that all of the smt calls fail every time. At least that's a deterministic behavior, so maybe it's an improvement :)

Let me know if there are any other troubleshooting steps that I should try next, or if there is any additional debug info that would be helpful to post to the list.

Thanks!
-Brandon 



On Thu, Nov 18, 2021 at 7:18 AM Mathias Fleury <mathias.fleury12 at gmail.com> wrote:
Hi Brandon,

The most likely problem is that the thread launching the SMT solver is not started fast enough. Set the timeout to infinity with ``declare [[smt_timeout=0]]`` should do the trick (this is the default value in Isabelle2021-1-RC3 anyway).


Best,
Mathias

Le jeu. 18 nov. 2021 à 12:01, Brandon Bohrer <bjbohrer at gmail.com> a écrit :
Hi all,

Short version: I am getting failures in the "smt" method, nondeterministically on the released version of an AFP article (Poincare-Bendixson); what troubleshooting steps are recommended next?

Since I have already taken some troubleshooting steps, the rest of my email describes what I have tried already, to help speed up troubleshooting. Note that I have one machine with the problem and one without it, which may help.

Failing command (for example):
$ isabelle build -d <path-to-afp>/thys  -b Poincare_Bendixson

Isabelle version: Tried 2019 and 2021 with matching AFP versions. No change.

Machine & OS information:
I have tested this on two machines, call them machine W (where the proof works) and machine B (where it's broken). Both run Windows 10. Both use the built-in Windows antivirus and I am prevented from turning it off completely, but I have added exclusions for my Isabelle and AFP directories. Also turned off search indexing of file contents.

The first difference between the machines that comes to mind: machine W is newer and faster; it has both an SSD and an HDD. However, I moved Isabelle (including .isabelle) and the AFP to my HDD, and the issue persisted. I still wonder whether Windows is using the SSD without my knowing, and racing.

Solvers: I tried Z3, CVC4, and VeriT. No change.

Timing and nondeterminism:
It is definitely nondeterministic. If I rerun an offending line through the jEdit UI, it usually works on a second or third try. Whether it succeeds or fails, it always returns quickly (e.g. 0.2 seconds for one of them). So it is not a timeout issue.

SMT tracing information:
I enabled the smt_trace option and noticed something: When "smt" fails, the "SMT: Result:" message doesn't have any, well, results after it, but when "smt" succeeds, there is lots of trace info. Is this expected behavior or is it a clue about what's going wrong? I can rerun and post the whole trace if needed.

Thanks for any advice you can provide!

Brandon Bohrer
Assistant Professor of Computer Science
Worcester Polytechnic Institute


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