Tool 2LS 0.7.2-sv-comp19 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-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 06:59:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options --graphml-witness witness.graphml -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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 0 .099 .097 24 .69 0   0   0 .62 .39 40 0   0   0 .023 .023 5.6 0   0   0 .99 .64 47 0   0   0 .0056 .0067 .54 0   0   - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 0 .085 .083 24 .85 0   0   0 .61 .37 42 0   0   0 .021 .023 5.6 0   0   0 .96 .62 46 0   0   0 .0052 .0062 .53 0   0   - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 .082 .083 24 1.0  0   0   0 .58 .36 40 0   0   0 .020 .021 5.6 0   0   0 .92 .61 47 0   0   0 .0021 .0025 .40 0   0   - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 0 .087 .089 24 .76 0   0   0 .61 .37 41 0   0   0 .023 .023 5.6 0   0   0 .99 .63 48 0   0   0 .0051 .0067 .53 0   0   - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 .085 .086 24 .83 0   0   0 .78 .47 41 0   0   0 .022 .022 5.6 0   0   0 .93 .62 47 0   0   0 .0048 .0060 .53 0   0   - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 .090 .090 23 .73 0   0   0 .61 .38 41 0   0   0 .049 .050 5.5 0   0   0 .96 .64 49 0   0   0 .0014 .0020 .54 0   0   - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 .086 .085 24 .74 0   0   0 .76 .46 40 0   0   0 .024 .025 5.5 0   0   0 .99 .65 48 0   0   0 .0026 .0036 .53 0   0   - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 .12  .11  23 .68 0   0   - - - - 0 .60 .37 40 0   0   0 .024 .025 5.6 0   0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 .085 .085 24 .84 0   0   - - - - 0 .61 .38 40 0   0   0 .021 .022 5.6 0   0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 .089 .089 24 .93 0   0   - - - - 0 .65 .40 42 0   0   0 .027 .028 5.6 0   0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 .099 .099 24 .74 0   0   - - - - 0 .76 .46 40 0   0   0 .023 .025 5.7 0   0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 .093 .093 24 .78 0   0   - - - - 0 .64 .40 41 0   0   0 .021 .023 5.6 0   0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 .098 .099 24 .80 0   0   - - - - 0 .59 .36 41 0   0   0 .021 .022 5.6 0   0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 .086 .085 24 .95 0   0   - - - - 0 .69 .42 40 0   0   0 .023 .024 5.6 0   0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 .14  .14  23 .73 0   0   - - - - 0 .72 .44 41 0   0   0 .054 .055 5.5 0   0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 .084 .084 24 .98 0   0   - - - - 0 .67 .40 41 0   0   0 .029 .030 5.6 0   0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 .12  .12  24 .68 0   0   - - - - 0 .75 .45 42 0   0   0 .021 .022 5.6 0   0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 .085 .086 24 .86 0   0   - - - - 0 .76 .46 41 0   0   0 .023 .024 5.7 0   0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 .11  .12  24 .62 0   0   - - - - 0 .61 .38 41 0   0   0 .021 .022 5.6 0   0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 .084 .084 24 .86 0   0   - - - - 0 .74 .46 40 0   0   0 .022 .024 5.7 0   0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 .087 .091 24 .73 0   0   - - - - 0 .68 .42 40 0   0   0 .021 .023 5.6 0   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 .086 .087 24 1.0  0   0   - - - - 0 .76 .47 40 0   0   0 .023 .024 5.6 0   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 .11  .11  24 .75 0   0   - - - - 0 .75 .47 41 0   0   0 .020 .021 5.6 0   0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 .091 .092 24 .91 0   0   - - - - 0 .63 .39 41 0   0   0 .022 .023 5.7 0   0  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 0 .12  .12  24 .70 0   0   0 .69 .42 42 0   0   0 .054 .056 5.5 0   0   0 .96 .63 47 0   0   0 .0048 .0080 .52 0   0   - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 0 .086 .086 24 .78 0   0   0 .60 .37 40 0   0   0 .023 .023 5.6 0   0   0 .95 .63 47 0   0   0 .0016 .0042 .49 0   0   - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 0 .083 .083 24 .89 0   0   0 .75 .46 41 0   0   0 .022 .023 5.7 0   0   0 .95 .61 47 0   0   0 .0047 .0059 .52 0   0   - -
recursive-simple/fibo_15_false-unreach-call.c 0 .090 .090 24 .77 0   0   0 .68 .43 41 0   0   0 .021 .022 5.7 0   0   0 .97 .62 47 0   0   0 .0061 .0077 .53 0   0   - -
recursive-simple/fibo_20_false-unreach-call.c 0 .088 .089 24 .72 0   0   0 .59 .37 40 0   0   0 .027 .027 5.5 0   0   0 .95 .63 48 0   0   0 .0052 .0062 .53 0   0   - -
recursive-simple/fibo_25_false-unreach-call.c 0 .088 .088 24 .90 0   0   0 .60 .38 41 0   0   0 .022 .025 5.8 0   0   0 .98 .64 48 0   0   0 .0018 .0025 .53 0   0   - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 .090 .090 24 .78 0   0   0 .58 .35 40 0   0   0 .024 .024 5.6 0   0   0 1.0  .67 48 0   0   0 .0018 .0024 .52 0   0   - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 .090 .089 24 .69 0   0   0 .62 .39 40 0   0   0 .020 .021 5.7 0   0   0 .96 .63 47 0   0   0 .0051 .0059 .39 0   0   - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 .13  .13  24 .75 0   0   0 .69 .43 42 0   0   0 .022 .024 5.6 0   0   0 .95 .61 49 0   0   0 .0060 .0076 .52 0   0   - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 .10  .10  24 .69 0   0   0 .77 .47 42 0   0   0 .023 .024 5.6 0   0   0 .98 .66 47 0   0   0 .0058 .0075 .52 0   0   - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 0 .094 .094 24 .70 0   0   0 .63 .37 41 0   0   0 .022 .023 5.6 0   0   0 .93 .62 47 0   0   0 .0016 .0023 .53 0   0   - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 0 .090 .090 24 .93 0   0   0 .77 .47 41 0   0   0 .023 .024 5.6 0   0   0 .96 .63 47 0   0   0 .0021 .0027 .53 0   0   - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 0 .088 .088 24 .97 0   0   0 .76 .45 41 0   0   0 .021 .022 5.6 0   0   0 .93 .61 47 0   0   0 .0054 .0069 .52 0   0   - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 0 .13  .13  24 .72 0   0   0 .68 .41 41 0   0   0 .026 .027 5.7 0   0   0 .96 .61 47 0   0   0 .0049 .0065 .53 0   0   - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 0 .12  .12  24 .84 0   0   0 .61 .37 41 0   0   0 .021 .023 5.8 0   0   0 .97 .63 47 0   0   0 .0017 .0023 .41 0   0   - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 0 .082 .081 24 .78 0   0   0 .78 .49 42 0   0   0 .023 .024 5.7 0   0   0 .97 .64 47 0   0   0 .0016 .0022 .53 0   0   - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 0 .12  .12  24 .73 0   0   0 .74 .45 41 0   0   0 .026 .027 5.6 0   0   0 .98 .64 48 0   0   0 .0047 .0057 .52 0   0   - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 .087 .086 24 .85 0   0   0 .71 .44 40 0   0   0 .023 .025 5.6 0   0   0 .94 .61 46 0   0   0 .0050 .0069 .54 0   0   - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 0 .094 .092 24 .74 0   0   0 .70 .44 40 0   0   0 .021 .022 5.6 0   0   0 .96 .63 47 0   0   0 .0048 .0054 .40 0   0   - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 .084 .083 24 .80 0   0   0 .63 .39 41 0   0   0 .024 .026 5.8 0   0   0 .97 .63 47 0   0   0 .0046 .0056 .54 0   0   - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 0 .081 .079 24 .85 0   0   0 .68 .41 42 0   0   0 .023 .024 5.6 0   0   0 .92 .60 47 0   0   0 .0067 .0093 .53 0   0   - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 0 .11  .11  24 .65 0   0   0 .62 .39 41 0   0   0 .024 .026 5.6 0   0   0 .97 .62 48 0   0   0 .0047 .0059 .52 0   0   - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 0 .088 .086 24 .78 0   0   0 .75 .46 41 0   0   0 .022 .022 5.6 0   0   0 .96 .63 48 0   0   0 .0019 .0024 .53 0   0   - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 0 .13  .13  24 .69 0   0   0 .76 .47 41 0   0   0 .021 .022 5.6 0   0   0 .97 .63 47 0   0   0 .0063 .0078 .52 0   0   - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 0 .088 .087 24 .69 0   0   0 .70 .43 40 0   0   0 .047 .049 5.5 0   0   0 .95 .62 47 0   0   0 .0057 .0073 .40 0   0   - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 .086 .084 24 .76 0   0   0 .76 .47 40 0   0   0 .024 .025 5.6 0   0   0 .94 .61 47 0   0   0 .0019 .0026 .54 0   0   - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 0 .093 .095 24 .80 0   0   0 .63 .38 40 0   0   0 .022 .023 5.6 0   0   0 .98 .68 46 0   0   0 .0054 .0068 .40 0   0   - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 0 .083 .084 24 .89 0   0   0 .61 .37 40 0   0   0 .022 .022 5.6 0   0   0 .96 .63 47 0   0   0 .0022 .0028 .52 0   0   - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 0 .089 .088 24 .98 0   0   0 .59 .36 40 0   0   0 .021 .022 5.6 0   0   0 .96 .61 47 0   0   0 .0053 .0068 .40 0   0   - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 0 .082 .083 24 .79 0   0   0 .61 .36 41 0   0   0 .022 .023 5.6 0   0   0 .99 .71 48 0   0   0 .0016 .0022 .52 0   0   - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 0 .11  .11  24 .73 0   0   0 .65 .39 43 0   0   0 .022 .023 5.6 0   0   0 .95 .61 47 0   0   0 .0015 .0025 .53 0   0   - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 0 .087 .087 24 .86 0   0   0 .63 .40 41 0   0   0 .022 .023 5.6 0   0   0 .96 .63 47 0   0   0 .0054 .0088 .53 0   0   - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 0 .082 .083 24 .88 0   0   0 .76 .46 42 0   0   0 .022 .022 5.7 0   0   0 .93 .61 48 0   0   0 .0015 .0025 .52 0   0   - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 0 .091 .090 24 .79 0   0   0 .65 .40 40 0   0   0 .021 .023 5.6 0   0   0 .98 .63 48 0   0   0 .0044 .0049 .40 0   0   - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 0 .11  .11  24 .68 0   0   0 .60 .38 42 0   0   0 .021 .023 5.6 0   0   0 .96 .63 47 0   0   0 .0052 .0063 .53 0   0   - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 0 .083 .082 24 .77 0   0   0 .75 .46 41 0   0   0 .045 .046 5.5 0   0   0 .94 .61 47 0   0   0 .0053 .0065 .53 0   0   - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 0 .10  .10  23 .85 0   0   0 .77 .47 40 0   0   0 .022 .024 5.6 0   0   0 .99 .63 49 0   0   0 .0056 .0076 .54 0   0   - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 0 .088 .088 24 .76 0   0   - - - - 0 .59 .37 41 0   0   0 .020 .023 5.6 0   0  
recursive-simple/afterrec_true-unreach-call_true-termination.c 0 .086 .087 24 .76 0   0   - - - - 0 .75 .45 40 0   0   0 .022 .023 5.6 0   0  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 0 .092 .092 24 .78 0   0   - - - - 0 .72 .44 41 0   0   0 .022 .022 5.6 0   0  
recursive-simple/fibo_15_true-unreach-call.c 0 .082 .083 24 .82 0   0   - - - - 0 .63 .38 41 0   0   0 .021 .022 5.8 0   0  
recursive-simple/fibo_20_true-unreach-call.c 0 .13  .13  23 .68 0   0   - - - - 0 .76 .46 41 0   0   0 .021 .022 5.6 0   0  
recursive-simple/fibo_25_true-unreach-call.c 0 .098 .098 24 .69 0   0   - - - - 0 .75 .47 41 0   0   0 .022 .024 5.6 0   0  
recursive-simple/fibo_2calls_10_true-unreach-call.c 0 .088 .088 24 .90 0   0   - - - - 0 .74 .45 41 0   0   0 .023 .024 5.7 0   0  
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 .091 .091 24 .75 0   0   - - - - 0 .60 .37 40 0   0   0 .020 .021 5.7 0   0  
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 .098 .097 24 .59 0   0   - - - - 0 .72 .45 40 0   0   0 .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 .086 .086 24 .95 0   0   - - - - 0 .62 .37 41 0   0   0 .028 .029 5.6 0   0  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 0 .11  .11  24 .86 0   0   - - - - 0 .78 .48 41 0   0   0 .020 .021 5.6 0   0  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 0 .095 .094 24 .70 0   0   - - - - 0 .70 .42 40 0   0   0 .020 .021 5.7 0   0  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 0 .087 .087 24 .81 0   0   - - - - 0 .82 .50 42 0   0   0 .022 .023 5.7 0   0  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 0 .095 .094 24 .77 0   0   - - - - 0 .68 .42 41 0   0   0 .023 .024 5.6 0   0  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 0 .090 .089 24 .73 0   0   - - - - 0 .60 .36 41 0   0   0 .055 .056 5.5 0   0  
recursive-simple/fibo_5_true-unreach-call_true-termination.c 0 .090 .089 24 .86 0   0   - - - - 0 .73 .45 41 0   0   0 .021 .022 5.6 0   0  
recursive-simple/fibo_7_true-unreach-call_true-termination.c 0 .086 .086 24 .75 0   0   - - - - 0 .59 .37 41 0   0   0 .029 .029 5.6 0   0  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 .087 .087 24 .82 0   0   - - - - 0 .58 .36 40 0   0   0 .021 .021 5.6 0   0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 .079 .080 24 1.3  0   0   - - - - 0 .70 .42 41 0   0   0 .023 .024 5.6 0   0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 .13  .13  23 .79 0   0   - - - - 0 .75 .45 41 0   0   0 .020 .021 5.6 0   0  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 0 .088 .088 24 .92 0   0   - - - - 0 .69 .43 40 0   0   0 .020 .022 5.6 0   0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 .085 .084 24 .72 0   0   - - - - 0 .75 .47 41 0   0   0 .022 .024 5.6 0   0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 .094 .094 24 .66 0   0   - - - - 0 .74 .44 41 0   0   0 .021 .022 5.6 0   0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 .098 .098 24 .66 0   0   - - - - 0 .67 .41 40 0   0   0 .048 .051 5.7 0   0  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 0 .14  .13  23 .75 0   0   - - - - 0 .64 .39 41 0   0   0 .020 .021 5.7 0   0  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 0 .084 .084 24 .74 0   0   - - - - 0 .76 .45 40 0   0   0 .022 .023 5.6 0   0  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 0 .080 .081 24 .91 0   0   - - - - 0 .59 .36 40 0   0   0 .050 .051 5.5 0   0  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 0 .083 .083 24 .97 0   0   - - - - 0 .63 .38 40 0   0   0 .027 .027 5.6 0   0  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 0 .096 .094 23 .85 0   0   - - - - 0 .68 .41 40 0   0   0 .024 .026 5.7 0   0  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 0 .15  .14  24 .66 0   0   - - - - 0 .70 .43 41 0   0   0 .023 .025 5.6 0   0  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 0 .082 .085 24 .76 0   0   - - - - 0 .74 .46 40 0   0   0 .021 .025 5.6 0   0  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 0 .093 .092 24 .63 0   0   - - - - 0 .60 .37 40 0   0   0 .020 .020 5.6 0   0  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 0 .085 .086 24 .81 0   0   - - - - 0 .67 .41 41 0   0   0 .021 .022 5.6 0   0  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 0 .093 .093 24 .71 0   0   - - - - 0 .60 .37 42 0   0   0 .030 .033 5.6 0   0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 0 .094 .093 24 .68 0   0   - - - - 0 .65 .39 41 0   0   0 .022 .023 5.6 0   0  
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 96 0 9.2 9.1 2300 76 0   0   44 0 30 18 1800 0   0   44 0 1.1 1.1 250 0   0   44 0 42 28 2100 0   0   44 0 .18 .23 22 0   0   52 0 36 22 2100 0   0   52 0 1.3 1.3 290 0   0  
    correct results 0 0 0 0 0 0 0
        correct true 0 0 0 0 0 0 0
        correct false 0 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 0 0 0 0 0 0 0
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-reachsafety.ReachSafety-Recursive