Tool CPAchecker 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-12-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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 26   990 200 false(unreach-call) 1 wit inspect 18    730 true -32 wit inspect 12     440   unknown 0 wit inspect 4.0  220 error (1) 0 wit inspect .71   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 43   2000 340 false(unreach-call) 1 wit inspect 20    490 false(unreach-call) 1 wit inspect 12     500   unknown 0 wit inspect 3.5  210 error (1) 0 wit inspect .61   19    - wit inspect - wit inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 45   1900 380 false(unreach-call) 1 wit inspect 28    680 false(unreach-call) 1 wit inspect 12     470   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .67   19    - wit inspect - wit inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 16   640 120 true -32 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.5   330   unknown 0 wit inspect 3.6  220 true -32 wit inspect .69   19    - wit inspect - wit inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) -16 wit inspect 26   810 210 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    840 true 2 wit inspect 28     520  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) -16 wit inspect 10   480 90 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 true 2 wit inspect 11     400  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 86   3800 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3  370 true 2 wit inspect 62     910  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 200   4000 2300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4  370 true 2 wit inspect 79     980  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 11   500 95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 15     510  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 15   620 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  270 true 2 wit inspect 19     520  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 42   1600 350 false(unreach-call) 1 wit inspect 39    1900 false(unreach-call) 1 wit inspect 9.8   370   unknown 0 wit inspect 3.5  220 error (1) 0 wit inspect .57   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 110   4200 1300 false(unreach-call) 1 wit inspect 38    1900 false(unreach-call) 1 wit inspect 10     370   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .63   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 110   4200 1100 false(unreach-call) 1 wit inspect 37    1900 false(unreach-call) 1 wit inspect 11     410   unknown 0 wit inspect 3.8  210 error (1) 0 wit inspect .57   19    - wit inspect - wit inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 110   4200 1200 false(unreach-call) 1 wit inspect 37    1900 false(unreach-call) 1 wit inspect 9.3   370   unknown 0 wit inspect 3.8  210 error (1) 0 wit inspect .57   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 240   4500 2600 false(unreach-call) 1 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 8.3   320   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .57   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 210   3800 2500 true -32 wit inspect 5.0  270 false(unreach-call) 1 wit inspect 9.4   440   unknown 0 wit inspect 3.8  220 true -32 wit inspect .70   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 400   4700 5100 true -32 wit inspect 5.0  270 true -32 wit inspect 9.4   400   unknown 0 wit inspect 3.8  210 true -32 wit inspect .75   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 73   3700 730 true -32 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 7.8   360   unknown 0 wit inspect 3.9  220 true -32 wit inspect .72   20    - wit inspect - wit inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 310   5200 3600 false(unreach-call) 1 wit inspect 5.8  270 false(unreach-call) 1 wit inspect 11     400   unknown 0 wit inspect 3.7  220 error (1) 0 wit inspect .58   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 27   1300 240 false(unreach-call) 1 wit inspect 5.1  280 false(unreach-call) 1 wit inspect 9.7   360   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .61   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 25   1300 200 false(unreach-call) 1 wit inspect 5.4  280 false(unreach-call) 1 wit inspect 10     370   unknown 0 wit inspect 4.0  220 error (1) 0 wit inspect .60   19    - wit inspect - wit inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 71   3800 710 true -32 wit inspect 4.7  280 false(unreach-call) 1 wit inspect 7.4   310   unknown 0 wit inspect 3.4  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 54   3300 530 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    410 true 2 wit inspect 29     1000  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 39   2600 370 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    400 true 2 wit inspect 35     1200  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 44   2600 310 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 12    430 true 2 wit inspect 33     1200  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 39   2600 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    400 true 2 wit inspect 32     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c true 2 wit inspect 41   2600 410 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5000 true 2 wit inspect 30     910  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 9.9 450 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  300 true 2 wit inspect 7.7   310  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.2 300 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  280 true 2 wit inspect 6.4   260  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c true 2 wit inspect 120   3500 1300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4800 true 2 wit inspect 48     1100  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c true 2 wit inspect 67   3200 740 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4700 true 2 wit inspect 38     1100  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c true 2 wit inspect 82   3400 950 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    5000 true 2 wit inspect 37     960  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c true 2 wit inspect 67   3800 650 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 true 2 wit inspect 36     920  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c true 2 wit inspect 92   3900 1100 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    4500 true 2 wit inspect 41     980  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c true 2 wit inspect 45   2400 380 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 true 2 wit inspect 30     1200  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 3.2 280 28 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.2   270   unknown 0 wit inspect 2.9  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 3.1 270 30 false(unreach-call) 1 wit inspect 3.4  270 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.2  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 120   4700 1300 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.1  270 true 2 wit inspect 19     700  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 310   6800 3600 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.8  270 true 2 wit inspect 19     1100  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout (true) 0 wit inspect 920   13000 10000 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.1  280 true 2 wit inspect 24     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   11000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .031 4.9
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   10000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .022 5.0
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   10000 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 4.9
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 10   460 67 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.5  270 true 2 wit inspect 7.9   270  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 13   620 93 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.6  270 true 2 wit inspect 8.8   310  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 23   1300 150 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.6  270 true 2 wit inspect 10     390  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 32   2400 310 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.4  270 true 2 wit inspect 12     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 53   4000 540 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.8  270 true 2 wit inspect 13     510  
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4800 11000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 34   1200 280 timeout 0 wit inspect 92    2100 true -32 wit inspect 14     470   unknown 0 wit inspect 5.4  280 timeout 0 wit inspect 96      20    - wit inspect - wit inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 24   760 180 true -32 wit inspect 7.0  280 true -32 wit inspect 24     580   unknown 0 wit inspect 6.1  300 timeout 0 wit inspect 96      20    - wit inspect - wit inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 28   1000 200 true -32 wit inspect 5.9  270 true -32 wit inspect 11     440   unknown 0 wit inspect 4.8  270 error (2) 0 wit inspect .98   19    - wit inspect - wit inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 10   470 80 true -32 wit inspect 7.1  300 unknown 0 wit inspect 78     930   unknown 0 wit inspect 6.7  300 error (2) 0 wit inspect 1.6    22    - wit inspect - wit inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 33   1200 260 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 39    740 true 2 wit inspect 24     540  
ntdrivers/diskperf_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 40   1500 330 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.8  400 true 2 wit inspect 14     490  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c true 1 wit inspect 150   3900 1700 - wit inspect - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 890    7000 timeout 0 wit inspect 960     5500  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c true 2 wit inspect 300   4100 3500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 true 2 wit inspect 760     6700  
ntdrivers/parport_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 17   610 140 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 8.8  350 true 2 wit inspect 38     750  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c timeout 0 wit inspect 900   2600 13000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .88 48 error (invalid witness file) 0 wit inspect .0037 .31 - wit inspect - wit inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c timeout 0 wit inspect 900   3600 12000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c timeout 0 wit inspect 900   3400 13000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0017 .28 - wit inspect - wit inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c timeout 0 wit inspect 900   2500 11000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0039 .34 - wit inspect - wit inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 12   550 100 true -32 wit inspect 5.2  260 true -32 wit inspect 7.9   330   unknown 0 wit inspect 4.1  270 error (2) 0 wit inspect .83   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 12   470 100 true -32 wit inspect 5.2  270 true -32 wit inspect 8.5   330   unknown 0 wit inspect 4.1  260 error (2) 0 wit inspect .79   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 11   470 100 true -32 wit inspect 5.2  270 true -32 wit inspect 8.6   340   unknown 0 wit inspect 4.2  260 error (2) 0 wit inspect .78   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 11   480 83 true -32 wit inspect 5.2  270 true -32 wit inspect 8.1   330   unknown 0 wit inspect 4.1  270 error (2) 0 wit inspect .81   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 16   660 130 true -32 wit inspect 5.3  260 timeout 0 wit inspect 97     820   unknown 0 wit inspect 4.3  260 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 21   650 170 true -32 wit inspect 5.1  260 timeout 0 wit inspect 97     820   unknown 0 wit inspect 4.4  260 error (2) 0 wit inspect .83   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 140   3800 1700 true -32 wit inspect 5.9  270 timeout 0 wit inspect 96     1600   unknown 0 wit inspect 4.6  270 error (2) 0 wit inspect .81   21    - wit inspect - wit inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 18   620 140 true -32 wit inspect 5.2  270 timeout 0 wit inspect 97     800   unknown 0 wit inspect 4.1  260 error (2) 0 wit inspect .82   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 84   3700 910 true -32 wit inspect 5.7  280 timeout 0 wit inspect 96     1900   unknown 0 wit inspect 4.5  270 error (2) 0 wit inspect .79   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 94   3800 900 true -32 wit inspect 5.6  270 timeout 0 wit inspect 96     800   unknown 0 wit inspect 4.3  260 error (2) 0 wit inspect .77   19    - wit inspect - wit inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 14   560 94 true -32 wit inspect 5.6  260 timeout 0 wit inspect 96     880   unknown 0 wit inspect 4.4  260 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 20   680 160 true -32 wit inspect 5.7  280 timeout 0 wit inspect 97     810   unknown 0 wit inspect 4.1  260 error (2) 0 wit inspect .83   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 14   590 110 true -32 wit inspect 5.1  260 timeout 0 wit inspect 96     850   unknown 0 wit inspect 4.2  230 error (2) 0 wit inspect .80   20    - wit inspect - wit inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900   4100 13000 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .053 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0040 .29 - wit inspect - wit inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 13   600 100 true -32 wit inspect 5.4  260 timeout 0 wit inspect 96     810   unknown 0 wit inspect 4.1  260 error (2) 0 wit inspect .81   20    - wit inspect - wit inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   3800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .017 4.9
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   3800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900   3100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .032 4.9
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c timeout 0 wit inspect 900   3200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .025 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 370   4000 5400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 timeout 0 wit inspect 960     6600  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 1 wit inspect 86   3500 940 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 error (7) 0 wit inspect 900     5200  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 1 wit inspect 860   4800 12000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     6600  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 120   3100 1200 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 12    370 true 2 wit inspect 8.0   330  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 1 wit inspect 850   4300 11000 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 out of memory 0 wit inspect 600     7000  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 100   3500 930 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 12    440 true 2 wit inspect 8.7   340  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 1 wit inspect 400   3900 5500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 out of memory 0 wit inspect 470     7000  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c false(unreach-call) -16 wit inspect 97   3800 1100 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 12    450 true 2 wit inspect 7.9   360  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 1 wit inspect 480   4700 5500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 out of memory 0 wit inspect 490     7000  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 1 wit inspect 160   3900 1700 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1700 out of memory 0 wit inspect 820     7000  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 1 wit inspect 570   5000 6500 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 out of memory 0 wit inspect 430     7000  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900   4200 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 1 wit inspect 820   4900 9400 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 out of memory 0 wit inspect 560     7000  
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 -51 23000 280000 280000 42 -691 460 20000 42 -272 1300 21000 42 0 150 9000 42 -224 220   700 52 24 17000 73000 52 68 8700 97000
    correct results 42 67 3300 110000 36000 13 13 250 11000 16 16 150 5900 0 0 12 24 170 5100 34 68 1600 31000
        correct true 25 50 1900 68000 20000 0 0 0 0 12 24 170 5100 34 68 1600 31000
        correct false 17 17 1500 44000 16000 13 13 250 11000 16 16 150 5900 0 0 0 0
    correct-unconfimed results 29 10 5800 69000 70000 0 0 0 0 0 0
        correct-unconfirmed true 10 10 4800 43000 59000 0 0 0 0 0 0
        correct-unconfirmed false 19 0 980 26000 11000 0 0 0 0 0 0
    incorrect results 8 -128 440 15000 4200 22 -704 120 5900 9 -288 100 3700 0 7 -224 4.7 130 0 0
        incorrect true 0 22 -704 120 5900 9 -288 100 3700 0 7 -224 4.7 130 0 0
        incorrect false 8 -128 440 15000 4200 0 0 0 0 0 0
score (94 tasks, max score: 146) -51 -691 -272 0 -224 24 68
Run set interpchecker.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-ControlFlow