storm icon indicating copy to clipboard operation
storm copied to clipboard

Failing MultiObjectiveModelCheckerTest on Apple Silicon

Open tquatmann opened this issue 1 year ago • 1 comments

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.

tquatmann avatar Apr 25 '23 06:04 tquatmann

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.

marisgg avatar Jun 07 '23 14:06 marisgg