Fix incorrect result in ReachSafety-ControlFlow

[hbgit]

Verification tasks from SV-COMP

One possible solution for the incorrect true results is to adopt a redundant check.

• Add program invariant result in ERROR

• libfuzzer out: fuzzing was not performed, you have only executed the target code on a fixed set of inputs.

• ../../sv-benchmarks/c/ntdrivers-simplified/cdaudio_simpl1.cil-1.c
  - Checking KLEE options
  - Bug in process KLEE result "KLEE: WARNING: error opening file"

• ../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
  - Bug in process KLEE result "KLEE: WARNING: error opening file"

• ../../sv-benchmarks/c/ntdrivers-simplified/floppy_simpl4.cil-1.c
  - Bug in process KLEE result "KLEE: WARNING: error opening file"

KLEE was not able to find the bug:

• ../../sv-benchmarks/c/ntdrivers-simplified/kbfiltr_simpl2.cil-2.c
• ../../sv-benchmarks/c/ssh-simplified/s3_clnt_2.cil-1.c
• ../../sv-benchmarks/c/ssh-simplified/s3_clnt_3.cil-2.c
• ../../sv-benchmarks/c/ssh-simplified/s3_clnt_4.cil-2.c
• ../../sv-benchmarks/c/ssh/s3_clnt.blast.01.i.cil-2.c
• ../../sv-benchmarks/c/ssh/s3_clnt.blast.02.i.cil-1.c
• ../../sv-benchmarks/c/ssh/s3_clnt.blast.03.i.cil-1.c
• ../../sv-benchmarks/c/ssh/s3_clnt.blast.04.i.cil-1.c
• ../../sv-benchmarks/c/ssh/s3_srvr.blast.08.i.cil-2.c
• ../../sv-benchmarks/c/ssh/s3_srvr.blast.10.i.cil-2.c
• ../../sv-benchmarks/c/ssh/s3_srvr.blast.11.i.cil-1.c
• ../../sv-benchmarks/c/ssh/s3_srvr.blast.15.i.cil-1.c