Tool ULTIMATE Kojak f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   760   14000 2000 2.3 0      error (invalid witness file) .65 .41 6.4 42 error (invalid witness file) 6.3 3.3 140 290 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 390   320   5500 2100 2.6 0      error (invalid witness file) 5.0  2.7  53   220 false(unreach-call) 13   6.6 220 460 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 470   390   6400 1700 2.6 0      error (invalid witness file) 4.5  2.4  50   240 false(unreach-call) 15   7.7 240 540 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 36   13   330 810 2.6 0      error (invalid witness file) 4.0  2.2  63   230 false(unreach-call) 12   6.4 250 440 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 750   630   11000 1900 3.4 0      - - true 32    17    250   740 true 97   56   960 1200
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   770   12000 4200 2.3 0      - - error (invalid witness file) .58 .38 12   44 error (invalid witness file) 6.8 3.5 130 310
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   730   13000 2500 2.3 0      - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 5.9 3.1 93 300
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   760   15000 2100 2.3 0      - - error (invalid witness file) .51 .32 14   40 error (invalid witness file) 6.2 3.3 110 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 21   7.2 200 580 2.7 0      - - true 6.5  3.5  130   280 false(unreach-call) 17   9.5 240 550
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 33   11   280 800 2.9 0      - - true 10    5.4  130   360 true 30   16   420 570
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 540   460   7700 1600 2.7 0      true 13    6.7  99   440 false(unreach-call) 13   6.6 210 480 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 380   310   5700 1500 2.7 0      true 10    5.3  160   440 false(unreach-call) 12   6.3 210 460 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 340   280   4700 1600 2.8 0      true 12    6.4  130   450 false(unreach-call) 12   6.5 140 560 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 460   370   5500 1500 2.7 0      true 11    5.7  120   430 false(unreach-call) 11   6.0 140 490 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 8.2 2.4 61 400 2.6 0      true 8.3  4.4  82   340 false(unreach-call) 10   5.5 160 390 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c timeout 0 wit inspect 900   770   13000 1900 2.3 0      error (invalid witness file) .50 .32 8.4 40 error (invalid witness file) 6.2 3.3 120 300 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c timeout 0 wit inspect 900   770   13000 1500 2.3 0      error (invalid witness file) .48 .32 6.2 40 error (invalid witness file) 5.9 3.1 120 300 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c timeout 0 wit inspect 900   780   14000 1500 2.3 0      error (invalid witness file) .51 .32 10   39 error (invalid witness file) 6.0 3.2 120 300 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 27   8.9 220 740 2.6 0      true 11    5.9  130   430 false(unreach-call) 12   6.5 200 450 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 250   200   3800 1300 2.7 0      true 10    5.4  100   430 false(unreach-call) 14   7.2 230 520 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 240   190   3400 1300 2.7 0      true 12    6.1  200   450 false(unreach-call) 12   6.2 150 490 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 7.9 2.3 55 370 2.6 0      false(unreach-call) 7.0  3.8  82   290 false(unreach-call) 10   5.5 150 370 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c timeout 0 wit inspect 900   770   12000 1400 2.3 0      - - error (invalid witness file) .57 .37 9.9 40 error (invalid witness file) 6.6 3.5 130 300
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   770   13000 3600 2.3 0      - - error (invalid witness file) .60 .39 9.9 40 error (invalid witness file) 5.8 3.0 83 300
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c timeout 0 wit inspect 900   780   16000 1800 2.3 0      - - error (invalid witness file) .48 .31 7.7 40 error (invalid witness file) 5.9 3.1 100 300
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 0 wit inspect 900   770   15000 2100 2.3 0      - - error (invalid witness file) .60 .38 9.3 40 error (invalid witness file) 6.1 3.2 130 300
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 0 wit inspect 900   780   13000 1400 2.3 0      - - error (invalid witness file) .47 .31 10   39 error (invalid witness file) 6.5 3.4 140 310
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 45   23   510 950 2.6 0      - - true 11    5.6  170   380 true 40   23   580 840
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect 13   4.1 100 490 2.6 0      - - true 6.4  3.5  76   290 true 15   8.3 240 400
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 0 wit inspect 900   780   12000 1200 2.3 0      - - error (invalid witness file) .55 .36 10   40 error (invalid witness file) 6.2 3.3 120 300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 0 wit inspect 900   780   12000 1400 2.3 0      - - error (invalid witness file) .58 .37 9.6 39 error (invalid witness file) 6.0 3.2 120 300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 0 wit inspect 900   780   12000 1300 2.3 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.2 3.3 120 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 0 wit inspect 900   780   13000 1800 2.3 .0082 - - error (invalid witness file) .51 .32 11   42 error (invalid witness file) 7.3 3.8 120 320
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 0 wit inspect 900   780   14000 2800 2.3 0      - - error (invalid witness file) .50 .34 10   39 error (invalid witness file) 6.5 3.4 120 310
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 0 wit inspect 900   790   15000 1400 2.3 0      - - error (invalid witness file) .49 .32 11   42 error (invalid witness file) 5.8 3.1 120 290
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.9 2.1 52 330 2.5 0      true 4.8  2.6  55   270 false(unreach-call) 9.7 5.2 150 340 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect 6.7 2.0 51 320 2.5 0      true 4.6  2.5  93   290 false(unreach-call) 9.3 5.0 160 340 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 24   9.9 230 750 2.6 0      - - true 8.0  4.3  99   320 true 24   13   410 800
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 29   13   300 690 2.6 0      - - true 7.0  3.8  120   310 true 25   13   250 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 34   17   400 870 2.6 0      - - true 7.4  4.0  120   290 true 30   17   290 1900
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 42   23   500 890 2.6 0      - - true 8.0  4.3  78   300 true 43   26   630 3400
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 49   30   480 970 2.6 0      - - true 7.0  3.7  140   300 true 88   54   1200 6100
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 59   38   730 1000 2.6 0      - - true 8.9  4.8  99   300 out of memory 100   63   1500 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 10   3.0 87 470 2.6 0      - - true 5.7  3.1  87   280 true 10   5.5 180 350
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 12   3.4 98 470 2.6 0      - - true 6.7  3.6  80   280 true 12   6.3 200 390
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 15   4.5 110 480 2.6 0      - - true 6.9  3.7  87   290 true 13   7.0 190 440
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 18   5.7 150 730 2.6 0      - - true 6.9  3.7  72   290 true 15   8.1 240 560
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect 21   7.6 190 610 2.6 0      - - true 6.8  3.7  110   290 true 18   9.3 250 560
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900   820   12000 12000 2.3 0      error (invalid witness file) .48 .31 12   40 error (invalid witness file) 7.0 3.7 130 320 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 120   91   1300 3100 2.5 0      exception 5.3  2.8  81   230 false(unreach-call) 15   8.1 220 530 - -
ntdrivers/floppy_false-unreach-call.i.cil.c timeout 0 wit inspect 900   850   10000 11000 2.5 0      error (invalid witness file) .49 .33 8.4 39 error (invalid witness file) 6.5 3.4 73 300 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c timeout 0 wit inspect 900   800   11000 3300 2.3 0      error (invalid witness file) .52 .33 14   40 error (invalid witness file) 6.4 3.4 140 310 - -
ntdrivers/parport_false-unreach-call.i.cil.c timeout 0 wit inspect 900   850   10000 1600 2.5 0      error (invalid witness file) .59 .37 7.9 42 error (invalid witness file) 6.8 3.6 130 300 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   11000 12000 2.3 0      - - error (invalid witness file) .62 .40 7.9 39 error (invalid witness file) 7.1 3.7 140 310
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   15000 5100 2.3 0      - - error (invalid witness file) .56 .36 10   39 error (invalid witness file) 6.8 3.6 130 300
ntdrivers/floppy2_true-unreach-call.i.cil.c timeout 0 wit inspect 900   850   13000 12000 2.5 0      - - error (invalid witness file) .64 .40 6.6 39 error (invalid witness file) 7.6 4.1 130 330
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c timeout 0 wit inspect 900   850   11000 10000 2.5 0      - - error (invalid witness file) .60 .37 10   41 error (invalid witness file) 6.7 3.5 89 310
ntdrivers/parport_true-unreach-call.i.cil.c timeout 0 wit inspect 900   810   13000 2900 2.3 0      - - error (invalid witness file) .65 .43 8.8 40 error (invalid witness file) 7.3 3.8 110 320
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error 0 wit inspect 650   580   8200 1500 2.5 0      error (invalid witness file) .68 .43 8.2 45 error (invalid witness file) 5.9 3.1 110 300 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error 0 wit inspect 500   450   6400 1200 2.5 0      error (invalid witness file) .54 .36 10   43 error (invalid witness file) 6.4 3.3 120 300 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error 0 wit inspect 390   350   5400 1200 2.5 0      error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.5 3.4 120 310 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error 0 wit inspect 470   410   5900 1300 2.5 0      error (invalid witness file) .52 .32 12   41 error (invalid witness file) 6.1 3.2 120 310 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error 0 wit inspect 310   260   3800 2700 2.5 0      error (invalid witness file) .65 .41 7.4 40 error (invalid witness file) 6.2 3.3 120 300 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error 0 wit inspect 310   250   3600 1700 2.5 0      error (invalid witness file) .49 .33 10   39 error (invalid witness file) 6.2 3.3 120 300 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error 0 wit inspect 450   380   5400 1400 2.5 0      error (invalid witness file) .53 .35 8.9 40 error (invalid witness file) 6.3 3.3 130 300 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error 0 wit inspect 330   270   3800 3400 2.5 0      error (invalid witness file) .60 .38 8.9 44 error (invalid witness file) 7.2 3.8 150 310 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   12000 1500 2.3 0      error (invalid witness file) .59 .39 8.0 42 error (invalid witness file) 6.5 3.4 130 310 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   13000 1800 2.3 0      error (invalid witness file) .49 .33 8.6 40 error (invalid witness file) 6.8 3.6 120 310 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   11000 1500 2.3 0      error (invalid witness file) .56 .36 10   40 error (invalid witness file) 5.9 3.1 130 290 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 1800 2.3 0      error (invalid witness file) .56 .36 11   44 error (invalid witness file) 6.2 3.3 120 310 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   13000 1400 2.3 0      error (invalid witness file) .61 .40 9.7 41 error (invalid witness file) 5.6 3.1 110 290 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error 0 wit inspect 730   650   9500 2100 2.5 0      error (invalid witness file) .62 .40 8.5 40 error (invalid witness file) 6.1 3.2 74 310 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 1700 2.3 0      error (invalid witness file) .54 .34 6.9 42 error (invalid witness file) 5.9 3.2 130 300 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   13000 2700 2.3 0      error (invalid witness file) .58 .36 7.9 40 error (invalid witness file) 6.6 3.5 120 300 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   11000 1700 2.3 0      error (invalid witness file) .56 .36 14   43 error (invalid witness file) 6.3 3.3 110 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 0 wit inspect 900   780   11000 1600 2.3 0      error (invalid witness file) .48 .32 7.8 40 error (invalid witness file) 6.0 3.2 130 290 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 0 wit inspect 900   790   12000 1500 2.3 .074  error (invalid witness file) .65 .42 8.3 40 error (invalid witness file) 7.0 3.7 100 300 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   12000 1500 2.3 0      - - error (invalid witness file) .64 .41 7.8 41 error (invalid witness file) 6.9 3.6 110 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   11000 1300 2.3 0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 8.6 4.5 98 310
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   11000 1600 2.3 0      - - error (invalid witness file) .64 .41 8.5 40 error (invalid witness file) 6.7 3.6 130 320
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 1400 2.3 0      - - error (invalid witness file) .54 .35 9.4 39 error (invalid witness file) 6.3 3.3 88 320
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   15000 1700 2.3 0      - - error (invalid witness file) .55 .35 12   44 error (invalid witness file) 5.7 3.1 95 290
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 1400 2.3 0      - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.2 3.3 120 300
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 2400 2.3 0      - - error (invalid witness file) .63 .40 8.0 40 error (invalid witness file) 5.9 3.2 84 290
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   13000 2400 2.3 0      - - error (invalid witness file) .54 .34 12   40 error (invalid witness file) 6.2 3.3 100 300
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   12000 1600 2.3 0      - - error (invalid witness file) .57 .37 10   39 error (invalid witness file) 6.7 3.5 110 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   12000 2700 2.3 0      - - error (invalid witness file) .55 .34 10   40 error (invalid witness file) 6.4 3.4 120 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   13000 1500 2.3 0      - - error (invalid witness file) .49 .31 9.8 39 error (invalid witness file) 6.0 3.2 120 290
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 2500 2.3 0      - - error (invalid witness file) .71 .45 8.6 42 error (invalid witness file) 6.2 3.3 110 310
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 2100 2.3 0      - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.2 3.3 110 320
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   15000 3200 2.3 0      - - error (invalid witness file) .62 .38 9.1 39 error (invalid witness file) 5.8 3.1 110 290
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900   800   14000 1600 2.3 0      - - error (invalid witness file) .51 .33 13   43 error (invalid witness file) 5.9 3.1 100 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   14000 1600 2.3 0      - - error (invalid witness file) .66 .41 5.8 40 error (invalid witness file) 6.0 3.2 76 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900   790   13000 1600 2.3 0      - - error (invalid witness file) .67 .42 9.0 41 error (invalid witness file) 6.2 3.3 81 310
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 94 47 57000 50000 810000 200000 230 .082 94 140 75 1700 6300   94 350 190 6000 15000   94 170 90 2200 6800   94 810 460 12000 37000  
    correct results 31 47 4500 3500 60000 31000 82 0     11 120 65 1500 5200   15 180 95 2800 6900   16 140 77 1900 5300   15 580 330 7800 26000  
        correct true 16 32 1200 830 15000 13000 42 0     10 0 0 0 0   0 0 0 0 0   16 140 77 1900 5300   14 580 330 7800 26000  
        correct false 15 15 3300 2600 45000 19000 40 0     1 120 65 1500 5200   15 180 95 2800 6900   0 0 0 0 0   1 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (94 tasks, max score: 146) 47
Run set sv-comp17.ReachSafety-ControlFlow