Tool 2LS 0.7.2-sv-comp19 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*
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-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 06:59:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml -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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 1.4   1.3   370 17    0      0    -32 11    5.9  420 0   0   1 14     8.1   450   .62 0   0 6.4  3.4  290 0   0   1 .88   .88   21    .33  0      - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .36  .35  62 4.0  0      0    -32 6.4  3.5  280 0   0   1 15     8.8   480   .66 0   0 5.3  2.9  280 0   0   -32 .76   .76   21    .21  .033  - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .53  .52  120 5.4  0      0    -32 7.7  4.1  280 0   0   1 19     11     530   .62 0   0 5.6  3.1  290 0   0   -32 .81   .81   21    .27  .049  - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .26  .25  40 3.9  0      0    -32 6.9  3.7  280 0   0   1 11     6.1   330   .62 0   0 5.1  2.9  270 0   0   1 .73   .73   21    .18  0      - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 1.4   1.4   410 18    0      0    - - - - 2 13    6.8  480 0   0   2 110     65     1100   .62 0  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .52  .51  110 5.0  0      0    - - - - 0 570    540    7000 0   0   2 64     37     870   .62 0  
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .34  .34  70 3.6  0      0    - - - - 2 11    5.8  390 0   0   2 79     44     830   .62 0  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .57  .56  140 6.2  0      0    - - - - 2 13    6.7  480 0   0   2 88     49     760   .62 0  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .19  .19  27 1.5  0      0    - - - - 2 5.3  2.9  280 0   0   2 20     11     520   .62 0  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 .25  .24  46 2.4  0      0    - - - - 2 7.3  4.0  270 0   0   2 22     12     540   .62 0  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 0 10     10     180 83    0      0    -32 7.6  4.0  280 0   0   -32 9.2   5.4   320   .66 0   0 5.1  2.8  270 0   0   -32 .73   .73   21    .15  0      - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 0 9.9   9.9   190 94    0      0    -32 5.9  3.2  270 0   0   -32 9.2   5.5   320   .62 0   0 4.9  2.7  270 0   0   -32 .72   .72   21    .15  0      - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 0 38     38     260 250    0      0    -32 5.6  3.0  270 0   0   -32 9.3   5.6   330   .62 0   0 4.6  2.6  260 0   0   0 .73   .72   21    .074 0      - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 0 10     10     190 78    0      0    -32 7.1  3.8  280 0   0   -32 8.9   5.4   320   .62 0   0 4.9  2.8  260 0   0   -32 .74   .74   21    .16  0      - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 .27  .26  41 3.4  0      0    -32 6.5  3.5  270 0   0   -32 8.3   4.8   310   .62 0   0 4.7  2.6  270 0   0   1 .74   .74   21    .17  0      - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 19     19     240 140    0      0    -32 9.3  4.9  290 0   0   -32 10     5.7   370   .62 0   0 5.6  3.0  280 0   0   -32 .80   .80   22    .18  0      - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 19     19     240 150    0      0    -32 9.2  4.8  290 0   0   -32 10     5.7   350   .62 0   0 5.4  3.0  280 0   0   -32 .78   .78   22    .19  0      - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 0 21     21     180 170    0      0    -32 7.7  4.1  280 0   0   -32 9.4   5.6   330   .62 0   0 5.4  2.9  270 0   0   -32 .73   .73   21    .17  0      - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 5.7   5.6   93 47    0      0    -32 8.2  4.3  270 0   0   -32 9.2   5.2   320   .62 0   0 5.2  2.9  270 0   0   1 .72   .71   21    .16  0      - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 0 22     22     190 160    0      0    -32 7.4  3.9  280 0   0   -32 9.4   5.2   320   .62 0   0 5.0  2.8  280 0   0   -32 .72   .72   21    .16  0      - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 0 10     10     160 110    0      0    -32 7.0  3.7  280 0   0   -32 9.4   5.2   320   .62 0   0 4.9  2.7  260 0   0   -32 .73   .74   21    .16  .045  - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 .28  .27  40 2.6  0      0    -32 6.6  3.6  270 0   0   -32 8.8   4.9   310   .66 0   0 4.6  2.6  270 0   0   1 .72   .71   21    .15  0      - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 10     10     250 95    0      0    - - - - 2 18    10    550 0   0   2 35     19     870   .31 0  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 12     12     260 99    0      0    - - - - 2 19    10    560 0   0   2 38     21     890   .62 0  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 39     39     360 300    0      0    - - - - 2 19    11    580 0   0   2 38     21     980   .62 0  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 11     11     260 110    0      .13 - - - - 2 19    10    560 0   0   2 36     20     890   .62 0  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 900     900     7800 9300    .016  0    - - - - 0 .84 .50 41 0   0   0 .024 .025 5.5 0    0  
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 2 .71  .71  37 10    0      0    - - - - 2 8.3  4.5  340 0   0   2 11     6.3   360   .66 0  
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 2 .40  .40  24 4.5  0      0    - - - - 2 5.3  2.9  290 0   0   2 10     5.8   310   .66 0  
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 900     900     7700 10000    .016  0    - - - - 0 .68 .44 40 0   0   0 .021 .022 5.6 0    0  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 900     900     7800 11000    .012  0    - - - - 0 .73 .46 41 0   0   0 .038 .046 5.5 0    0  
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 900     900     7700 10000    .016  0    - - - - 0 .64 .40 41 0   0   0 .022 .025 5.6 0    0  
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 900     900     7700 11000    .012  0    - - - - 0 .78 .48 41 0   0   0 .025 .027 5.7 0    0  
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 900     900     7700 9300    .016  0    - - - - 0 .73 .45 41 0   0   0 .020 .021 5.6 0    0  
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 900     900     7700 9700    .016  0    - - - - 0 .70 .43 40 0   0   0 .023 .023 5.6 0    0  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 .15  .14  25 1.1  0      0    -32 5.5  3.0  250 0   0   -32 7.6   4.7   310   .62 0   0 4.5  2.5  250 0   0   1 .66   .65   21    .090 0      - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 .14  .14  25 1.3  0      0    -32 4.9  2.7  260 0   0   -32 7.8   4.9   310   .62 0   0 4.8  2.7  260 0   0   1 .73   .73   21    .098 .0082 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12  .11  24 1.2  0      0    - - - - 2 5.7  3.1  300 0   0   2 20     11     650   .66 0  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12  .11  25 1.0  0      0    - - - - 2 6.0  3.2  290 0   0   2 24     13     860   .62 0  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  24 1.4  0      0    - - - - 2 7.0  3.8  290 0   0   2 30     17     2100   .62 0  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 .12  .12  24 1.2  0      0    - - - - 2 6.1  3.4  300 0   0   2 39     24     3300   .62 0  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13  .13  25 1.2  0      0    - - - - 2 6.7  3.7  300 0   0   2 92     55     6600   .62 0  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13  .12  25 1.3  0      0    - - - - 2 8.0  4.3  300 0   0   0 110     73     7000   .65 0  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 .099 .097 24 .89 0      0    - - - - 2 5.3  2.9  290 0   0   2 10     5.8   330   .62 0  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  24 .99 0      0    - - - - 2 5.1  2.8  290 0   0   2 11     6.1   370   .62 0  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  24 1.1  0      0    - - - - 2 6.5  3.6  290 0   0   2 13     7.1   440   .23 0  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 .11  .11  24 1.1  0      0    - - - - 2 6.1  3.4  290 0   0   2 14     8.2   470   .25 0  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 .13  .12  25 .84 0      0    - - - - 2 5.5  3.0  290 0   0   2 16     8.9   500   .62 0  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 .69  .69  67 6.4  .0082 0    0 .73 .44 42 0   0   0 .022 .023 5.6 0    0   0 .99 .64 47 0   0   0 .0051 .0064 .53 0     0      - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 1.1   1.1   47 11    .0082 0    0 .65 .40 41 0   0   0 .021 .022 5.7 0    0   0 .98 .64 47 0   0   0 .0056 .0071 .53 0     0      - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 1.4   1.4   61 12    .0082 0    0 .77 .48 41 0   0   0 .022 .023 5.6 0    0   0 .97 .64 48 0   0   0 .0048 .0059 .52 0     0      - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 .31  .31  38 2.9  .0082 0    0 .61 .38 41 0   0   0 .021 .022 5.6 0    0   0 .92 .61 47 0   0   0 .0046 .0058 .53 0     0      - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 15     15     220 150    .0082 0    0 .74 .46 40 0   0   0 .021 .022 5.6 0    0   0 .94 .61 47 0   0   0 .0051 .0080 .46 0     0      - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 .67  .67  68 5.6  .0082 0    - - - - 0 .68 .42 40 0   0   0 .026 .027 5.6 0    0  
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 1.3   1.3   49 14    .0082 0    - - - - 0 .78 .47 41 0   0   0 .021 .022 5.6 0    0  
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 8.7   8.7   690 88    .0082 0    - - - - 0 .75 .46 41 0   0   0 .020 .027 5.6 0    0  
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 1.4   1.4   61 13    .0082 0    - - - - 0 .60 .36 41 0   0   0 .025 .026 5.6 0    0  
ntdrivers/parport_true-unreach-call.i.cil.c 0 16     16     230 170    .0082 0    - - - - 0 .67 .45 41 0   0   0 .021 .022 5.6 0    0  
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 440     440     1800 2700    .0082 0    -32 9.1  4.8  290 0   0   0 12     7.3   290   .71 0   0 5.2  2.9  270 0   0   0 .65   .65   21    .066 0      - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 350     350     1600 1800    .0082 0    -32 9.6  5.0  300 0   0   0 13     7.2   290   .71 0   0 4.9  2.7  270 0   0   0 .68   .68   21    .066 0      - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 380     380     1600 1700    .0082 0    -32 7.7  4.1  290 0   0   0 13     7.9   290   .68 0   0 4.8  2.7  260 0   0   0 .67   .67   21    .066 0      - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 370     370     1600 2100    .0082 0    -32 9.1  4.8  300 0   0   0 12     7.4   290   .71 0   0 4.9  2.7  270 0   0   0 .68   .68   21    .066 0      - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 900     900     1500 3800    .020  0    0 .70 .43 40 0   0   0 .044 .047 5.5 0    0   0 .95 .62 46 0   0   0 .0035 .0044 .54 0     0      - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 900     900     1500 5500    .020  0    0 .72 .43 41 0   0   0 .022 .023 5.6 0    0   0 .94 .60 47 0   0   0 .0021 .0028 .52 0     0      - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 900     900     1500 4400    .020  0    0 .79 .51 42 0   0   0 .021 .022 5.6 0    0   0 .96 .63 48 0   0   0 .0043 .0051 .40 0     0      - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 900     900     1400 4200    .020  0    0 .79 .47 42 0   0   0 .022 .024 5.6 0    0   0 .93 .61 47 0   0   0 .0037 .0048 .53 0     0      - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 900     900     1500 4900    .020  0    0 .68 .42 40 0   0   0 .023 .024 5.6 0    0   0 .98 .64 47 0   0   0 .0047 .0057 .52 0     0      - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 900     900     1500 4800    .020  0    0 .74 .47 40 0   0   0 .021 .022 5.6 0    0   0 .99 .64 49 0   0   0 .0054 .0068 .53 0     0      - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 900     900     1400 5000    .020  0    0 .79 .50 41 0   0   0 .026 .028 5.7 0    0   0 .93 .62 47 0   0   0 .0021 .0026 .40 0     0      - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 900     900     1500 4900    .020  0    0 .77 .47 41 0   0   0 .021 .031 5.6 0    0   0 .98 .64 47 0   0   0 .0057 .0068 .52 0     0      - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 900     900     1500 6200    .020  0    0 .76 .45 40 0   0   0 .021 .023 5.6 0    0   0 .98 .65 48 0   0   0 .0056 .0074 .53 0     0      - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 900     900     1400 4700    .020  0    0 .75 .47 42 0   0   0 .021 .022 5.6 0    0   0 .96 .63 47 0   0   0 .0063 .0081 .53 0     0      - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 900     900     1500 4900    .020  0    0 .82 .49 42 0   0   0 .021 .022 5.6 0    0   0 .98 .65 47 0   0   0 .0021 .0027 .53 0     0      - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 900     900     1500 7600    .020  0    0 .78 .48 42 0   0   0 .022 .024 5.6 0    0   0 .93 .61 46 0   0   0 .0051 .0062 .53 0     0      - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 900     900     1400 5200    .020  0    0 .68 .42 41 0   0   0 .022 .024 5.8 0    0   0 .94 .61 47 0   0   0 .0019 .0024 .52 0     0      - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900     900     1500 7300    .020  0    0 .60 .38 41 0   0   0 .022 .024 5.6 0    0   0 .94 .63 47 0   0   0 .0063 .0079 .53 0     0      - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 900     900     1500 3900    .020  0    0 .61 .38 41 0   0   0 .022 .022 5.6 0    0   0 .96 .63 47 0   0   0 .0020 .0026 .53 0     0      - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 1 360     360     2300 3000    .0082 0    - - - - 0 900    890    1700 0   0   0 14     7.6   300   .71 0  
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 1 350     350     2200 2900    .0082 0    - - - - 0 900    890    1700 0   0   0 14     8.2   300   .71 0  
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 1 390     390     2200 2200    .0082 0    - - - - 0 900    890    1500 0   0   0 13     7.3   290   .66 0  
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 1 330     330     2200 1700    .0082 0    - - - - 0 900    890    1600 0   0   0 13     7.2   290   .71 0  
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900     900     1500 6000    .020  0    - - - - 0 .73 .44 40 0   0   0 .022 .022 5.6 0    0  
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900     900     1500 5800    .020  0    - - - - 0 .75 .48 42 0   0   0 .022 .023 5.6 0    0  
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900     900     1500 5900    .020  0    - - - - 0 .62 .40 41 0   0   0 .022 .025 5.7 0    0  
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900     900     1500 4400    .020  0    - - - - 0 .59 .36 41 0   0   0 .025 .026 5.6 0    0  
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900     900     1500 4400    .020  0    - - - - 0 .74 .45 40 0   0   0 .022 .023 5.7 0    0  
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900     900     1500 5100    .020  0    - - - - 0 .71 .43 41 0   0   0 .045 .046 5.6 0    0  
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900     900     1500 4600    .020  0    - - - - 0 .72 .43 41 0   0   0 .026 .028 5.7 0    0  
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900     900     1400 4100    .020  0    - - - - 0 .71 .44 41 0   0   0 .021 .023 5.6 0    0  
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900     900     1500 3800    .020  0    - - - - 0 .79 .47 42 0   0   0 .026 .026 5.6 0    0  
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900     900     3800 8200    .025  0    - - - - 0 .60 .37 40 0   0   0 .021 .022 5.6 0    0  
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900     900     1500 7100    .020  0    - - - - 0 .72 .43 40 0   0   0 .021 .022 5.7 0    0  
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900     900     1500 4700    .020  0    - - - - 0 .59 .37 40 0   0   0 .021 .022 5.6 0    0  
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900     900     1500 4400    .020  0    - - - - 0 .77 .47 42 0   0   0 .022 .024 5.6 0    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 59 35000   35000   120000 240000 .83  .13 42 -704 180 97 7100 0   0   42 -444 240 140 7600 14   0   42 0 130 74 6900 0   0   42 -313 16   16   470 3.3 .14   52 44 4400 4200 23000 0   0   52 44 990 570 33000 16 0  
    correct results 32 55 87   87   3100 750 0     .13 0 4 4 59 34 1800 2.5 0   0 7 7 5.2 5.2 150 1.2 .0082 22 44 200 110 8000 0   0   22 44 820 470 24000 13 0  
        correct true 23 46 78   78   2300 670 0     .13 0 0 0 0 22 44 200 110 8000 0   0   22 44 820 470 24000 13 0  
        correct false 9 9 9.0 8.9 820 86 0     0    0 4 4 59 34 1800 2.5 0   0 7 7 5.2 5.2 150 1.2 .0082 0 0
    correct-unconfimed results 17 4 3100   3100   17000 19000 .066 0    0 0 0 0 0 0
        correct-unconfirmed true 4 4 1400   1400   8900 9900 .033 0    0 0 0 0 0 0
        correct-unconfirmed false 13 0 1700   1700   8300 9600 .033 0    0 0 0 0 0 0
    incorrect results 0 22 -704 170 88 6300 0   0   14 -448 130 74 4600 8.8 0   0 10 -320 7.5 7.5 210 1.8 .13   0 0
        incorrect true 0 22 -704 170 88 6300 0   0   14 -448 130 74 4600 8.8 0   0 10 -320 7.5 7.5 210 1.8 .13   0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 59 -704 -444 0 -313 44 44
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow