storm
storm copied to clipboard
Failing MultiObjectiveModelCheckerTest on Apple Silicon
As reported by @culechetoo here (thanks), there is a potential issue with the test case SparseMaPcaaMultiObjectiveModelCheckerTest.serverRationalNumbers
. See PR #349 for their cmake
and lldb
output.
~I haven't been able to reproduce it yet, but~ it seems to be Eigen related.
Note: This only covers a small part of Storms functionality, so most users should be fine.
Update: We were able to reproduce this on two Apple M2 systems. Systems with an M1 and M1Pro seem to be fine.
Hi!
Thank you for developing Storm. I'm posting another occurrence of this issue on a different machine here in the case that it might help.
I can also reproduce this issue with Storm 1.8.0 on an Apple M1 Ultra. CMake
shows that Eigen 3.4.0 is found:
-- Storm - Including Eigen 3.4.0 commit b0eded878d5d162d61583a286c0d8a45406ad1bc.
.
I'm not sure how to explicitly verify ARM compiled binaries are used throughout, but it seems so. A shipped version of carl
is used:
-- Storm - Linking with shipped carl 14.25 (include: /Users/marisg/git/storm_root_dir/storm/build/resources/3rdparty/carl/include/, library /Users/marisg/git/storm_root_dir/storm/build/resources/3rdparty/carl/lib/libcarl.dylib, CARL_USE_CLN_NUMBERS: OFF, CARL_USE_GINAC: OFF).
I ran lldb -- ./test-modelchecker-multiobjective
to produce a backtrace, the output is the same as reported in #349.
Please let me know if I can be of any help in terms of debug output or otherwise. I don't think this issue affects my current use of Storm.