Tool VeriAbs 1.3.10 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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow
Options -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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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 false(unreach-call) 1 wit inspect 280 250   460 3000 .88 .0041 false(unreach-call) 1 wit inspect 7.7  4.1  290 0   0      false(unreach-call) 1 --- inspect 13     7.7   450   .66 0     false(unreach-call) 1 --- inspect 5.3  2.9  280 0      0     true -32 --- inspect .87   .87   21    .32  0     - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 270 250   360 2900 .62 0      false(unreach-call) 1 wit inspect 5.8  3.1  270 0   0      false(unreach-call) 1 --- inspect 21     12     470   .66 0     false(unreach-call) 1 --- inspect 5.0  2.7  280 0      0     true -32 --- inspect .77   .76   22    .21  0     - --- inspect - --- inspect
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 270 250   400 3000 .74 0      false(unreach-call) 1 wit inspect 7.7  4.1  270 0   0      false(unreach-call) 1 --- inspect 18     10     540   .66 0     false(unreach-call) 1 --- inspect 5.5  3.0  280 0      0     true -32 --- inspect .83   .83   22    .27  0     - --- inspect - --- inspect
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 260 250   330 3100 .54 0      false(unreach-call) 1 wit inspect 6.7  3.5  280 0   0      false(unreach-call) 1 --- inspect 11     5.9   340   .66 0     false(unreach-call) 1 --- inspect 4.9  2.7  270 0      0     false(unreach-call) 1 --- inspect .74   .74   21    .18  0     - --- inspect - --- inspect
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 380 290   1800 3700 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 10    5.4  520 0   0      true 2 --- inspect 120     70     960   .62 0     
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 --- inspect 900 880   700 9100 .89 .30   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 360 280   1600 4300 170    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.5  5.0  420 0   0      true 2 --- inspect 190     130     1300   .62 0     
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 360 290   1600 3500 150    6.1    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 11    5.9  380 0   0      true 2 --- inspect 180     130     1400   .62 .049 
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 280 250   680 3200 140    .27   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.8  270 0   0      true 2 --- inspect 25     14     480   .66 0     
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 280 250   780 3000 170    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.2  3.9  280 0   0      true 2 --- inspect 21     12     510   .66 0     
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 47 30   370 560 .50 0      false(unreach-call) 1 wit inspect 6.9  3.7  290 0   0      false(unreach-call) 1 --- inspect 12     6.6   400   .66 0     false(unreach-call) 1 --- inspect 6.6  3.6  280 0      0     true -32 --- inspect .72   .72   22    .15  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 48 31   380 510 .50 0      false(unreach-call) 1 wit inspect 6.6  3.5  290 0   0      false(unreach-call) 1 --- inspect 11     5.8   350   .66 0     false(unreach-call) 1 --- inspect 6.0  3.3  280 0      0     true -32 --- inspect .75   .74   22    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 51 33   430 590 .48 0      false(unreach-call) 1 wit inspect 6.4  3.3  290 0   0      false(unreach-call) 1 --- inspect 10     5.9   370   .66 0     unknown 0 --- inspect 6.2  3.4  280 0      0     true -32 --- inspect .75   .75   22    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 47 30   380 500 .46 .0082 false(unreach-call) 1 wit inspect 7.7  4.0  290 0   0      false(unreach-call) 1 --- inspect 11     6.1   400   .66 0     unknown 0 --- inspect 4.8  2.7  270 0      0     true -32 --- inspect .72   .72   22    .15  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 57 41   430 670 .49 0      false(unreach-call) 1 wit inspect 6.2  3.3  270 0   0      false(unreach-call) 1 --- inspect 12     6.9   330   .66 0     unknown 0 --- inspect 5.7  3.2  270 0      0     false(unreach-call) 1 --- inspect .74   .74   21    .17  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 320 300   600 4500 .59 0      true -32 wit inspect 9.1  4.8  290 0   0      false(unreach-call) 1 --- inspect 14     7.5   550   .66 0     unknown 0 --- inspect 5.3  2.9  280 0      0     false(unreach-call) 1 --- inspect .76   .75   24    .18  .045 - --- inspect - --- inspect
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 180 160   530 2400 .51 0      false(unreach-call) 1 wit inspect 6.1  3.2  290 0   0      false(unreach-call) 1 --- inspect 11     6.5   460   .66 .053 unknown 0 --- inspect 5.1  2.9  280 0      0     true -32 --- inspect .79   .80   22    .18  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 73 54   520 800 .48 .27   false(unreach-call) 1 wit inspect 7.7  4.1  290 0   0      false(unreach-call) 1 --- inspect 10     6.0   390   .66 0     unknown 0 --- inspect 5.3  2.9  280 0      .13  true -32 --- inspect .74   .74   22    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 69 51   480 900 .50 0      false(unreach-call) 1 wit inspect 6.9  3.7  280 0   0      false(unreach-call) 1 --- inspect 11     5.9   340   .62 0     false(unreach-call) 1 --- inspect 4.6  2.6  260 0      0     true -32 --- inspect .73   .73   21    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 64 47   500 690 .49 0      false(unreach-call) 1 wit inspect 6.0  3.2  290 0   0      false(unreach-call) 1 --- inspect 12     6.3   380   .66 .045 unknown 0 --- inspect 5.2  2.9  270 0      0     false(unreach-call) 1 --- inspect .72   .72   22    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 65 48   470 660 .49 0      false(unreach-call) 1 wit inspect 7.4  4.0  290 0   0      false(unreach-call) 1 --- inspect 11     6.0   420   .66 0     unknown 0 --- inspect 5.4  3.0  270 0      0     false(unreach-call) 1 --- inspect .72   .71   22    .16  0     - --- inspect - --- inspect
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 68 52   470 650 .51 0      false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0      false(unreach-call) 1 --- inspect 9.4   5.7   320   .62 0     false(unreach-call) 1 --- inspect 4.4  2.5  260 0      0     false(unreach-call) 1 --- inspect .70   .71   21    .15  .049 - --- inspect - --- inspect
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c true 2 wit inspect 95 60   1300 960 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    8.7  550 0   0      true 2 --- inspect 36     19     770   .66 0     
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 100 62   1600 1100 150    39      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.6  550 0   0      true 2 --- inspect 38     21     840   .62 0     
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c true 2 wit inspect 110 66   1400 1200 200    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 14    8.3  570 0   .0041 true 2 --- inspect 38     21     910   .62 0     
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c true 2 wit inspect 99 61   1400 1100 150    .037  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 17    9.6  550 0   0      true 2 --- inspect 36     20     1000   .62 0     
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   710 8500 .57 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 39 0   0      error (2) 0 --- inspect .023 .023 5.6 0    0     
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 270 250   490 2500 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.8  5.3  350 0   0      true 2 --- inspect 19     11     480   .66 0     
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 24 9.9 470 180 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.9  3.3  290 0   0      true 2 --- inspect 11     6.2   400   .66 0     
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   690 11000 .45 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   700 8700 .50 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   700 10000 .45 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   680 7100 .61 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   710 6900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c timeout 0 --- inspect 900 880   720 8600 .51 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .86 .53 42 0   0      error (2) 0 --- inspect .022 .022 5.7 0    0     
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 20 9.1 280 160 .41 0      false(unreach-call) 1 wit inspect 4.8  2.7  260 0   .0082 false(unreach-call) 1 --- inspect 8.7   4.9   310   .66 0     false(unreach-call) 1 --- inspect 4.0  2.3  260 0      0     false(unreach-call) 1 --- inspect .67   .67   21    .090 0     - --- inspect - --- inspect
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 21 9.8 280 180 .43 .45   false(unreach-call) 1 wit inspect 5.0  2.7  270 0   0      false(unreach-call) 1 --- inspect 8.4   4.7   310   .66 0     false(unreach-call) 1 --- inspect 5.5  3.1  260 0      0     false(unreach-call) 1 --- inspect .67   .67   21    .098 0     - --- inspect - --- inspect
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 28 11   910 240 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.0  3.8  300 0   0      true 2 --- inspect 20     11     630   .66 0     
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 34 15   1700 320 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.3  310 0   0      true 2 --- inspect 24     13     940   .66 0     
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 44 22   2400 390 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.1  3.3  300 0   0      true 2 --- inspect 31     17     2100   .62 0     
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 63 35   5000 570 150    .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.3  3.4  310 0   0      true 2 --- inspect 47     28     3900   .62 0     
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 79 39   5300 690 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 6.3  3.5  300 0   0      true 2 --- inspect 81     51     5800   .62 0     
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 85 40   5600 680 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.0  4.3  310 0   0      out of memory 0 --- inspect 120     74     7000   .64 0     
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 16 7.6 450 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  280 0   0      true 2 --- inspect 10     5.8   320   .66 0     
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 17 7.8 510 140 200    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  290 0   0      true 2 --- inspect 12     6.9   370   .66 0     
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 18 8.1 630 180 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.8  290 0   0      true 2 --- inspect 13     6.9   450   .66 .0041
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 21 8.8 710 180 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.0  290 0   0      true 2 --- inspect 14     8.3   530   .66 0     
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 24 10   760 210 140    39      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.4  4.0  300 0   .0041 true 2 --- inspect 15     8.9   530   .62 0     
ntdrivers/cdaudio_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 520 470   6700 6100 56    .049  error (invalid witness file) 0 --- inspect 86    55    4100 0   .34   timeout 0 --- inspect 97     79     2300   .73 0     timeout 0 --- inspect 11    130    450 .053  0     error (1) 0 --- inspect 1.6    1.6    100    .34  0     - --- inspect - --- inspect
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 130 80   850 1300 1.7  0      unknown 0 wit inspect 8.7  4.5  310 0   0      true -32 --- inspect 82     61     2400   .62 .16  unknown 0 --- inspect 6.6  3.6  290 0      0     timeout 0 --- inspect 96      96      21    .17  0     - --- inspect - --- inspect
ntdrivers/floppy_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 95 50   910 990 2.5  0      false(unreach-call) 1 wit inspect 21    15    690 0   0      error (7) 0 --- inspect 22     12     370   .75 0     unknown 0 --- inspect 7.4  4.1  300 0      0     timeout 0 --- inspect 96      96      22    .28  0     - --- inspect - --- inspect
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 51 29   430 470 1.1  .19   false(unreach-call) 1 wit inspect 11    6.2  340 0   0      true -32 --- inspect 55     41     1500   .62 0     unknown 0 --- inspect 6.2  3.5  290 0      0     error (2) 0 --- inspect .92   .92   22    .16  0     - --- inspect - --- inspect
ntdrivers/parport_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 830 760   1300 8200 4.1  0      exception 0 --- inspect 6.5  3.4  280 0   0      timeout 0 --- inspect 97     79     3300   .85 0     exception 0 --- inspect 8.6  4.6  300 0      0     error (1) 0 --- inspect 1.3    1.3    25    .32  .34  - --- inspect - --- inspect
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 170 66   2000 1700 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 53    37    960 0   0      true 2 --- inspect 680     630     2600   .62 0     
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 0 --- inspect 900 840   9500 11000 1.9  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c unknown 0 --- inspect 220 140   1300 2300 17    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 --- inspect 900 860   1000 8400 3.4  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 42 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 --- inspect 900 830   1400 10000 4.2  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 80 56   630 810 .65 7.5    true -32 wit inspect 8.1  4.3  290 0   0      error (7) 0 --- inspect 13     7.6   290   .75 0     unknown 0 --- inspect 7.1  3.9  280 0      0     error (2) 0 --- inspect .79   .79   22    .29  0     - --- inspect - --- inspect
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 2000 .16 0      error (invalid witness file) 0 --- inspect .74 .46 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .64 48 0      0     error (invalid witness file) 0 --- inspect .0049 .0060 .53 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 1800 .16 0      error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .93 .59 47 0      0     error (invalid witness file) 0 --- inspect .0014 .0016 .39 0     0     - --- inspect - --- inspect
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 1800 .16 0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     error (invalid witness file) 0 --- inspect .93 .61 48 0      0     error (invalid witness file) 0 --- inspect .0046 .0056 .53 0     0     - --- inspect - --- inspect
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 320 300   8400 4200 .67 .0041 true -32 wit inspect 8.2  4.3  290 0   0      error (7) 0 --- inspect 16     9.0   290   .75 0     unknown 0 --- inspect 5.4  3.0  300 0      0     true -32 --- inspect .80   .80   22    .31  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 320 300   8100 3600 .68 0      true -32 wit inspect 7.5  4.0  290 0   0      error (7) 0 --- inspect 15     8.6   290   .75 0     unknown 0 --- inspect 5.4  3.0  280 0      0     true -32 --- inspect .80   .80   22    .31  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 330 300   7500 3600 .68 0      true -32 wit inspect 7.8  4.1  290 0   0      error (7) 0 --- inspect 13     7.6   300   .75 0     unknown 0 --- inspect 5.7  3.2  280 0      0     true -32 --- inspect .82   .82   22    .31  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 320 300   8200 4000 .68 13      true -32 wit inspect 6.6  3.5  290 0   0      error (7) 0 --- inspect 12     7.0   290   .75 0     unknown 0 --- inspect 5.3  2.9  280 0      0     true -32 --- inspect .80   .79   22    .31  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 380 360   5300 4400 .97 0      true -32 wit inspect 8.9  4.7  330 0   0      error (7) 0 --- inspect 16     9.0   300   .75 0     timeout 0 --- inspect 4.6  130    220 .016  0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 330 300   4700 3500 .68 0      true -32 wit inspect 6.8  3.6  290 0   0      error (7) 0 --- inspect 14     8.1   290   .75 0     unknown 0 --- inspect 6.0  3.3  280 0      0     true -32 --- inspect .84   .84   23    .32  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 380 350   6000 4800 .98 0      true -32 wit inspect 10    5.4  340 0   0      error (7) 0 --- inspect 15     8.5   290   .71 0     timeout 0 --- inspect 5.6  130    220 .016  0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 330 300   4700 3600 .68 0      true -32 wit inspect 6.6  3.5  290 0   .074  error (7) 0 --- inspect 13     7.7   290   .75 0     unknown 0 --- inspect 5.7  3.2  280 0      0     true -32 --- inspect .81   .81   23    .32  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 370 340   7800 5100 .97 .045  true -32 wit inspect 8.5  4.4  340 0   0      error (7) 0 --- inspect 13     7.7   290   .75 0     timeout 0 --- inspect 4.5  130    220 .053  0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 330 300   4700 3500 .68 0      true -32 wit inspect 6.7  3.5  300 0   0      error (7) 0 --- inspect 13     7.5   290   .75 0     unknown 0 --- inspect 5.4  3.0  280 0      .12  true -32 --- inspect .85   .88   22    .32  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 370 350   6000 4300 .93 0      true -32 wit inspect 8.7  4.6  300 0   0      error (7) 0 --- inspect 13     7.7   290   .75 0     timeout 0 --- inspect 4.6  130    220 .057  0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 330 300   4700 3700 .68 .16   true -32 wit inspect 6.7  3.6  290 0   0      error (7) 0 --- inspect 14     8.4   290   .75 0     unknown 0 --- inspect 5.6  3.1  280 0      .074 true -32 --- inspect .83   .82   22    .31  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 370 350   5300 4200 .88 0      true -32 wit inspect 8.1  4.2  300 0   0      error (7) 0 --- inspect 14     8.3   290   .75 .078 timeout 0 --- inspect 4.2  130    210 .0041 0     error (2) 0 --- inspect 1.1    1.1    22    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 370 350   5700 4200 .98 .049  true -32 wit inspect 8.7  4.5  350 0   0      error (7) 0 --- inspect 13     7.6   290   .75 0     timeout 0 --- inspect 5.0  130    220 .0041 0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(unreach-call) 0 wit inspect 380 350   5300 3900 .98 .078  true -32 wit inspect 8.7  4.5  340 0   0      error (7) 0 --- inspect 12     6.7   290   .75 .078 timeout 0 --- inspect 4.7  130    220 .016  0     error (2) 0 --- inspect 1.3    1.3    23    .11  0     - --- inspect - --- inspect
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 1 wit inspect 180 100   2300 1900 150    0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    7.7  460 0   0      error (7) 0 --- inspect 15     8.4   300   .75 0     
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 2000 .16 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 2000 .16 .43   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .42 41 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c out of memory 0 --- inspect 140 120   15000 1800 .16 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 --- inspect 900 880   8300 7500 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 --- inspect 900 880   7000 8400 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0      error (2) 0 --- inspect .025 .025 5.8 0    0     
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   5300 8100 .88 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   4600 7600 .87 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 40 0   0      error (2) 0 --- inspect .027 .027 5.5 0    0     
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   7200 11000 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   4700 8300 .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   8100 9800 .86 .29   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   4700 8400 .87 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   5300 8200 .92 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   4700 6200 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   5300 8200 .89 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   5500 7300 .88 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 --- inspect 900 870   5300 9700 .83 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 41 0   0      error (2) 0 --- inspect .021 .022 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 67 35000 32000 340000 360000 3800 110    42 -525 380 220 16000 0   .43   42 -46 790 520 22000 27   .41  42 10 220 1100 11000 .22 .32 42 -568 230   230   940 7.9 .43  52 46 280 160 11000 0   .0082 52 44 1800 1300 35000 15 .053
    correct results 43 66 5300 4100 48000 57000 3600 86    19 19 140 80 5800 0   .0082 18 18 210 120 7100 12   .098 10 10 52 29 2700 0    0    8 8 5.7 5.7 170 1.2 .094 23 46 240 140 9000 0   .0082 22 44 1700 1200 27000 14 .053
        correct true 23 46 2900 2100 39000 30000 3500 85    0 0 0 0 23 46 240 140 9000 0   .0082 22 44 1700 1200 27000 14 .053
        correct false 20 20 2400 2000 9000 27000 13 .92 19 19 140 80 5800 0   .0082 18 18 210 120 7100 12   .098 10 10 52 29 2700 0    0    8 8 5.7 5.7 170 1.2 .094 0 0
    correct-unconfimed results 20 1 7000 6300 100000 79000 220 21    0 0 0 0 0 0
        correct-unconfirmed true 1 1 180 100 2300 1900 150 0    0 0 0 0 0 0
        correct-unconfirmed false 19 0 6800 6200 100000 77000 75 21    0 0 0 0 0 0
    incorrect results 0 17 -544 140 72 5200 0   .074  2 -64 140 100 3800 1.2 .16  0 18 -576 14   14   400 4.4 0     0 0
        incorrect true 0 17 -544 140 72 5200 0   .074  2 -64 140 100 3800 1.2 .16  0 18 -576 14   14   400 4.4 0     0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 67 -525 -46 10 -568 46 44
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-ControlFlow