Tool VeriAbs
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-14 09:46:18 CET [[ 2017-01-15 04:55:34 CET ]] [[ 2017-01-15 05:46:09 CET ]] [[ 2017-01-15 05:17:25 CET ]] [[ 2017-01-15 05:48:02 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/veriabs.2017-01-14_0946.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/veriabs.2017-01-14_0946.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 unknown 0 wit inspect 830   830   4500 480 .35  0      error (invalid witness file) .57 .36 12   43 error (invalid witness file) 5.8 3.1 120 300 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (124) 0 wit inspect 900   900   6700 5100 .85  0      error (invalid witness file) .50 .32 3.5 40 error (invalid witness file) 6.3 3.3 130 310 - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.6 2.6 45 270 .086 0      error (invalid witness file) .50 .32 5.2 42 error (invalid witness file) 6.8 3.6 140 320 - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 5.2 2.7 48 150 .25  0      error (invalid witness file) .48 .33 8.4 40 error (invalid witness file) 5.7 3.0 120 290 - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 770   760   4600 190 .34  0      error (invalid witness file) .49 .32 13   39 error (invalid witness file) 5.1 2.7 70 290 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 770   770   3600 190 .34  0      error (invalid witness file) .51 .33 11   42 error (invalid witness file) 5.8 3.1 100 300 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 540   530   2800 330 .27  .094  error (invalid witness file) .54 .35 11   44 error (invalid witness file) 5.7 3.1 110 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 740   740   3600 370 .40  0      - - error (invalid witness file) .48 .31 12   40 error (invalid witness file) 6.0 3.1 98 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 740   740   3900 450 .49  0      - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.6 3.5 130 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 740   740   3800 400 .40  0      - - error (invalid witness file) .54 .35 8.7 39 error (invalid witness file) 5.7 3.0 120 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   900   7900 5000 3.8   0      - - error (invalid witness file) .57 .37 5.6 42 error (invalid witness file) 6.1 3.2 130 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout (error (124)) 0 wit inspect 900   900   5900 8400 1.9   0      - - error (invalid witness file) .48 .33 6.1 40 error (invalid witness file) 6.3 3.3 120 290
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 5.3 2.7 52 150 .25  0      - - error (invalid witness file) .53 .33 9.6 40 error (invalid witness file) 6.0 3.2 110 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 770   770   3600 190 .37  0      - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.3 3.3 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.6 2.5 63 290 .045 0      - - error (recursion) 3.4  1.9  54   260 true 32   18   610 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 770   770   3000 190 .38  0      - - error (invalid witness file) .50 .33 9.5 41 error (invalid witness file) 8.0 4.2 120 320
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 660   650   4100 330 .42  0      - - error (invalid witness file) .51 .34 4.7 40 error (invalid witness file) 6.0 3.2 130 310
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 850   850   6400 2500 .70  0      - - error (invalid witness file) .52 .32 11   39 error (invalid witness file) 5.3 2.9 110 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 780   770   6500 2500 1.4   0      - - error (invalid witness file) .46 .30 6.7 40 error (invalid witness file) 5.8 3.1 110 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   900   7400 6700 .72  .76   - - error (invalid witness file) .56 .36 6.0 42 error (invalid witness file) 6.4 3.4 120 290
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   900   7300 5400 1.9   0      - - error (invalid witness file) .48 .30 4.8 39 error (invalid witness file) 5.4 2.9 100 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 650   650   3900 180 .45  0      - - error (invalid witness file) .60 .39 8.8 40 error (invalid witness file) 6.2 3.3 110 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 4.9 2.3 42 150 .23  .094  - - error (invalid witness file) .49 .31 6.4 39 error (invalid witness file) 6.1 3.2 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 4.7 2.2 38 150 .23  0      - - error (invalid witness file) .53 .34 5.2 39 error (invalid witness file) 6.0 3.2 110 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 52 220 .086 0      error (invalid witness file) .51 .33 9.8 42 error (invalid witness file) 6.0 3.2 120 290 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.4 2.5 46 220 .086 0      error (invalid witness file) .56 .35 13   40 error (invalid witness file) 5.4 2.9 110 280 - -
recursive-simple/fibo_10_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 5.7 2.7 45 220 .086 .094  error (invalid witness file) .54 .33 13   40 error (invalid witness file) 6.2 3.3 120 300 - -
recursive-simple/fibo_15_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 12   9.3 140 230 .086 0      error (invalid witness file) .52 .36 3.8 40 error (invalid witness file) 5.9 3.1 110 300 - -
recursive-simple/fibo_20_false-unreach-call.c unknown 0 wit inspect 720   720   5100 200 .36  0      error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.0 3.2 120 300 - -
recursive-simple/fibo_25_false-unreach-call.c unknown 0 wit inspect 4.6 2.2 40 150 .23  0      error (invalid witness file) .57 .36 5.3 43 error (invalid witness file) 6.9 3.6 140 320 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 5.7 2.7 46 220 .086 0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.4 3.4 130 300 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 12   9.2 130 230 .086 0      error (invalid witness file) .55 .35 5.2 43 error (invalid witness file) 5.8 3.1 130 300 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c unknown 0 wit inspect 720   720   6100 200 .35  0      error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.1 3.3 120 300 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c unknown 0 wit inspect 840   840   6600 200 .35  0      error (invalid witness file) .50 .33 4.9 41 error (invalid witness file) 6.2 3.3 100 300 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.7 2.5 49 230 .086 0      error (invalid witness file) .50 .33 13   39 error (invalid witness file) 5.4 2.9 95 290 - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.6 2.4 51 230 .086 0      error (invalid witness file) .54 .34 12   39 error (invalid witness file) 5.9 3.1 120 300 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 54 230 .086 0      error (invalid witness file) .53 .34 13   42 error (invalid witness file) 6.0 3.1 110 290 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 47 230 .086 0      error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.5 2.9 92 290 - -
recursive-simple/fibo_2calls_8_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 5.6 2.5 56 220 .086 0      error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.7 3.5 120 310 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 47 230 .086 .57   error (invalid witness file) .54 .35 5.9 42 error (invalid witness file) 6.0 3.3 120 310 - -
recursive-simple/fibo_7_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 54 230 .086 0      error (invalid witness file) .52 .33 12   41 error (invalid witness file) 5.7 3.1 130 290 - -
recursive-simple/id2_b3_o2_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 6.0 2.9 56 270 .086 0      error (invalid witness file) .52 .33 13   41 error (invalid witness file) 6.1 3.2 110 300 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 49 230 .086 0      error (invalid witness file) .51 .32 4.7 41 error (invalid witness file) 6.2 3.3 130 310 - -
recursive-simple/id_b3_o2_false-unreach-call.c unknown 0 wit inspect 4.7 2.3 42 160 .23  .094  error (invalid witness file) .48 .32 7.8 40 error (invalid witness file) 5.6 3.0 100 290 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 50 220 .086 0      error (invalid witness file) .56 .35 11   42 error (invalid witness file) 6.5 3.4 120 310 - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.7 2.5 51 230 .086 0      error (invalid witness file) .52 .33 8.9 41 error (invalid witness file) 6.0 3.2 120 300 - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.4 2.5 51 230 .086 0      error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.1 3.2 130 300 - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c unknown 0 wit inspect 4.7 2.2 39 150 .23  0      error (invalid witness file) .51 .35 10   39 error (invalid witness file) 6.0 3.2 110 300 - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.3 2.4 50 230 .086 0      error (invalid witness file) .47 .31 8.0 39 error (invalid witness file) 5.7 3.0 94 300 - -
recursive-simple/id_o1000_false-unreach-call.c unknown 0 wit inspect 4.6 2.2 41 160 .23  0      error (invalid witness file) .55 .36 12   39 error (invalid witness file) 6.6 3.5 130 300 - -
recursive-simple/id_o100_false-unreach-call.c unknown 0 wit inspect 4.7 2.2 40 150 .23  0      error (invalid witness file) .51 .35 6.4 39 error (invalid witness file) 6.3 3.3 120 300 - -
recursive-simple/id_o10_false-unreach-call.c unknown 0 wit inspect 4.9 2.3 42 160 .23  0      error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.2 3.2 120 300 - -
recursive-simple/id_o200_false-unreach-call.c unknown 0 wit inspect 4.8 2.3 49 150 .23  0      error (invalid witness file) .51 .33 8.5 39 error (invalid witness file) 6.7 3.5 130 320 - -
recursive-simple/id_o20_false-unreach-call.c unknown 0 wit inspect 4.7 2.2 44 160 .23  0      error (invalid witness file) .50 .31 4.1 40 error (invalid witness file) 5.5 2.9 110 280 - -
recursive-simple/id_o3_false-unreach-call.c unknown 0 wit inspect 4.6 2.2 43 160 .23  0      error (invalid witness file) .56 .35 13   41 error (invalid witness file) 6.1 3.2 90 300 - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.3 2.4 57 230 .086 0      error (invalid witness file) .48 .31 9.9 39 error (invalid witness file) 5.7 3.0 110 300 - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.4 2.5 44 230 .086 0      error (invalid witness file) .51 .35 5.1 40 error (invalid witness file) 5.6 3.0 120 290 - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 57 230 .086 0      error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.3 3.3 120 300 - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c unknown 0 wit inspect 4.9 2.2 40 150 .24  0      error (invalid witness file) .48 .31 6.0 40 error (invalid witness file) 6.0 3.2 98 300 - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.5 2.5 48 220 .086 0      error (invalid witness file) .49 .31 6.3 40 error (invalid witness file) 6.1 3.2 110 310 - -
recursive-simple/sum_non_eq_false-unreach-call.c witness invalid (false(unreach-call)) 0 wit inspect 5.8 2.6 46 280 .086 0      error (invalid witness file) .52 .33 9.7 40 error (invalid witness file) 5.5 3.0 120 290 - -
recursive-simple/sum_non_false-unreach-call_true-termination.c witness invalid (false(unreach-call)) 0 wit inspect 5.8 2.7 54 280 .086 0      error (invalid witness file) .50 .32 9.7 39 error (invalid witness file) 6.1 3.2 130 290 - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 7.3 2.4 53 290 .045 0      - - true 3.5  1.9  60   260 true 7.4 4.0 110 320
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 6.8 2.3 55 290 .045 0      - - true 3.5  2.0  84   260 true 7.7 4.2 170 320
recursive-simple/fibo_10_true-unreach-call.c true 2 wit inspect 7.5 2.5 61 290 .045 0      - - error (recursion) 3.4  1.9  76   250 true 45   26   870 3000
recursive-simple/fibo_15_true-unreach-call.c true 2 wit inspect 9.8 4.6 95 290 .045 0      - - error (recursion) 3.5  2.0  78   260 true 600   550   8500 6300
recursive-simple/fibo_20_true-unreach-call.c unknown 0 wit inspect 720   730   5400 200 .36  0      - - error (invalid witness file) .54 .34 14   40 error (invalid witness file) 5.9 3.1 120 310
recursive-simple/fibo_25_true-unreach-call.c unknown 0 wit inspect 4.7 2.2 43 150 .23  0      - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 5.7 3.0 110 290
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 7.6 2.5 56 300 .045 0      - - error (recursion) 3.6  2.0  82   260 true 86   53   2100 4500
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 10   4.8 88 290 .045 0      - - error (recursion) 3.6  2.0  71   250 timeout 960   900   24000 5400
recursive-simple/fibo_2calls_20_true-unreach-call.c unknown 0 wit inspect 720   720   5900 200 .37  0      - - error (invalid witness file) .49 .31 7.0 41 error (invalid witness file) 5.7 3.0 100 280
recursive-simple/fibo_2calls_25_true-unreach-call.c unknown 0 wit inspect 840   850   6700 200 .30  0      - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.8 3.1 120 300
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 7.2 2.3 54 290 .045 0      - - true 3.5  2.0  73   260 true 12   6.5 240 370
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 8.1 2.5 71 320 .045 0      - - error (recursion) 3.6  2.0  67   260 true 20   11   420 530
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 7.4 2.4 64 300 .045 0      - - error (recursion) 3.8  2.1  75   260 true 26   14   500 660
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 7.9 2.5 63 290 .045 0      - - error (recursion) 3.5  1.9  49   260 true 33   19   680 780
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 7.9 2.5 61 290 .045 .10   - - error (recursion) 3.5  1.9  53   260 true 48   28   880 1200
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 7.8 2.5 65 290 .045 0      - - error (recursion) 3.6  2.0  57   250 true 17   9.2 310 530
recursive-simple/fibo_7_true-unreach-call.c true 2 wit inspect 7.8 2.4 59 290 .045 0      - - error (recursion) 3.6  2.0  82   260 true 22   12   460 570
recursive-simple/id2_b2_o3_true-unreach-call.c unknown 0 wit inspect 5.1 2.6 48 150 .25  0      - - error (invalid witness file) .50 .33 3.8 40 error (invalid witness file) 5.7 3.1 110 300
recursive-simple/id2_b3_o5_true-unreach-call.c unknown 0 wit inspect 5.2 2.7 52 150 .25  0      - - error (invalid witness file) .56 .37 11   43 error (invalid witness file) 6.4 3.3 140 310
recursive-simple/id2_b5_o10_true-unreach-call.c unknown 0 wit inspect 5.2 2.7 51 150 .25  0      - - error (invalid witness file) .62 .40 8.7 43 error (invalid witness file) 6.1 3.3 130 300
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 7.6 2.4 54 290 .045 0      - - error (recursion) 3.5  1.9  72   260 true 16   8.7 360 520
recursive-simple/id_b2_o3_true-unreach-call.c unknown 0 wit inspect 5.0 2.4 43 150 .23  0      - - error (invalid witness file) .51 .32 8.5 39 error (invalid witness file) 6.3 3.3 140 300
recursive-simple/id_b3_o5_true-unreach-call.c unknown 0 wit inspect 5.0 2.4 45 150 .23  0      - - error (invalid witness file) .52 .33 12   42 error (invalid witness file) 5.8 3.1 120 290
recursive-simple/id_b5_o10_true-unreach-call.c unknown 0 wit inspect 4.9 2.4 49 150 .23  0      - - error (invalid witness file) .51 .32 7.2 40 error (invalid witness file) 5.4 2.9 100 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 7.6 2.5 64 300 .045 0      - - error (recursion) 3.5  2.0  74   250 true 18   10   350 540
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 7.5 2.4 61 290 .045 .0082 - - error (recursion) 3.6  2.0  74   260 true 24   14   500 620
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 8.0 2.6 70 290 .045 0      - - error (recursion) 3.5  2.0  69   250 true 32   19   620 730
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c unknown 0 wit inspect 4.9 2.3 46 160 .23  0      - - error (invalid witness file) .49 .32 12   43 error (invalid witness file) 5.8 3.1 92 300
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 7.4 2.4 65 290 .045 0      - - error (recursion) 3.5  2.0  64   260 true 11   6.3 200 380
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 7.7 2.5 69 290 .045 0      - - error (recursion) 3.5  2.0  62   260 true 20   12   440 580
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 7.6 2.4 61 300 .045 0      - - error (recursion) 3.4  1.9  49   260 true 27   16   590 660
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 7.9 2.5 61 290 .045 0      - - error (recursion) 3.4  1.9  61   260 true 39   23   690 720
recursive-simple/sum_25x0_true-unreach-call_true-termination.c unknown 0 wit inspect 4.6 2.2 45 160 .24  0      - - error (invalid witness file) .51 .34 6.5 40 error (invalid witness file) 5.6 3.0 100 290
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 7.4 2.4 59 290 .045 0      - - error (recursion) 3.6  2.0  81   260 true 11   6.2 230 400
recursive-simple/sum_non_eq_true-unreach-call.c unknown 0 wit inspect 4.7 2.3 43 150 .23  .094  - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.0 3.1 120 300
recursive-simple/sum_non_true-unreach-call_true-termination.c unknown 0 wit inspect 4.9 2.5 48 160 .24  0      - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.5 3.0 100 300
../../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 45 19000 19000   130000 57000 27     1.9  98 23 15 420 1800   98 270 140 5200 13000   98 97   56   1800 7100 98 2300 1900 48000 40000
    correct results 22 44 170 56   1400 6500 .99  .11 0 0 0 0 0   0 0 0 0 0   3 77   44   1500 5700 22 1200 870 20000 25000
        correct true 22 44 170 56   1400 6500 .99  .11 0 0 0 0 0   0 0 0 0 0   3 77   44   1500 5700 22 1200 870 20000 25000
        correct false 0
    correct-unconfimed results 1 1 10 4.8 88 290 .045 0    0 0 0 0 0   0 0 0 0 0   0 3.6 2.0 71 250 0 960 900 24000 5400
        correct-unconfirmed true 1 1 10 4.8 88 290 .045 0    0 0 0 0 0   0 0 0 0 0   0 3.6 2.0 71 250 0 960 900 24000 5400
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 45
Run set sv-comp17.ReachSafety-Recursive