Tool CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 12   480 87 false(unreach-call) 1 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 13     440   unknown 0 wit inspect 5.0  220 true -32 wit inspect .79   19    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 35   1600 270 false(unreach-call) 1 wit inspect 4.5  270 false(unreach-call) 1 wit inspect 10     370   unknown 0 wit inspect 4.7  210 true -32 wit inspect .75   19    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c witness invalid (false(unreach-call)) 0 wit inspect 38   1800 320 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c witness invalid (false(unreach-call)) 0 wit inspect 13   510 86 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 42   2000 350 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 13    420 true 2 wit inspect 100     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 53   3000 510 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 370    7000 true 2 wit inspect 68     870  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1 wit inspect 27   1500 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.8
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 1 wit inspect 36   1900 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 47 error (2) 0 wit inspect .019 4.9
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 7.0 380 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 18     500  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 8.8 470 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  270 true 2 wit inspect 16     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   530 110 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 9.9   350   unknown 0 wit inspect 2.5  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 14   520 110 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 11     350   unknown 0 wit inspect 3.6  220 true -32 wit inspect .64   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 15   550 120 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 5.8   340   unknown 0 wit inspect 3.6  210 true -32 wit inspect .68   20    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 13   530 93 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 11     350   unknown 0 wit inspect 3.7  210 true -32 wit inspect .69   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 45   1900 330 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 7.5   320   unknown 0 wit inspect 4.2  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 18   600 140 false(unreach-call) 1 wit inspect 5.6  280 false(unreach-call) 1 wit inspect 16     540   unknown 0 wit inspect 4.9  220 true -32 wit inspect .68   21    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 240   6600 2000 false(unreach-call) 1 wit inspect 5.1  280 false(unreach-call) 1 wit inspect 13     490   unknown 0 wit inspect 4.7  220 true -32 wit inspect .68   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   4600 9500 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .99 47 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 74   3400 600 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 10     330   unknown 0 wit inspect 4.1  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.5 410 70 false(unreach-call) 1 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 8.2   370   unknown 0 wit inspect 4.1  210 true -32 wit inspect .69   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.7 420 60 false(unreach-call) 1 wit inspect 4.8  280 false(unreach-call) 1 wit inspect 10     390   unknown 0 wit inspect 5.3  220 true -32 wit inspect .66   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.4 300 38 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.8   300   unknown 0 wit inspect 4.5  240 true -32 wit inspect .65   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 22   1000 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    400 true 2 wit inspect 35     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 10   480 88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    400 true 2 wit inspect 36     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.9 470 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    420 true 2 wit inspect 42     1100  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.7 480 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    400 true 2 wit inspect 38     1000  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c true 2 wit inspect 14   510 98 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6200 true 2 wit inspect 33     910  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 310 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 11    320 false(unreach-call) -16 wit inspect 5.5   260  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.5 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  290 false(unreach-call) -16 wit inspect 6.5   260  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c true 2 wit inspect 9.1 460 74 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 true 2 wit inspect 48     1100  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c true 2 wit inspect 12   530 97 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4700 true 2 wit inspect 36     1200  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c true 2 wit inspect 9.0 470 79 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5100 true 2 wit inspect 45     930  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c true 2 wit inspect 18   690 160 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4700 true 2 wit inspect 34     940  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c true 2 wit inspect 13   540 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 true 2 wit inspect 47     1000  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c true 2 wit inspect 14   490 110 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4500 true 2 wit inspect 42     1100  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 4.8 300 44 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 3.3  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 4.8 300 46 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.4   270   unknown 0 wit inspect 3.4  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.3 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 18     660  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.5 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4  280 true 2 wit inspect 23     1200  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.4 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  280 true 2 wit inspect 31     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.3 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 true 2 wit inspect 48     3700  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.4 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  310 true 2 wit inspect 75     5200  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.4 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  290 out of memory 0 wit inspect 98     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  270 true 2 wit inspect 10     280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 11     320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.0 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  280 true 2 wit inspect 10     370  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.1 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  280 true 2 wit inspect 12     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 3.2 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  280 true 2 wit inspect 15     520  
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 22   890 150 false(unreach-call) 1 wit inspect 14    670 false(unreach-call) 1 wit inspect 15     480   unknown 0 wit inspect 5.1  280 timeout 0 wit inspect 96      19    - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 32   1300 220 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0011 .32 - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 16   700 120 false(unreach-call) 1 wit inspect 8.6  300 true -32 wit inspect 14     450   unknown 0 wit inspect 5.8  270 error (2) 0 wit inspect .95   19    - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 35   1400 280 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .027 4.8
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 30   1500 260 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 14    490 true 2 wit inspect 180     4600  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c true 1 wit inspect 38   1500 290 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .019 4.9
ntdrivers/parport_true-unreach-call.i.cil.c true 1 wit inspect 110   4400 940 - wit inspect - wit inspect - wit inspect - wit inspect error 0 wit inspect 13    440 timeout 0 wit inspect 960     4800  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 14   530 100 error (invalid witness file) 0 wit inspect 3.0  180 unknown 0 wit inspect 2.9   200   error (invalid witness file) 0 wit inspect 3.4  210 error (invalid witness file) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 13   490 110 false(unreach-call) 1 wit inspect 5.1  280 true -32 wit inspect 8.4   340   unknown 0 wit inspect 5.0  250 error (2) 0 wit inspect .77   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 14   510 89 false(unreach-call) 1 wit inspect 6.6  270 true -32 wit inspect 8.3   320   unknown 0 wit inspect 4.8  220 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 13   490 94 false(unreach-call) 1 wit inspect 5.3  270 true -32 wit inspect 9.6   320   unknown 0 wit inspect 4.8  220 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 7.6 400 69 error (invalid witness file) 0 wit inspect 3.3  210 unknown 0 wit inspect 3.5   200   error (invalid witness file) 0 wit inspect 3.7  210 error (invalid witness file) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 7.5 400 67 error (invalid witness file) 0 wit inspect 2.8  170 unknown 0 wit inspect 4.5   200   error (invalid witness file) 0 wit inspect 4.0  210 error (invalid witness file) 0 wit inspect .71   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 7.6 410 60 error (invalid witness file) 0 wit inspect 2.9  210 unknown 0 wit inspect 3.7   190   error (invalid witness file) 0 wit inspect 3.1  180 error (invalid witness file) 0 wit inspect .68   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 7.5 410 63 error (invalid witness file) 0 wit inspect 3.5  180 unknown 0 wit inspect 5.2   280   error (invalid witness file) 0 wit inspect 3.7  210 error (invalid witness file) 0 wit inspect .72   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 9.9 480 81 error (invalid witness file) 0 wit inspect 3.0  210 unknown 0 wit inspect 4.0   200   error (invalid witness file) 0 wit inspect 4.3  210 error (invalid witness file) 0 wit inspect .71   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 8.9 500 76 error (invalid witness file) 0 wit inspect 2.9  210 unknown 0 wit inspect 4.5   190   error (invalid witness file) 0 wit inspect 4.2  210 error (invalid witness file) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 10   470 76 error (invalid witness file) 0 wit inspect 3.0  210 unknown 0 wit inspect 4.3   200   error (invalid witness file) 0 wit inspect 3.2  180 error (invalid witness file) 0 wit inspect .69   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 8.6 500 77 error (invalid witness file) 0 wit inspect 3.5  180 unknown 0 wit inspect 3.6   200   error (invalid witness file) 0 wit inspect 3.2  210 error (invalid witness file) 0 wit inspect .69   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 8.8 490 73 error (invalid witness file) 0 wit inspect 2.9  200 unknown 0 wit inspect 4.5   200   error (invalid witness file) 0 wit inspect 2.2  210 error (invalid witness file) 0 wit inspect .69   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 9.6 500 83 error (invalid witness file) 0 wit inspect 3.0  220 unknown 0 wit inspect 4.0   200   error (invalid witness file) 0 wit inspect 3.4  210 error (invalid witness file) 0 wit inspect .72   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 9.6 500 72 error (invalid witness file) 0 wit inspect 3.8  170 unknown 0 wit inspect 3.2   200   error (invalid witness file) 0 wit inspect 3.2  180 error (invalid witness file) 0 wit inspect .74   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 8.4 500 72 error (invalid witness file) 0 wit inspect 3.6  200 unknown 0 wit inspect 3.6   200   error (invalid witness file) 0 wit inspect 2.3  210 error (invalid witness file) 0 wit inspect .69   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 8.9 490 78 error (invalid witness file) 0 wit inspect 2.8  180 unknown 0 wit inspect 4.2   200   error (invalid witness file) 0 wit inspect 3.3  210 error (invalid witness file) 0 wit inspect .70   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 9.4 480 71 error (invalid witness file) 0 wit inspect 3.7  180 unknown 0 wit inspect 4.1   200   error (invalid witness file) 0 wit inspect 3.3  210 error (invalid witness file) 0 wit inspect .71   18    - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness invalid (false(unreach-call)) 0 wit inspect 9.2 500 69 error (invalid witness file) 0 wit inspect 3.4  180 unknown 0 wit inspect 4.2   200   error (invalid witness file) 0 wit inspect 3.8  180 error (invalid witness file) 0 wit inspect .76   18    - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 14   530 120 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.4  180 unknown 0 wit inspect 4.5   200  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 15   550 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.7  170 unknown 0 wit inspect 4.6   200  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 15   530 140 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.2  180 unknown 0 wit inspect 3.6   200  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 14   530 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.2  180 unknown 0 wit inspect 4.0   200  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 8.7 500 64 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9  180 unknown 0 wit inspect 3.6   200  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 8.2 430 75 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.0  180 unknown 0 wit inspect 3.8   210  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 17   600 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.1  180 unknown 0 wit inspect 3.4   200  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.5 490 73 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.1  170 unknown 0 wit inspect 4.0   200  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 12   510 86 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 4.0  180 unknown 0 wit inspect 3.5   200  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.5 510 81 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9  210 unknown 0 wit inspect 3.6   190  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 10   520 77 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.7  180 unknown 0 wit inspect 3.4   190  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.5 490 78 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9  180 unknown 0 wit inspect 3.3   190  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 13   510 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.3  200 unknown 0 wit inspect 4.3   190  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 9.3 500 74 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.4  180 unknown 0 wit inspect 3.4   190  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 15   580 120 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.7  180 unknown 0 wit inspect 4.0   190  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 14   520 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9  180 unknown 0 wit inspect 3.3   200  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 15   600 110 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.9  200 unknown 0 wit inspect 3.7   200  
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 94 -190 5200 87000 57000 42 20 160 9200 42 -112 260 11000 42 0 150 8100 42 -480 120 690 52 40 6900 53000 52 20 2200 50000
    correct results 49 78 920 39000 7500 20 20 110 5800 16 16 160 6000 0 0 20 40 150 6300 26 52 1100 34000
        correct true 29 58 330 17000 2800 0 0 0 0 20 40 150 6300 26 52 1100 34000
        correct false 20 20 590 21000 4700 20 20 110 5800 16 16 160 6000 0 0 0 0
    correct-unconfimed results 4 4 210 9200 1700 0 0 0 0 0 0
        correct-unconfirmed true 4 4 210 9200 1700 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 17 -272 210 8900 1700 0 4 -128 40 1400 0 15 -480 10 290 0 2 -32 12 520
        incorrect true 0 0 4 -128 40 1400 0 15 -480 10 290 0 0
        incorrect false 17 -272 210 8900 1700 0 0 0 0 0 2 -32 12 520
score (94 tasks, max score: 146) -190 20 -112 0 -480 40 20
Run set cpa-bam-bnb.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-ControlFlow