Skip to content

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

@esteffin

Description

@esteffin

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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions