Check out this sample: https://raw.githubusercontent.com/sosy-lab/sv-benchmarks/master/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c I would suggest to you add a checker result when CrabLLVM was adopted in the verification.