Support for `empty` types is not yet implemented in incremental smt2 decision procedure
Opened this issue · 0 comments
esteffin commented
Support for the empty
type is not yet implemented in incremental smt2 decision procedure.
This causes a failure with invariant in convert_type_to_smt_sort
about unimplemented generation of formulas for typeempty
as an example.
This is required for the following test:
- cbmc/havoc_slice_checks/test.desc
- cbmc/memset_null/test.desc