Dear Florian,
thanks for sharing the problem! You could give a link to a failing job pair for further investigation, but it already sounds like a problem you should report to the StarExec team: https://github.com/StarExec/StarExec/issues. Maybe additionally notify Aaron.
Best, Akihisa
On 2021/06/20 1:34, Florian Frohn wrote:
Dear all,
I'm struggling with StarExec and running out of ideas, so if anybody experienced similar issues, please let me know:
On StarExec, my tool LoAT reliably crashes on some problems with error messages like:
/export/starexec/sandbox/solver /bin/starexec_run_loat_nonterm_debug: line 4: 62638 Illegal instruction (core dumped) ./loat-static --plain --timeout $TO --nonterm $1
The crash happens after a few milliseconds. The same binary works perfectly fine on my PC and in the VM (https://www.starexec.org/vmimage/).
My tool is written in C++. I build the binary and its dependencies (Z3, Yices, ginac, ntl, purrs) with gcc in a voidlinux docker container. It's statically linked with musl (http://musl.libc.org/).
I tried to compile it in the VM instead, but one more dependency (giac) is missing in the CentOS repositories. Since building giac from scratch seems rather complex, I gave up at that point.
I disabled optimizations as far as possible (by compiling LoAT as well as its dependencies with -O0), but that didn't change anything. Running the same binary with valgrind or the clang/gcc sanitizer for undefined behavior does not reveal any problems either.
If you have any ideas what else to try or how to debug such issues on StarExec, please let me know!
Thanks, Florian _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de