Z3 doesn't build with NVIDIA's compiler

[never_released]

This is some notes about building z3 with HPC SDK 20.7:

• in src/muz/base/dl_rule_set.h, “void restrict(const item_set & allowed);” has restrict compiled as a keyword, with the build as such failing, renaming the name resolves the issue.
• when building src/muz/base/dl_context.cpp:

`Block containing LandingPadInst must be jumped to only by the unwind edge of an invoke.
  %283 = landingpad %astruct.dt64
          cleanup
LLVM ERROR: Broken module found, compilation aborted!`

… the compiler breaks down, as such I built just that file with g++…

… but then, when running the testsuite (make test and then trying to run the testsuite):

`****************************************************************************************************
1 3 2
*ASSERTION VIOLATION
File: ../src/test/total_order.cpp
Line: 122
Failed to verify: to.lt(v[k], v[k+1])

Z3 4.8.10.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
`

Those tests were done on an AArch64 machine. (NVIDIA Carmel processor)

Thank you,
(Building z3 with NVIDIA's compilers · Issue #4694 · Z3Prover/z3 · GitHub)

[MatColgrove]

Thanks for the report. It looks like the authors fixed the “restrict” issue by updating the code. For the LLVM error, I added a problem report (TPR#29020) and sent it to engineering for further investigation. Using “g++” as a work around is fine since nvc++ is object compatible with g++, but you can also lower the optimization level from -O3 to -O1 since the error only occurs at higher optimization levels.

The runtime error also goes away if you compile all the source at lower optimization. Given the size and structure of the code, this will take me some time to dig into why the issue is occurring with higher optimization.

-Mat

[bleback]

This issue was fixed in our 20.11 release.