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 type`empty` as an example. This is required for the following test: - cbmc/havoc_slice_checks/test.desc - cbmc/memset_null/test.desc