Tool PeSCo 1.7-svn b8d6131600+ CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 05:07:50 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 27 11   1300 260 .053 0     1 6.7  3.5  280 0   0   1 15     9.1   520   .62 0   0 5.7  3.1  280 0   0   -32 .88   .87   22    .32  0     - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 22 7.8 1600 210 .053 0     1 6.2  3.3  290 0   0   1 17     9.7   500   .62 0   0 5.0  2.8  270 0   0   -32 .77   .78   21    .21  0     - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 21 6.0 1200 180 .053 0     1 7.8  4.2  290 0   0   1 16     9.2   530   .66 0   0 5.6  3.1  280 0   0   -32 .89   .89   21    .26  0     - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 21 6.0 1400 170 .041 0     1 6.0  3.2  270 0   0   1 10     5.5   330   .62 0   0 5.7  3.1  270 0   0   -32 .73   .73   21    .17  0     - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 34 14   1900 360 0     0     - - - - 2 13   6.9 520 0   0   2 110   65   940 .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 23 7.5 1200 190 0     0     - - - - 0 520   500   7000 0   0   2 70   40   810 .62 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 21 6.0 1200 150 0     0     - - - - 2 8.9 4.7 370 0   0   2 78   43   710 .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 22 6.8 1100 210 0     0     - - - - 2 11   5.9 450 0   0   2 78   44   900 .62 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 17 4.7 1100 120 0     0     - - - - 2 6.2 3.4 260 0   0   2 27   14   520 .62 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 17 5.1 1100 130 0     0     - - - - 2 6.6 3.5 280 0   0   2 25   14   530 .66 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 18 5.3 1200 140 .066 0     1 7.0  3.7  290 0   0   1 11     5.8   350   .62 0   0 5.1  2.9  280 0   0   -32 .76   .76   22    .16  0     - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 17 5.0 1300 130 .066 0     1 6.5  3.5  290 0   0   1 10     5.7   340   .62 0   0 6.1  3.4  290 0   0   -32 .86   .85   22    .16  0     - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 1 18 5.2 1200 150 .066 0     1 7.4  3.9  300 0   0   1 11     5.8   350   .66 0   0 6.6  3.6  290 0   0   -32 .78   .78   22    .16  0     - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 17 5.1 1300 140 .066 0     1 7.5  4.0  290 0   0   1 10     5.6   340   .62 0   0 5.1  2.9  290 0   0   -32 .75   .74   22    .15  .037 - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 15 4.8 1300 110 .025 0     1 5.0  2.7  270 0   0   1 10     5.5   330   .66 0   0 5.0  2.9  270 0   0   -32 .73   .72   21    .17  0     - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 1 39 9.0 1800 300 .12  0     1 8.4  4.5  310 0   0   1 13     6.8   530   .66 0   0 5.9  3.3  300 0   0   -32 .80   .79   23    .17  0     - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 1 35 8.3 1700 260 .11  0     1 7.4  3.9  280 0   0   1 11     6.0   410   .62 0   0 6.0  3.2  300 0   0   -32 .82   .85   23    .18  0     - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 27 7.0 1600 220 .14  0     1 7.4  3.9  300 0   0   1 12     6.5   400   .66 0   0 5.9  3.3  290 0   0   -32 .77   .77   22    .17  0     - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 19 5.3 1500 140 .045 0     1 6.8  3.7  280 0   0   1 11     5.9   340   .62 0   0 4.8  2.7  260 0   0   1 .72   .72   21    .16  0     - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 18 5.4 1300 160 .078 0     1 7.5  4.0  290 0   0   1 10     6.0   360   .62 0   0 5.8  3.2  290 0   0   -32 .78   .79   22    .16  .045 - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 18 5.5 1200 160 .078 0     1 6.5  3.4  300 0   0   1 11     6.5   350   .66 0   0 5.5  3.0  290 0   0   -32 .73   .72   22    .16  0     - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 16 4.9 1400 120 .012 0     1 4.9  2.7  260 0   0   1 9.0   5.1   320   .62 0   0 4.6  2.7  250 0   0   -32 .70   .70   20    .15  .049 - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 19 5.3 1400 160 0     0     - - - - 2 14   8.0 560 0   0   2 42   23   750 .66 0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 16 4.8 1200 120 0     0     - - - - 2 14   8.0 560 0   0   2 39   21   1000 .62 0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 16 4.8 1300 120 0     0     - - - - 2 15   8.6 580 0   0   2 41   23   970 .66 0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 17 4.8 1100 130 0     0     - - - - 2 15   8.5 560 0   0   2 39   22   1000 .66 0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 2 19 5.6 1200 140 0     0     - - - - 0 910   890   5100 0   0   2 47   26   1000 .62 0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 15 4.1 1200 100 0     0     - - - - 2 9.9 5.3 360 0   0   2 11   6.0 340 .66 0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 12 3.6 1200 93 0     0     - - - - 2 6.9 3.8 290 0   0   2 9.6 5.4 310 .66 0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 2 17 5.1 1400 140 0     0     - - - - 0 910   890   4900 0   0   2 49   28   1100 .62 0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 2 18 5.4 1400 140 0     .090 - - - - 0 910   890   4800 0   0   2 47   26   1100 .62 0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 2 17 5.0 1200 140 0     0     - - - - 0 910   890   5200 0   0   2 49   27   840 .66 0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 2 25 8.2 1500 230 0     0     - - - - 0 900   890   5200 0   0   2 58   32   1500 .62 0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 2 19 5.5 1200 140 0     0     - - - - 0 910   890   4600 0   0   2 52   29   930 .66 0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 2 18 5.4 1400 150 0     0     - - - - 0 910   890   5100 0   0   2 49   27   1000 .66 0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 16 4.4 1200 100 .025 0     1 5.9  3.2  270 0   0   1 9.1   5.1   310   .66 0   0 4.2  2.4  260 0   0   -32 .66   .66   21    .090 0     - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 16 4.5 1200 110 .025 0     1 5.5  2.9  260 0   0   1 8.7   5.3   310   .62 0   0 4.1  2.4  250 0   0   -32 .68   .68   21    .10  0     - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 29 14   1700 280 0     0     - - - - 2 8.4 4.6 300 0   0   2 21   11   650 .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 66 43   2100 670 0     0     - - - - 2 7.0 3.9 300 0   0   2 29   16   970 .66 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 110 84   2100 1300 0     0     - - - - 2 7.2 3.9 300 0   0   2 31   18   2100 .62 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 110 83   2100 1100 0     0     - - - - 2 6.3 3.5 300 0   0   2 45   27   3700 .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 16 4.3 1200 120 0     0     - - - - 2 7.3 4.0 300 0   0   2 80   50   5800 .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 16 4.2 1200 120 0     0     - - - - 2 8.1 4.4 310 0   0   0 120   77   7000 .66 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 14 4.0 1100 90 0     0     - - - - 2 5.6 3.1 290 0   0   2 9.3 5.3 320 .66 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 12 3.9 1200 89 0     0     - - - - 2 6.8 3.8 290 0   0   2 12   6.5 360 .66 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 16 4.4 1200 120 0     0     - - - - 2 6.4 3.5 300 0   0   2 13   7.0 450 .66 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 19 5.0 1200 140 0     0     - - - - 2 6.1 3.4 290 0   0   2 15   8.5 470 .66 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 19 6.7 1400 150 0     0     - - - - 2 6.0 3.3 300 0   0   2 15   8.4 480 .66 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 130 88   2800 1400 .89  0     0 97    85    1400 0   0   0 96     81     2600   1.4  0   0 15    8.0  570 0   0   0 2.0    2.0    46    .37  0     - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 1 30 15   1300 290 .029 0     1 30    24    610 0   0   0 97     78     3100   .70 0   0 6.3  3.5  290 0   0   0 96      96      21    .63  0     - -
ntdrivers/floppy_false-unreach-call.i.cil.c 1 58 36   1500 530 .033 0     1 23    15    750 0   0   0 19     10     370   .71 0   0 8.0  4.4  290 0   0   0 96      96      22    .27  0     - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 1 24 7.5 1200 180 .053 0     1 10    5.5  340 0   0   -32 54     40     1400   .62 0   0 6.4  3.6  290 0   0   0 .91   .91   21    .16  0     - -
ntdrivers/parport_false-unreach-call.i.cil.c 1 71 52   1500 540 .029 0     1 11    5.8  330 0   0   0 97     79     3000   .95 0   0 7.7  4.2  320 0   0   0 1.4    1.4    25    .36  .34  - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 2 63 40   1700 570 0     0     - - - - 2 49   35   930 0   0   2 700   630   3100 .62 0  
ntdrivers/diskperf_true-unreach-call.i.cil.c 2 29 12   1300 270 0     0     - - - - 0 12   6.3 510 0   0   2 420   350   3900 .62 0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 2 560 520   2600 4300 .20  0     - - - - 0 910   870   5600 0   0   2 330   250   3600 .62 0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 1 56 36   1400 600 0     0     - - - - 0 900   880   3200 0   0   0 18   10   370 .75 0  
ntdrivers/parport_true-unreach-call.i.cil.c 1 91 64   1900 790 0     0     - - - - 0 18   9.3 560 0   0   0 960   870   3300 1.5  0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 1 53 14   1500 420 .10  0     1 8.0  4.3  320 0   0   0 13     7.4   300   .71 0   0 6.3  3.5  300 0   0   0 .86   .85   23    .31  0     - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 52 12   1900 340 .086 0     1 8.6  4.6  310 0   0   0 13     8.0   290   .75 0   0 6.2  3.4  290 0   0   0 .82   .82   22    .30  0     - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 47 12   1500 380 .066 0     1 8.9  4.7  300 0   0   0 12     7.2   290   .68 0   0 7.0  3.9  290 0   0   0 .81   .83   22    .29  0     - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 47 12   1500 390 .070 0     1 7.8  4.1  300 0   0   0 12     7.7   290   .75 0   0 5.8  3.2  290 0   0   0 .80   .81   22    .29  0     - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 1 35 8.3 1300 260 .078 0     1 7.5  4.0  310 0   0   0 13     7.8   300   .71 0   0 6.0  3.3  290 0   0   -32 .86   .85   22    .32  0     - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 1 31 7.5 1300 220 .090 0     1 7.6  4.0  310 0   0   0 14     8.0   290   .75 0   0 5.6  3.1  270 0   0   -32 .85   .85   22    .32  0     - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 1 32 7.8 1300 210 .090 0     1 7.8  4.2  310 0   0   0 13     7.5   290   .75 0   0 5.8  3.1  290 0   0   -32 .84   .86   22    .32  0     - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 1 39 9.2 1400 270 .090 0     1 7.1  3.8  280 0   0   0 14     8.0   290   .71 0   0 5.9  3.2  290 0   0   -32 .84   .84   22    .32  0     - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 1 51 13   1500 370 .12  0     1 8.0  4.3  320 0   0   0 13     7.6   290   .68 0   0 7.0  3.8  300 0   0   -32 .90   .90   23    .32  0     - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 1 53 14   1600 430 .13  0     1 9.6  5.1  310 0   0   0 14     8.0   300   .71 0   0 6.4  3.6  280 0   0   -32 .86   .86   23    .32  0     - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 1 120 45   1900 1100 .19  0     1 9.5  5.1  330 0   0   0 13     8.0   290   .75 0   0 6.9  3.7  310 0   0   -32 .92   .92   25    .32  0     - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 1 51 13   1500 390 .14  0     1 9.7  5.1  320 0   0   0 14     8.0   300   .71 0   0 7.4  4.1  300 0   0   -32 .90   .90   23    .32  0     - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 1 120 45   1800 1200 .20  0     1 13    6.6  330 0   0   0 15     8.6   300   .75 0   0 7.5  4.1  310 0   0   -32 .96   .96   25    .32  0     - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 960 900   2700 12000 0     0     0 .61 .38 41 0   0   0 .021 .021 5.6 0    0   0 .92 .60 47 0   0   0 .0042 .0047 .40 0     0     - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 1 50 13   1500 380 .14  0     1 8.0  4.3  290 0   0   0 13     7.6   300   .75 0   0 6.6  3.6  300 0   0   -32 .91   .92   23    .32  0     - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 1 51 13   1500 370 .13  0     1 8.6  4.6  320 0   0   0 13     7.6   300   .71 0   0 6.5  3.5  300 0   0   -32 .86   .86   23    .32  0     - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 1 55 14   1500 410 .14  0     1 8.4  4.4  290 0   0   0 13     7.9   300   .75 0   0 5.8  3.3  270 0   0   -32 .89   .89   23    .32  0     - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 1 180 71   2400 1600 .20  0     1 11    5.7  330 0   0   0 15     8.4   300   .75 0   0 6.9  3.8  310 0   0   -32 .91   .90   25    .32  0     - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 1 49 12   1500 360 .14  0     1 9.1  4.9  320 0   0   0 14     8.0   290   .75 0   0 6.5  3.6  300 0   0   -32 .87   .87   23    .32  0     - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 1 37 8.7 1300 260 0     0     - - - - 0 13   6.9 440 0   0   0 15   8.4 300 .75 0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 1 35 8.4 1400 230 0     0     - - - - 0 10   5.5 440 0   0   0 13   7.5 300 .75 0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 1 39 9.3 1400 280 0     0     - - - - 0 12   6.4 440 0   0   0 14   7.9 300 .75 0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 1 38 9.1 1400 280 0     0     - - - - 0 14   7.2 450 0   0   0 15   8.6 290 .75 0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 2 44 11   1500 330 0     0     - - - - 2 740   720   1600 0   0   0 13   7.8 290 .75 0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 1 30 7.4 1300 220 0     0     - - - - 0 250   230   1100 0   0   0 14   8.2 290 .75 0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 1 95 34   1900 860 0     0     - - - - 0 900   890   1800 0   0   0 14   8.2 300 .68 0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 1 93 33   1800 910 0     0     - - - - 0 900   890   1700 0   0   0 15   8.6 300 .75 0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 2 48 12   1900 350 0     0     - - - - 2 790   780   1700 0   0   0 13   7.8 290 .75 0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 1 97 35   1800 840 0     0     - - - - 0 900   890   1800 0   0   0 14   8.3 290 .75 0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 2 61 19   1600 500 0     0     - - - - 2 630   610   1600 0   0   0 17   9.1 290 .75 0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 1 85 29   1800 740 0     0     - - - - 0 900   890   1800 0   0   0 17   9.4 300 .75 0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 1 170 71   2000 1600 0     0     - - - - 0 900   890   2300 0   0   0 16   8.9 300 .71 0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 1 49 12   1500 350 0     0     - - - - 0 900   890   1700 0   0   0 15   8.8 290 .75 0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 1 99 35   1800 820 0     0     - - - - 0 900   890   1800 0   0   0 14   8.0 300 .75 0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 2 49 13   2100 370 0     0     - - - - 2 560   550   1500 0   0   0 14   8.0 300 .75 0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 1 110 37   2400 930 0     0     - - - - 0 900   890   1700 0   0   0 13   7.7 300 .75 0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 94 129 5500 3000 140000 50000 4.6  .090 42 40 450 280 14000 0   0   42 -14 810 540 23000 29    0   42 0 260 140 12000 0   0   42 -991 230    230    940 11    .47 52 54 19000 19000 85000 0   0   52 64 4000 3000 58000 36 0  
    correct results 77 114 3300 1500 110000 27000 3.7  .090 40 40 350 200 13000 0   0   18 18 200 120 6900 11    0   0 1 1 .72 .72 21 .16 0    27 54 3000 2800 15000 0   0   32 64 2600 1900 42000 20 0  
        correct true 37 74 1600 990 53000 14000 .20 .090 0 0 0 0 27 54 3000 2800 15000 0   0   32 64 2600 1900 42000 20 0  
        correct false 40 40 1700 560 58000 14000 3.5  0     40 40 350 200 13000 0   0   18 18 200 120 6900 11    0   0 1 1 .72 .72 21 .16 0    0 0
    correct-unconfimed results 16 15 1200 520 28000 11000 .89 0     0 0 0 0 0 0
        correct-unconfirmed true 15 15 1100 430 25000 9700 0    0     0 0 0 0 0 0
        correct-unconfirmed false 1 0 130 88 2800 1400 .89 0     0 0 0 0 0 0
    incorrect results 0 0 1 -32 54 40 1400 .62 0   0 31 -992 25    25    690 7.4  .13 0 0
        incorrect true 0 0 1 -32 54 40 1400 .62 0   0 31 -992 25    25    690 7.4  .13 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 129 40 -14 0 -991 54 64
Run set pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow