`array_exprt` is not handled correctly in the incremental smt2 decision procedure
Opened this issue · 0 comments
esteffin commented
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