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-Recursive
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)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   10000 1400 2.3 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.6 3.0 86 290 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 6.9 2.2 54 330 2.5 0      false(unreach-call) 4.1  2.3  55   270 false(unreach-call) 7.8 4.1 160 320 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 6.2 1.9 49 330 2.5 0      true 3.6  2.0  56   280 false(unreach-call) 7.4 3.9 120 320 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 6.0 1.8 52 340 2.5 0      false(unreach-call) 3.7  2.0  64   270 false(unreach-call) 7.4 3.9 110 320 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 11   3.0 85 490 2.5 0      false(unreach-call) 62    43    570   2200 false(unreach-call) 26   14   260 840 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 21   6.0 170 1300 2.6 0      timeout 97    70    1000   4500 timeout 97   70   1400 4300 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.6 1.8 47 320 2.5 0      false(unreach-call) 4.4  2.5  37   280 false(unreach-call) 7.0 3.7 140 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   510   10000 1300 2.3 0      - - error (invalid witness file) .49 .32 9.3 39 error (invalid witness file) 5.6 3.0 83 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   590   11000 1900 2.3 0      - - error (invalid witness file) .69 .44 7.6 39 error (invalid witness file) 5.8 3.1 97 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   590   11000 2000 2.3 0      - - error (invalid witness file) .62 .41 8.3 40 error (invalid witness file) 6.2 3.3 100 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.0 2.6 59 460 2.5 0      - - error (recursion) 4.5  2.5  53   260 true 12   6.4 260 370
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   810   7700 2500 2.3 0      - - error (invalid witness file) .56 .34 9.5 40 error (invalid witness file) 5.6 3.0 72 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   820   12000 850 2.3 0      - - error (invalid witness file) .51 .33 8.7 41 error (invalid witness file) 6.0 3.2 100 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   540   9800 1100 2.3 .012  - - error (invalid witness file) .55 .37 12   44 error (invalid witness file) 5.7 3.0 88 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   790   14000 5100 2.3 0      - - error (invalid witness file) .59 .38 7.1 40 error (invalid witness file) 6.2 3.3 110 300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   790   12000 5300 2.3 0      - - error (invalid witness file) .67 .41 7.7 40 error (invalid witness file) 5.5 2.9 82 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.0 2.2 61 360 2.5 0      - - error (recursion) 4.1  2.3  57   260 true 9.3 5.0 170 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   590   12000 1500 2.3 0      - - error (invalid witness file) .53 .33 13   40 error (invalid witness file) 5.4 2.9 110 280
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   650   12000 1100 2.3 0      - - error (invalid witness file) .57 .37 11   39 error (invalid witness file) 5.7 3.1 93 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.7 2.4 67 410 2.5 0      - - error (recursion) 3.6  2.0  71   250 true 11   6.4 210 380
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   660   11000 890 2.3 0      - - error (invalid witness file) .64 .40 7.4 39 error (invalid witness file) 5.3 2.9 75 290
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   590   12000 1300 2.3 0      - - error (invalid witness file) .54 .34 9.2 39 error (invalid witness file) 5.9 3.1 89 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.9 1.9 42 330 2.5 0      - - error (recursion) 4.3  2.4  42   260 true 8.2 4.5 150 330
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 9.2 3.0 81 460 2.5 0      - - error (recursion) 3.5  2.0  60   260 timeout 960   950   14000 2600
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.0 1.9 47 320 2.5 0      true 4.0  2.3  49   280 false(unreach-call) 7.2 3.9 140 310 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.4 2.0 47 330 2.5 0      true 3.5  1.9  39   270 false(unreach-call) 8.8 4.7 170 340 - -
recursive-simple/fibo_10_false-unreach-call.c timeout 0 wit inspect 900   590   11000 1800 2.3 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.2 3.3 120 290 - -
recursive-simple/fibo_15_false-unreach-call.c timeout 0 wit inspect 900   650   11000 2000 2.3 0      error (invalid witness file) .50 .33 11   41 error (invalid witness file) 6.7 3.5 130 330 - -
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 900   570   11000 2100 2.3 0      error (invalid witness file) .52 .33 12   43 error (invalid witness file) 6.8 3.6 120 300 - -
recursive-simple/fibo_25_false-unreach-call.c timeout 0 wit inspect 900   570   12000 1800 2.3 0      error (invalid witness file) .49 .31 8.3 40 error (invalid witness file) 5.6 3.0 110 290 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c timeout 0 wit inspect 900   520   9600 1700 2.3 0      error (invalid witness file) .52 .34 12   39 error (invalid witness file) 5.9 3.1 99 310 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 0 wit inspect 900   660   12000 1100 2.3 0      error (invalid witness file) .57 .37 8.7 40 error (invalid witness file) 6.0 3.2 120 290 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 900   520   12000 1500 2.3 0      error (invalid witness file) .51 .34 9.0 40 error (invalid witness file) 5.8 3.1 83 300 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 900   520   10000 1600 2.3 0      error (invalid witness file) .65 .43 7.5 40 error (invalid witness file) 6.1 3.2 120 300 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.9 2.1 51 330 2.5 0      false(unreach-call) 3.8  2.1  50   280 false(unreach-call) 7.5 4.0 120 320 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c timeout 0 wit inspect 900   700   12000 1100 2.3 0      error (invalid witness file) .51 .33 9.5 40 error (invalid witness file) 6.0 3.2 110 290 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c timeout 0 wit inspect 900   670   11000 1100 2.3 0      error (invalid witness file) .52 .35 8.0 40 error (invalid witness file) 5.8 3.1 110 290 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c timeout 0 wit inspect 900   520   11000 1700 2.3 0      error (invalid witness file) .51 .32 8.3 40 error (invalid witness file) 5.6 3.1 120 290 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c timeout 0 wit inspect 900   660   14000 1100 2.3 0      error (invalid witness file) .54 .35 11   40 error (invalid witness file) 6.1 3.2 120 300 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c timeout 0 wit inspect 900   580   10000 1900 2.3 0      error (invalid witness file) .62 .41 7.2 40 error (invalid witness file) 6.3 3.3 120 300 - -
recursive-simple/fibo_7_false-unreach-call.c timeout 0 wit inspect 900   570   10000 1900 2.3 0      error (invalid witness file) .56 .36 11   42 error (invalid witness file) 6.0 3.3 110 300 - -
recursive-simple/id2_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect 6.8 2.1 53 330 2.5 0      false(unreach-call) 5.7  3.1  76   290 false(unreach-call) 8.2 4.3 170 330 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.5 2.7 66 500 2.5 0      false(unreach-call) 6.6  3.6  66   290 false(unreach-call) 8.2 4.4 170 330 - -
recursive-simple/id_b3_o2_false-unreach-call.c false(unreach-call) 1 wit inspect 7.2 2.2 61 330 2.5 0      false(unreach-call) 5.3  2.9  64   290 false(unreach-call) 7.4 4.0 150 320 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 20   7.5 190 600 2.5 0      false(unreach-call) 8.2  4.4  130   410 true 7.4 3.9 130 320 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 36   18   350 830 2.5 0      false(unreach-call) 11    5.8  140   470 true 7.5 4.0 100 310 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 83   55   1200 1600 2.5 0      false(unreach-call) 14    7.2  120   520 true 8.0 4.2 140 320 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 140   100   1800 1300 2.5 0      false(unreach-call) 18    9.5  140   690 true 7.5 4.0 140 330 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.8 2.6 65 470 2.5 0      false(unreach-call) 6.0  3.3  85   290 false(unreach-call) 7.7 4.1 130 320 - -
recursive-simple/id_o1000_false-unreach-call.c timeout 0 wit inspect 900   730   13000 3900 2.3 0      error (invalid witness file) .52 .33 12   39 error (invalid witness file) 5.9 3.1 120 300 - -
recursive-simple/id_o100_false-unreach-call.c false(unreach-call) 0 wit inspect 290   230   3900 1800 2.6 0      timeout 97    78    1100   4100 true 9.9 5.2 190 520 - -
recursive-simple/id_o10_false-unreach-call.c false(unreach-call) 1 wit inspect 12   3.5 100 480 2.5 0      false(unreach-call) 12    6.2  170   480 true 8.1 4.3 160 320 - -
recursive-simple/id_o200_false-unreach-call.c timeout 0 wit inspect 900   730   13000 3600 2.3 0      error (invalid witness file) .54 .35 8.1 39 error (invalid witness file) 6.0 3.2 110 300 - -
recursive-simple/id_o20_false-unreach-call.c false(unreach-call) 1 wit inspect 22   7.6 180 790 2.5 0      false(unreach-call) 26    14    330   1400 true 8.3 4.4 150 320 - -
recursive-simple/id_o3_false-unreach-call.c false(unreach-call) 1 wit inspect 7.7 2.3 57 350 2.5 0      false(unreach-call) 6.9  3.7  59   300 false(unreach-call) 7.5 4.0 140 310 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 10   2.9 77 480 2.5 0      false(unreach-call) 6.4  3.4  73   300 true 7.5 4.0 150 320 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   3.7 110 500 2.5 0      false(unreach-call) 8.2  4.3  110   460 true 8.2 4.3 170 320 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 17   4.7 120 540 2.5 0      false(unreach-call) 10    5.4  130   460 true 8.1 4.3 160 330 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 20   6.1 170 620 2.5 0      false(unreach-call) 12    6.3  140   490 true 9.5 5.0 120 330 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.9 2.0 54 340 2.5 0      false(unreach-call) 4.8  2.7  41   280 false(unreach-call) 7.2 3.9 150 320 - -
recursive-simple/sum_non_eq_false-unreach-call.c false(unreach-call) 1 wit inspect 5.5 1.7 43 320 2.5 0      false(unreach-call) 4.3  2.4  51   270 false(unreach-call) 7.1 3.8 110 310 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.9 1.8 43 350 2.5 0      false(unreach-call) 3.6  2.1  79   270 false(unreach-call) 7.3 3.9 95 330 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 5.6 1.7 41 330 2.5 0      - - true 4.5  2.5  44   260 true 7.6 4.0 140 320
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 5.6 1.8 44 320 2.5 0      - - true 3.7  2.1  57   260 true 7.0 3.8 140 320
recursive-simple/fibo_10_true-unreach-call.c timeout 0 wit inspect 900   820   12000 5200 2.3 0      - - error (invalid witness file) .69 .44 9.1 45 error (invalid witness file) 5.7 3.0 92 300
recursive-simple/fibo_15_true-unreach-call.c timeout 0 wit inspect 900   850   13000 5200 2.3 0      - - error (invalid witness file) .49 .32 11   41 error (invalid witness file) 6.1 3.2 120 300
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900   850   15000 5200 2.3 0      - - error (invalid witness file) .62 .40 7.9 40 error (invalid witness file) 5.9 3.2 120 300
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900   840   11000 5300 2.3 0      - - error (invalid witness file) .70 .43 6.2 40 error (invalid witness file) 6.0 3.2 120 310
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 wit inspect 900   810   12000 5100 2.3 0      - - error (invalid witness file) .63 .39 8.2 39 error (invalid witness file) 6.0 3.2 91 300
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 wit inspect 900   810   12000 5300 2.3 0      - - error (invalid witness file) .67 .43 7.2 40 error (invalid witness file) 5.7 3.0 110 300
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900   810   12000 5200 2.3 0      - - error (invalid witness file) .50 .33 9.3 39 error (invalid witness file) 5.9 3.1 61 300
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900   810   12000 5200 2.3 0      - - error (invalid witness file) .64 .41 7.9 41 error (invalid witness file) 6.4 3.4 130 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   630   12000 1300 2.3 0      - - error (invalid witness file) .53 .33 11   41 error (invalid witness file) 5.8 3.1 86 300
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 wit inspect 900   700   13000 1100 2.3 0      - - error (invalid witness file) .54 .35 9.7 40 error (invalid witness file) 6.4 3.4 130 310
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   670   13000 1100 2.3 0      - - error (invalid witness file) .56 .36 9.2 39 error (invalid witness file) 5.7 3.0 110 300
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c timeout 0 wit inspect 900   530   12000 1800 2.3 0      - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.0 3.2 110 300
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 wit inspect 900   740   12000 2900 2.3 .012  - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.8 3.1 65 300
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   530   12000 1800 2.3 0      - - error (invalid witness file) .66 .42 8.3 42 error (invalid witness file) 5.9 3.1 110 300
recursive-simple/fibo_7_true-unreach-call.c timeout 0 wit inspect 900   650   13000 3300 2.3 0      - - error (invalid witness file) .62 .40 10   44 error (invalid witness file) 6.0 3.2 87 300
recursive-simple/id2_b2_o3_true-unreach-call.c true 2 wit inspect 6.6 2.0 51 340 2.5 0      - - error (recursion) 3.7  2.1  61   260 true 8.5 4.6 160 330
recursive-simple/id2_b3_o5_true-unreach-call.c true 2 wit inspect 6.2 2.1 49 330 2.5 0      - - error (recursion) 3.9  2.2  70   260 true 8.3 4.5 150 310
recursive-simple/id2_b5_o10_true-unreach-call.c true 2 wit inspect 6.2 2.0 45 330 2.5 0      - - error (recursion) 3.5  2.0  68   250 true 8.2 4.5 130 310
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   770   13000 1100 2.3 .0041 - - error (invalid witness file) .56 .35 8.4 39 error (invalid witness file) 5.9 3.1 100 300
recursive-simple/id_b2_o3_true-unreach-call.c true 2 wit inspect 6.0 2.0 48 330 2.5 0      - - error (recursion) 4.3  2.4  49   250 true 8.6 4.7 170 330
recursive-simple/id_b3_o5_true-unreach-call.c true 2 wit inspect 6.0 1.9 49 330 2.5 0      - - error (recursion) 4.5  2.5  51   260 true 8.8 4.8 150 320
recursive-simple/id_b5_o10_true-unreach-call.c true 2 wit inspect 6.4 1.9 48 340 2.5 0      - - error (recursion) 3.4  2.0  68   260 true 8.1 4.4 92 320
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 12   4.5 110 570 2.5 0      - - error (recursion) 4.0  2.3  38   260 true 16   9.2 210 550
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 18   6.8 140 600 2.5 0      - - error (recursion) 3.4  1.9  71   260 true 22   12   290 530
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 23   9.6 210 720 2.5 0      - - error (recursion) 4.4  2.5  44   260 true 32   18   400 710
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 29   13   290 800 2.5 0      - - error (recursion) 4.0  2.3  40   250 true 37   22   350 810
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 9.8 3.0 84 480 2.5 0      - - error (recursion) 4.3  2.4  44   250 true 12   6.7 210 380
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   760   14000 1000 2.3 0      - - error (invalid witness file) .60 .37 8.0 40 error (invalid witness file) 6.0 3.2 110 300
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   770   13000 1000 2.3 0      - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.0 3.2 110 310
recursive-simple/sum_20x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   770   13000 1100 2.3 0      - - error (invalid witness file) .64 .41 8.7 39 error (invalid witness file) 5.9 3.1 100 310
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   770   13000 1300 2.3 0      - - error (invalid witness file) .65 .42 7.4 40 error (invalid witness file) 6.5 3.4 95 310
recursive-simple/sum_2x3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   600   9900 930 2.3 0      - - error (invalid witness file) .49 .31 9.3 39 error (invalid witness file) 5.8 3.1 110 300
recursive-simple/sum_non_eq_true-unreach-call.c true 2 wit inspect 6.7 2.1 52 330 2.5 0      - - error (recursion) 3.7  2.1  61   260 true 9.2 5.0 120 340
recursive-simple/sum_non_true-unreach-call_true-termination.c true 2 wit inspect 6.6 2.1 50 330 2.5 0      - - error (recursion) 3.4  1.9  63   260 true 9.5 5.2 110 350
../../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 98 65 46000   35000   600000 140000 240   .029 98 460 300 5200 21000   98 430 250 7300 19000   98 98   57   1400 6500   98 1400 1200 21000 20000  
    correct results 45 64 670   310   6700 22000 110   0     26 260 150 2900 12000   26 220 120 3700 8900   2 75   42   1100 4900   19 240 140 3600 7700  
        correct true 19 38 180   66   1500 8000 48   0     3 0 0 0 0   10 0 0 0 0   2 75   42   1100 4900   19 240 140 3600 7700  
        correct false 26 26 490   240   5100 14000 66   0     23 260 150 2900 12000   16 220 120 3700 8900   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 3 1 320   240   4200 3500 7.7 0     0 190 150 2100 8600   1 110 75 1600 4800   0 3.5 2.0 60 260   0 960 950 14000 2600  
        correct-unconfirmed true 1 1 9.2 3.0 81 460 2.5 0     0 0 0 0 0   1 0 0 0 0   0 3.5 2.0 60 260   0 960 950 14000 2600  
        correct-unconfirmed false 2 0 310   230   4100 3000 5.2 0     0 190 150 2100 8600   0 110 75 1600 4800   0 0   0   0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 65
Run set sv-comp17.ReachSafety-Recursive