[isabelle] Troubleshooting a nondeterministic SMT failure
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Troubleshooting a nondeterministic SMT failure
- From: Brandon Bohrer <bjbohrer at gmail.com>
- Date: Wed, 17 Nov 2021 14:30:57 -0500
- Authentication-results: cam.ac.uk; iprev=pass (mail-ua1-f54.google.com) smtp.remote-ip=188.8.131.52; spf=pass smtp.mailfrom=gmail.com; dkim=pass header.d=gmail.com header.s=20210112 header.a=rsa-sha256; arc=none
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!
Assistant Professor of Computer Science
Worcester Polytechnic Institute
This archive was generated by a fusion of
Pipermail (Mailman edition) and