Skip to content

array_exprt is not handled correctly in the incremental smt2 decision procedure #8080

Open
@esteffin

Description

@esteffin

In the incremental smt2 decision procedure the array_exprt should be handled before being dispatched to the convert_expr_to_smt.
However in the failing test array_exprt expression are forwarded to the convert_expr_to_smt causing an invariant violation.

The test failing this is:

  • cbmc/array-cell-sensitivity12/test_execution.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