Michael says: no known issues here.
Ruben: Current trunk version is able to solve all programs without any bugs.
SV-COMP'15 (programs where cbmc gave wrong/unknown answer):
unknown: ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c trunk version: finds a cex in 0.2 secs. The cex is verified in 5 secs by the witness checker.
unknown: ssh-simplified/s3_srvr_10_false-unreach-call.cil.c trunk version: finds a cex in 0.2 secs. The cex is verified in 2 secs by the witness checker.
true: ssh-simplified/s3_srvr_2_false-unreach-call.cil.c trunk version: finds a cex in 4 secs. The cex is verified in 5 secs by the witness checker.
witness timeout: locks/test_locks_15_false-unreach-call.c trunk version: finds a cex in 0.2 secs. The witness checkers times out. The cex has 63 states. If --beautify is used then the cex has 62 states. Minimising the cex may improve the performance of the witness checker. For example, ESBMC returns a cex with 48 states which is verified by the witness checker in 2 min 27 secs.
For using the witness checker do the following steps:
1. Download CPAchecker at: http://cpachecker.sosy-lab.org/CPAchecker-1.4-unix.tar.bz2 2. In the CPAchecker directory do the following command: scripts/cpa.sh -witness-check -spec <witness> -spec <propertyfile> <program> 3. Alternatively, you can use the following 'witness.sh' bash script: #!/bin/bash if [ "x$1" = "x" ]; then echo "USAGE: ./witness.sh <property-file> <program> <witness>" exit 1 fi Note: CPAchecker Requires Java 1.7 to work.