diffblue/cbmc

Support for `empty` types is not yet implemented in incremental smt2 decision procedure

Opened this issue · 0 comments

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