04/2019 regression on sv-benchmarks/c/ntdrivers/cdaudio_(true|false)-unreach-call.i.cil.c

[peterschrammel]

Observed on ba576c4
Still working on f5483b2

http://svcomp.cprover.org/svcomp19/benchexec/results-ReachSafety-Arrays/diff.html

--- begin invariant violation report ---
Invariant check failed
File: ../util/std_types.h:214 function: to_struct_union_type
Condition: can_cast_type<struct_union_typet>(type)
Reason: Precondition
Backtrace:
./cbmc-binary() [0x4f9fca]
./cbmc-binary() [0x4fad74]
./cbmc-binary() [0x430729]
./cbmc-binary() [0x7875e5]
./cbmc-binary() [0x78e8ee]
./cbmc-binary() [0x73b6b3]
./cbmc-binary() [0x58c085]
./cbmc-binary() [0x58a905]
./cbmc-binary() [0x4250c4]
./cbmc-binary() [0x4173e0]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0) [0x7f196db48830]
./cbmc-binary() [0x425e99]

[peterschrammel]

Same on sv-benchmarks/c/ntdrivers/cdaudio_false-unreach-call.i.cil.c

--- begin invariant violation report ---
Invariant check failed
File: ../util/std_types.h:214 function: to_struct_union_type
Condition: can_cast_type<struct_union_typet>(type)
Reason: Precondition
Backtrace:
./cbmc-binary() [0x4f9fca]
./cbmc-binary() [0x4fad74]
./cbmc-binary() [0x430729]
./cbmc-binary() [0x7875e5]
./cbmc-binary() [0x78e8ee]
./cbmc-binary() [0x73b6b3]
./cbmc-binary() [0x58c085]
./cbmc-binary() [0x58a905]
./cbmc-binary() [0x4250c4]
./cbmc-binary() [0x4173e0]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf0) [0x7f903fff0830]
./cbmc-binary() [0x425e99]

[tautschnig]

#2001 fixes these.