Tool VerifierIntegerAssignmentPrograms 1.1.12(Date 28/11/2018) 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-09 18:49:43 CET 2018-12-09 21:23:04 CET 2018-12-09 22:02:00 CET 2018-12-09 22:04:11 CET 2018-12-12 22:08:25 CET 2018-12-09 21:05:40 CET 2018-12-09 21:25:32 CET
Run set viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive
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/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.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/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/viap.2018-12-09_1849.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/viap.2018-12-09_1849.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)
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.7 2.7 130 35 .33 1.2    false(unreach-call) 1 wit inspect 4.1 2.2 260 0   .029  false(unreach-call) 1 --- inspect 7.8 4.8 310 .66 0      unknown 0 --- inspect 3.7 2.2 250 0      0      true -32 --- inspect .60 .60 20 .049 0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 37 .30 .0041 false(unreach-call) 1 wit inspect 4.8 2.6 270 0   0      false(unreach-call) 1 --- inspect 12   6.8 480 .62 0      unknown 0 --- inspect 3.8 2.2 240 0      0      true -32 --- inspect .58 .58 21 .049 0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 2.6 2.6 130 34 .29 .11   true -32 wit inspect 3.6 2.0 250 0   0      true -32 --- inspect 6.2 3.5 300 .66 0      unknown 0 --- inspect 3.5 2.0 250 0      0      true -32 --- inspect .62 .62 20 .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 33 .30 0      false(unreach-call) 1 wit inspect 3.7 2.1 250 0   0      false(unreach-call) 1 --- inspect 6.9 3.9 300 .66 0      unknown 0 --- inspect 3.6 2.1 240 0      0      false(unreach-call) 1 --- inspect .60 .60 20 .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 34 .29 1.2    false(unreach-call) 1 wit inspect 4.5 2.5 270 0   0      false(unreach-call) 1 --- inspect 26   14   800 .66 0      unknown 0 --- inspect 3.9 2.3 250 0      0      true -32 --- inspect .58 .60 21 .049 0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 40 .29 .54   false(unreach-call) 1 wit inspect 6.7 3.6 300 0   0      timeout 0 --- inspect 98   70   5000 1.5  .0041 unknown 0 --- inspect 4.9 2.7 260 0      0      true -32 --- inspect .59 .59 22 .049 0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 34 .29 0      false(unreach-call) 1 wit inspect 3.6 2.0 250 0   0      false(unreach-call) 1 --- inspect 6.8 3.8 300 .66 0      unknown 0 --- inspect 3.6 2.1 250 0      0      true -32 --- inspect .59 .59 20 .049 .0041 - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 110   110   330 1300 .45 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0      error (2) 0 --- inspect .039 .039 5.5 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 110   110   690 1100 .39 1.2    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 42 0   0      error (2) 0 --- inspect .023 .034 5.5 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 --- inspect 110   110   830 910 .39 2.3    - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 110   110   310 1600 .39 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 42 0   0      error (2) 0 --- inspect .046 .052 5.7 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 57   57   310 690 .57 2.7    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 410     320     2200   .62 .0041
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 56   56   190 660 .63 2.7    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0      timeout 0 --- inspect 960     810     1300   .63 .0041
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 2 wit inspect 36   36   210 530 .59 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 14     8.7   460   .62 0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.2 4.2 130 59 .52 1.9    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  260 0   0      true 2 --- inspect 37     23     1700   .66 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 19   19   230 250 .65 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  260 0   0      true 2 --- inspect 28     16     820   .62 0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 6.8 6.9 130 89 .57 1.9    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.0  250 0   0      true 2 --- inspect 9.7   6.0   330   .62 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 78   78   220 1000 .67 2.2    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0      timeout 0 --- inspect 960     820     1100   .63 0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 --- inspect 4.4 4.4 130 60 .31 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0      error (2) 0 --- inspect .045 .046 5.4 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 12   12   150 190 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 10     6.3   360   .62 0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 110   110   730 1400 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      timeout 0 --- inspect 960     820     890   .63 0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect 4.7 4.7 130 70 .46 .27   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .025 .037 5.5 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.7 5.7 130 78 .63 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 6.9   4.0   310   .62 0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.9 5.9 130 77 .63 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   .0041 true 2 --- inspect 12     7.6   460   .62 0     
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 31 .29 0      true -32 wit inspect 3.5 1.9 250 0   0      false(unreach-call) 1 --- inspect 6.9 4.3 300 .66 0      false(unreach-call) 1 --- inspect 3.4 2.0 240 0      .0041 false(unreach-call) 1 --- inspect .59 .59 20 .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 34 .29 .58   true -32 wit inspect 3.4 1.9 250 0   0      false(unreach-call) 1 --- inspect 6.2 4.0 290 .66 0      false(unreach-call) 1 --- inspect 3.7 2.1 250 0      0      false(unreach-call) 1 --- inspect .57 .57 20 .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 2.7 130 41 .29 .11   false(unreach-call) 1 wit inspect 9.2 5.0 410 0   0      timeout 0 --- inspect 96   64   5200 1.4  0      false(unreach-call) 1 --- inspect 5.3 2.9 260 0      0      false(unreach-call) 1 --- inspect .63 .63 25 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect 5.0 5.0 420 54 .29 .28   false(unreach-call) 1 wit inspect 40   23   1500 0   0      timeout 0 --- inspect 97   64   7000 .63 0      false(unreach-call) 1 --- inspect 17   8.9 470 0      0      false(unreach-call) 1 --- inspect 1.2  1.3  77 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect 29   29   4000 240 .29 0      timeout 0 --- inspect 96   67   2600 0   0      out of memory 0 --- inspect 88   56   7000 .66 0      timeout 0 --- inspect 97   77   2500 0      0      false(unreach-call) 1 --- inspect 8.1  8.1  680 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6 5.6 1200 86 .29 .16   timeout 0 --- inspect 98   65   4000 0   .0041 true -32 --- inspect 7.4 4.2 310 .62 0      false(unreach-call) 1 --- inspect 3.4 2.0 240 0      0      false(unreach-call) 1 --- inspect .59 .59 20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect 2.8 2.8 130 36 .30 0      false(unreach-call) 1 wit inspect 8.4 4.6 370 0   0      timeout 0 --- inspect 98   64   6000 1.5  0      false(unreach-call) 1 --- inspect 5.1 2.9 260 0      0      false(unreach-call) 1 --- inspect .65 .66 25 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect 5.0 5.0 420 52 .30 .11   false(unreach-call) 1 wit inspect 29   18   1300 0   0      out of memory 0 --- inspect 76   49   7000 .70 .0041 false(unreach-call) 1 --- inspect 13   6.9 350 0      0      false(unreach-call) 1 --- inspect 1.2  1.2  77 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect 29   29   4000 280 .30 1.3    out of memory 0 --- inspect 82   53   7000 0   0      timeout 0 --- inspect 94   54   7000 1.5  0      timeout 0 --- inspect 97   79   2400 .020  0      false(unreach-call) 1 --- inspect 8.2  8.2  680 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect 5.7 5.6 1200 75 .30 .11   timeout 0 --- inspect 97   61   4000 0   .012  true -32 --- inspect 7.5 4.3 310 .66 0      false(unreach-call) 1 --- inspect 3.5 2.1 250 0      0      false(unreach-call) 1 --- inspect .60 .60 20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 34 .30 .73   false(unreach-call) 1 wit inspect 3.6 2.0 250 0   0      false(unreach-call) 1 --- inspect 7.3 4.5 310 .66 0      false(unreach-call) 1 --- inspect 3.9 2.2 250 0      0      false(unreach-call) 1 --- inspect .59 .59 20 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 37 .30 0      false(unreach-call) 1 wit inspect 4.3 2.4 260 0   0      false(unreach-call) 1 --- inspect 14   8.5 460 .66 0      false(unreach-call) 1 --- inspect 3.6 2.1 250 0      0      false(unreach-call) 1 --- inspect .63 .65 21 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 33 .30 .11   false(unreach-call) 1 wit inspect 4.6 2.5 270 0   0      false(unreach-call) 1 --- inspect 30   16   890 .62 0      false(unreach-call) 1 --- inspect 3.8 2.2 250 0      0      false(unreach-call) 1 --- inspect .63 .65 21 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 35 .30 0      false(unreach-call) 1 wit inspect 4.9 2.7 270 0   0      false(unreach-call) 1 --- inspect 47   26   2000 .62 0      false(unreach-call) 1 --- inspect 3.9 2.2 250 0      0      false(unreach-call) 1 --- inspect .59 .58 21 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 32 .30 .36   false(unreach-call) 1 wit inspect 6.2 3.3 300 0   0      timeout 0 --- inspect 97   67   4800 1.5  .0041 false(unreach-call) 1 --- inspect 4.8 2.6 260 0      0      false(unreach-call) 1 --- inspect .59 .59 22 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 35 .29 0      false(unreach-call) 1 wit inspect 4.7 2.6 270 0   0      false(unreach-call) 1 --- inspect 21   12   760 .66 0      false(unreach-call) 1 --- inspect 3.7 2.2 240 0      0      false(unreach-call) 1 --- inspect .57 .57 21 .049 0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 37 .29 .11   false(unreach-call) 1 wit inspect 5.7 3.1 280 0   .12   timeout 0 --- inspect 96   67   3500 .66 0      false(unreach-call) 1 --- inspect 4.3 2.4 250 0      0      false(unreach-call) 1 --- inspect .59 .59 22 .049 0      - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.7 2.7 130 38 .31 .25   false(unreach-call) 1 wit inspect 4.1 2.3 260 0   0      true -32 --- inspect 7.4 4.6 310 .66 0      unknown 0 --- inspect 3.5 2.0 240 0      0      true -32 --- inspect .63 .64 20 .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 34 .29 0      false(unreach-call) 1 wit inspect 3.9 2.2 260 0   0      false(unreach-call) 1 --- inspect 7.0 4.0 300 .66 0      false(unreach-call) 1 --- inspect 3.5 2.0 240 0      0      false(unreach-call) 1 --- inspect .61 .61 20 .049 0      - --- inspect - --- inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.6 2.6 130 32 .30 0      false(unreach-call) 1 wit inspect 4.0 2.2 260 0   0      true -32 --- inspect 7.5 4.5 310 .66 0      unknown 0 --- inspect 3.5 2.1 250 0      0      true -32 --- inspect .58 .58 20 .049 0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 33 .29 0      false(unreach-call) 1 wit inspect 4.4 2.4 270 0   0      false(unreach-call) 1 --- inspect 8.6 5.2 350 .66 0      false(unreach-call) 1 --- inspect 3.8 2.2 250 0      0      false(unreach-call) 1 --- inspect .60 .61 20 .045 .0041 - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 31 .29 0      false(unreach-call) 1 wit inspect 4.9 2.7 270 0   0      false(unreach-call) 1 --- inspect 12   6.9 520 .66 0      false(unreach-call) 1 --- inspect 4.0 2.3 250 0      0      false(unreach-call) 1 --- inspect .59 .59 22 .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 37 .29 .73   false(unreach-call) 1 wit inspect 5.3 2.8 270 0   0      false(unreach-call) 1 --- inspect 16   8.4 750 .66 .0041 false(unreach-call) 1 --- inspect 4.2 2.4 250 0      0      false(unreach-call) 1 --- inspect .58 .58 21 .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 35 .29 .33   false(unreach-call) 1 wit inspect 5.8 3.2 270 0   0      false(unreach-call) 1 --- inspect 21   12   830 .62 0      false(unreach-call) 1 --- inspect 4.5 2.6 250 0      0      false(unreach-call) 1 --- inspect .61 .62 21 .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 36 .29 .73   false(unreach-call) 1 wit inspect 4.4 2.4 260 0   0      false(unreach-call) 1 --- inspect 7.5 4.2 300 .66 0      false(unreach-call) 1 --- inspect 3.7 2.2 250 0      0      false(unreach-call) 1 --- inspect .59 .59 20 .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 0 wit inspect 3.6 3.7 200 41 .32 .95   exception 0 --- inspect 6.8 3.6 270 0   0      out of memory 0 --- inspect 89   63   7000 .63 0      timeout 0 --- inspect 6.3 130   260 .84   .0041 true -32 --- inspect .83 .83 41 .049 0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.7 2.7 130 35 .32 1.1    false(unreach-call) 1 wit inspect 16   8.2 510 0   0      timeout 0 --- inspect 96   63   7000 .66 0      unknown 0 --- inspect 9.2 5.0 370 0      0      true -32 --- inspect .61 .61 22 .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.7 2.7 130 32 .32 .25   false(unreach-call) 1 wit inspect 4.8 2.6 270 0   0      false(unreach-call) 1 --- inspect 9.7 5.2 370 .66 0      unknown 0 --- inspect 3.9 2.3 250 0      0      true -32 --- inspect .60 .60 21 .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.8 2.8 130 34 .32 .28   false(unreach-call) 1 wit inspect 32   21   1100 0   0      timeout 0 --- inspect 98   65   6200 .66 0      unknown 0 --- inspect 16   8.7 490 0      0      true -32 --- inspect .62 .62 24 .049 0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.7 2.7 130 34 .32 .11   false(unreach-call) 1 wit inspect 5.3 2.9 270 0   0      false(unreach-call) 1 --- inspect 16   8.7 760 .66 0      unknown 0 --- inspect 4.2 2.4 250 0      0      true -32 --- inspect .61 .64 21 .049 .0041 - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.7 2.7 130 35 .32 0      false(unreach-call) 1 wit inspect 3.9 2.2 260 0   0      false(unreach-call) 1 --- inspect 7.1 4.0 300 .66 0      unknown 0 --- inspect 3.5 2.1 250 0      0      true -32 --- inspect .57 .57 20 .049 .0041 - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 40 .29 0      false(unreach-call) 1 wit inspect 4.5 2.5 270 0   .016  false(unreach-call) 1 --- inspect 8.2 5.1 320 .66 0      false(unreach-call) 1 --- inspect 3.8 2.2 250 0      0      false(unreach-call) 1 --- inspect .59 .60 21 .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 30 .29 .40   false(unreach-call) 1 wit inspect 5.0 2.7 270 0   0      false(unreach-call) 1 --- inspect 11   6.6 520 .66 0      false(unreach-call) 1 --- inspect 4.3 2.5 250 0      0      false(unreach-call) 1 --- inspect .59 .59 21 .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 32 .29 0      false(unreach-call) 1 wit inspect 5.4 2.9 280 0   .0041 false(unreach-call) 1 --- inspect 15   8.5 630 .66 0      false(unreach-call) 1 --- inspect 4.0 2.3 250 0      0      false(unreach-call) 1 --- inspect .57 .57 21 .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 40 .29 .11   false(unreach-call) 1 wit inspect 5.6 3.1 280 0   0      false(unreach-call) 1 --- inspect 17   9.9 780 .62 0      false(unreach-call) 1 --- inspect 4.2 2.4 250 0      0      false(unreach-call) 1 --- inspect .57 .57 21 .045 0      - --- inspect - --- inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 2.6 130 29 .29 .74   false(unreach-call) 1 wit inspect 3.8 2.1 260 0   0      false(unreach-call) 1 --- inspect 7.7 4.4 310 .66 0      false(unreach-call) 1 --- inspect 3.9 2.3 250 0      0      false(unreach-call) 1 --- inspect .59 .62 20 .045 .0041 - --- inspect - --- inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 2.9 2.9 130 36 .29 .11   exception 0 --- inspect 6.4 3.5 270 0   0      timeout 0 --- inspect 97   64   6600 .66 0      timeout 0 --- inspect 5.6 130   260 .0041 0      false(unreach-call) 1 --- inspect .67 .67 30 .049 0      - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 3.8 3.8 130 47 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 7.2   4.1   310   .62 0     
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 3.7 3.7 130 55 .52 .11   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   .0041 true 2 --- inspect 6.7   4.3   310   .62 0     
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 190 110 .52 .24   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  1.9  250 0   0      true 2 --- inspect 38     24     2200   .62 0     
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect 8.1 8.1 190 110 .52 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      timeout 0 --- inspect 960     890     6000   1.0  0     
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect 13   13   200 180 .52 1.7    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      out of memory 0 --- inspect 700     650     7000   .63 0     
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect 15   15   210 190 .52 1.1    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.0  250 0   0      timeout 0 --- inspect 900     850     7000   .63 0     
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect 8.2 8.2 190 120 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.2  250 0   0      true 2 --- inspect 85     55     3800   .62 0     
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect 8.3 8.3 200 110 .53 .25   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0      timeout 0 --- inspect 960     900     5400   1.0  0     
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect 10   10   200 130 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      timeout 0 --- inspect 960     900     5300   1.0  0     
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect 6.9 7.0 200 81 .53 1.9    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      out of memory 0 --- inspect 580     530     7000   .63 0     
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect 7.0 7.0 170 84 .53 .25   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 11     6.8   390   .62 0     
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 190 120 .53 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.1  250 0   0      true 2 --- inspect 15     9.7   540   .62 0     
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 190 120 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 21     13     510   .62 0     
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect 8.3 8.3 190 100 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 26     16     700   .62 0     
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 190 99 .53 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.0  2.2  260 0   0      true 2 --- inspect 50     32     1300   .62 0     
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect 8.1 8.1 190 92 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 16     9.6   580   .62 .0041
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect 8.0 8.0 190 110 .52 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 21     13     550   .62 0     
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.0 9.0 200 110 .84 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 12     7.5   460   .10 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.8 8.9 200 110 .84 2.6    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 13     8.2   460   .62 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.0 9.0 200 110 .84 1.9    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   .0041 true 2 --- inspect 13     8.3   520   .62 0     
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 6.9 6.9 160 87 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 14     8.6   500   .62 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.0 9.0 200 120 .79 3.0    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 11     6.9   380   .62 0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.0 7.0 150 90 .79 .049  - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 8.5   4.8   320   .62 0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.9 6.9 150 100 .79 .21   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 7.8   4.9   310   .62 0     
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 8.2 8.2 200 100 .52 2.2    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 16     9.9   480   .62 0     
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 8.9 8.9 200 130 .52 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  260 0   0      true 2 --- inspect 21     13     630   .62 0     
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 9.7 9.7 200 140 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 28     17     700   .62 0     
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 11   11   200 160 .52 .11   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 35     23     730   .62 0     
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 6.8 6.8 160 98 .52 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.4  250 0   .0041 true 2 --- inspect 11     6.9   440   .62 0     
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect 6.7 6.7 210 78 .52 .19   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 19     12     490   .62 0     
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect 7.0 7.1 210 84 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 26     16     650   .62 .0041
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect 55   55   300 600 .52 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 35     22     580   .62 0     
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect 55   55   300 690 .52 .32   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.9  2.1  250 0   .0041 true 2 --- inspect 49     32     690   .62 0     
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect 5.2 5.2 130 59 .52 .18   - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 11     6.4   380   .62 0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 81   81   220 950 .53 1.9    - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 10     6.1   340   .62 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 96 124 1500   1500   28000 18000 42    47   44 -61 670 410   32000 0   .18 44 -134 1600 1000 95000 33   .016  44 26 400 520 16000 .86 .0082 44 -418 43   43   2400 2.1  .025  52 6 170 95   12000 0   .020  52 74 9100 8000 68000 29 .016
    correct results 79 116 710   710   23000 8900 34    32   35 35 270 150   13000 0   .17 26 26 360 200 14000 17   .0041 26 26 130 71 6800 0    .0041 30 30 34   34   2100 1.4  .0082 3 6 11 5.9 750 0   .0041 37 74 1200 790 27000 23 .012
        correct true 37 74 540   540   7000 6800 22    20   0 0 0 0 3 6 11 5.9 750 0   .0041 37 74 1200 790 27000 23 .012
        correct false 42 42 170   170   16000 2000 12    12   35 35 270 150   13000 0   .17 26 26 360 200 14000 17   .0041 26 26 130 71 6800 0    .0041 30 30 34   34   2100 1.4  .0082 0 0
    correct-unconfimed results 10 8 200   200   1900 2600 5.0  11   0 0 0 0 0 0
        correct-unconfirmed true 8 8 200   200   1600 2500 4.4  10   0 0 0 0 0 0
        correct-unconfirmed false 2 0 6.2 6.3 330 75 .61 1.1 0 0 0 0 0 0
    incorrect results 0 3 -96 10 5.9 750 0   0    5 -160 36 21 1500 3.2 0      0 14 -448 8.6 8.7 310 .69 .016  0 0
        incorrect true 0 3 -96 10 5.9 750 0   0    5 -160 36 21 1500 3.2 0      0 14 -448 8.6 8.7 310 .69 .016  0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 124 -61 -134 26 -418 6 74
Run set viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-viap.sv-comp19_prop-reachsafety.ReachSafety-Recursive