Old version of Z3 causes extremely slow solving times in incremental smt2 decision procedure

Question

Old version of Z3 causes extremely slow solving times in incremental smt2 decision procedure

Opened this issue 10 months ago · 0 comments

When using the incremental SMT2 decision procedure in combination with Z3 older than 4.12.0 some tests take long time.

As updating Z3 to version ≤ 4.12.0 seems to fix the issue it should be added to all CI jobs and as minimum requirement for using the incremental SMT2 decision procedure.

The test timing-out is:

cbmc/Unbounded_Array6/test.desc