Re: [isabelle] Troubleshooting a nondeterministic SMT failure



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.