steakhal wrote: Alright. I had a look and it's interesting. For me, it crashes with `LLVM ERROR: Z3 error: unknown parameter 'rlimit'`, but that shouldn't matter. Actually `rlimit` should be available from 4.5.0, according to the [release notes](https://github.com/Z3Prover/z3/blob/master/RELEASE_NOTES.md) of Z3. That release note does not mention `rlimit` or `timeout` basically at all. However, by manual checking it seems that the from the very next patch release (4.8.9+) it compiles and passes the test you mentioned failing. I'd recommend you to upgrade Z3 to unblock your workflow. Given this, I'll propose an RFC later (in the upcoming weeks) to bump the minimal Z3 version to 4.8.9 (by one patch release), to follow the llvm guidelines.
Thanks for reporting this, and I hope this helps. https://github.com/llvm/llvm-project/pull/95128 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
