Arie Gurfinkel

`test/opsem/nham.1.ll` gets stuck during simplification in z3. Needs to be triaged once migration to llvm9 is complete. The test passes quickly in `llvm5` (current master). Details on how to reproduce...

Support for overflow and underflow operators over bv

2

Both Z3 and Boolector provide API to detect whether arithmetic over bit-vectors overflows/underflows. This seems to be missing from Yices. Is there some good way to get similar functionality. I...

Potentially unused variable

1

https://github.com/seahorn/seahorn/blob/3f50ac10ce028e117c449d0a51ecfef0089a012f/lib/seahorn/BvOpSem2TrackingRawMemMgr.cc#L429 Clang-12 says that this variable is unused. Is it needed?

https://github.com/seahorn/seahorn/blob/48405825b6b36f1fd853e712378ba0137b48c638/lib/seahorn/BvOpSem2.cc#L615 On that line, and elsewhere where `hana` is used, clang gives a compilation warning about left operator of comma. PTAL

https://github.com/seahorn/seahorn/blob/48405825b6b36f1fd853e712378ba0137b48c638/lib/seahorn/BvOpSem2FatMemMgr.cc#L311 @priyasiddharth please review. Found by clang. Seems to be definitely wrong since the function calls itself immediately. Should be calling `m_main.ptrAdd` instead. I'm committing a fix in `dev12` branch....