Email Gateway (Aug 22 2022 at 18:59): Email Gateway (Aug 22 2022 at 18:59):From: Dominique Unruh <unruh@ut.ee>
Hello,
in an Isabelle build (involving only AFP theories), I get the following
message in the log:
[much stuff]
*** Solver z3: Solver terminated abnormally with error code 127
*** At command "by" (line 1266 of
"/builds/unruh/qrhl-tool/tmp/qrhl-0.5alpha/isabelle-afp/Polynomial_Interpolation/Missing_Polynomial.thy")
This error does not occur on my own computer, only when I run the build on
the Gitlab CI servers.
I cannot find more information in the log file.
Is there any place where Z3 would output error messages?
Or some flag that can be activated to get more debug output?
Or has someone encountered this error before and knows what it is about?
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 18:59):From: Sascha Böhme <boehmes@in.tum.de>
Hi Dominique,
This error might have been caused by some exception in Z3. In my experience, that could very well be some memory issue like a null-pointer exception. To get more information, you can use the option [[smt_trace]] just before the invocation of Z3 like so:
lemma True using [[smt_trace]] by smt
This will emit some more details about the things that are done in Isabelle to communicate with Z3. In particular you get the data that is sent to Z3. If you provide me with this information, I might have a look if some newer version of Z3 has already solved this issue. Otherwise we can pass the data to the Z3 developers to analyze and resolve this issue.
Regards,
Sascha
Email Gateway (Aug 22 2022 at 19:00):From: Dominique Unruh <unruh@ut.ee>
Hi,
smt_trace helped. Thanks! The message is
SMT: Result:
/builds/unruh/qrhl-tool/tmp/qrhl-0.5alpha/isabelle-temp/setups/Isabelle2018/contrib/z3-4.4.0pre-2/x86_64-linux/z3:
error while loading shared libraries: libgomp.so.1: cannot open shared
object file: No such file or directory
so all I had to do was to use a docker image containing that library.
As a feature suggestion: perhaps the smt-method can be changed so that this
message (or whatever other error message z3 gives) is output even without
smt_trace (only in case of z3 failing, of course).
Best wishes,
Dominique.
Last updated: Apr 19 2024 at 16:20 UTC