diffblue/cbmc

`array_exprt` is not handled correctly in the incremental smt2 decision procedure

Opened this issue · 0 comments

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