Dat3M 4.2.0 is out!

What's Changed

• Update README.md by @hernanponcedeleon in #707
• add support to show source location in witness graph for spirv by @CapZTr in #738
• Pass the C file to the svcomp runner rather than the optimized llvm by @hernanponcedeleon in #739
• Add support for atomic_exchange_explicit in litmus code by @hernanponcedeleon in #740
• Backwards reaching definitions by @xeren in #726
• Better may set for sync barrier by @natgavrilenko in #745
• Fix UI parsing by @ThomasHaas in #747
• Relation analysis with immutable and lazy data structures by @natgavrilenko in #743
• Updated model in spirv tests by @natgavrilenko in #749
• Support for Apple silicon by @hernanponcedeleon in #748
• Some improvements to aarch64 pseudo-assembly by @hernanponcedeleon in #741
• Add support for show statement in cat parser by @hernanponcedeleon in #742
• Introduce stdlib.cat by @hernanponcedeleon in #751
• Add support for variable-sized and variable-aligned allocations by @ThomasHaas in #750
• Require the existence of violation node when validate violation witness by @hernanponcedeleon in #754
• Add OpenCL Model by @tonghaining in #744
• Fix overlap queries in Alias Analysis by @xeren in #753
• Configuration files and management by @xeren in #752
• Svcomp config by @hernanponcedeleon in #756
• Fix #757 by @ThomasHaas in #758
• Allow bounds to be saved to and loaded from files by @hernanponcedeleon in #759
• Improve PPC grammar and visitor by @hernanponcedeleon in #762
• Fix usages of non-determinism in intrinsics by @ThomasHaas in #763
• Improvements for SVCOMP 2025 by @hernanponcedeleon in #765
• Check if events may alias when deriving RA knowledge from witnesses (… by @hernanponcedeleon in #766
• Fix witnesses excluding the rf edges they enforce. by @xeren in #771
• Spirv OpUndef by @natgavrilenko in #769
• Remove svcomp specific options by @hernanponcedeleon in #773
• Support explicitly defined offsets in aggregate type by @natgavrilenko in #770
• Remove empty tag from vulkan litmus tests by @natgavrilenko in #774
• Support of Showing Local Events Location in Spirv by @CapZTr in #761
• Fix handling of empty type by @ThomasHaas in #776
• Further changes for SVCOMP 2025 by @hernanponcedeleon in #777
• Update to version 4.2.0 by @hernanponcedeleon in #782

New Contributors

• @CapZTr made their first contribution in #738

Full Changelog: 4.1.0...4.2.0