Rafael Sá Menezes

Ok, lots of requests here: > With latest master of ESBMC and Z3 this issue does not exist anymore. What is the policy on updating dependencies like Z3? Since we...

These are the current failing tests for Z3. We still have some performance issues. These tests were executed at: - Ubuntu 20.04 - Z3 4.8.9 (still has the memory bug)...

> A little more info, please. I've added to the original comment

> These are not related to this issue. Ow, I will remove those. > This issue was about a specific performance bug in Z3, which is fixed in ESBMC and...

> Where do you see this issue happening? For me it is fixed: That's the problem, I am still trying to get a test case that showcase this (this is...

> On the [fb/tst-z3](https://github.com/esbmc/esbmc/tree/fb/tst-z3) branch I've allowed via the benchexec action to pass --default-solver z3 as cmdline options, but I don't have a Ubuntu-20.04 Selecting which solver to use looks...

I agree, we may close this issue.

Just to link: This will close https://github.com/esbmc/esbmc/issues/33

> Are there any such constructs left? I couldn't find one. I've updated the issue

We do not. I think the best approach is to instrument an assume(0) at its end. Right?