Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Recursive
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .20 11 1.9 false(unreach-call) 1 wit inspect 8.4 290 true -32 wit inspect 3.4 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .16 12 2.1 false(unreach-call) 1 wit inspect 5.1 270 true -32 wit inspect 4.6 240 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .17 11 1.9 false(unreach-call) 1 wit inspect 2.5 250 true -32 wit inspect 3.0 240 unknown 0 wit inspect 1.9 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .20 12 2.8 false(unreach-call) 1 wit inspect 3.3 260 true -32 wit inspect 3.2 230 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .24 12 2.4 false(unreach-call) 1 wit inspect 14   360 true -32 wit inspect 3.1 230 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .32 12 4.2 timeout 0 wit inspect 91   1200 true -32 wit inspect 4.8 230 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect .16 11 2.1 false(unreach-call) 1 wit inspect 3.0 260 true -32 wit inspect 4.7 230 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    8100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .022 5.0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    8100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .019 4.8
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    8100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .021 4.9
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    93 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 5.0
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    130 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 5.0
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect .39 13 4.7 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     4600  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout (timeout) 0 wit inspect 900    11000 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .024 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 26     2600  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    14000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .021 4.9
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    190 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    140 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .024 4.8
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout (timeout) 0 wit inspect 900    1400 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .020 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    48 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.9
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    26 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 5.0
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900    12000 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .020 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .23 12 2.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.8  250 true 2 wit inspect 5.6   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .23 12 2.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 34     860  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.4 false(unreach-call) 1 wit inspect 3.4 260 true -32 wit inspect 4.2 210 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.4 false(unreach-call) 1 wit inspect 3.1 260 true -32 wit inspect 4.4 230 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.6 false(unreach-call) 1 wit inspect 5.8 360 true -32 wit inspect 3.4 230 unknown 0 wit inspect 2.7 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c false(unreach-call) 1 wit inspect .15 11 1.7 false(unreach-call) 1 wit inspect 13   1200 true -32 wit inspect 4.5 230 unknown 0 wit inspect 2.6 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c false(unreach-call) 1 wit inspect .23 19 2.7 out of memory 0 wit inspect 44   7000 true -32 wit inspect 4.9 230 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c false(unreach-call) 1 wit inspect .84 110 11   timeout 0 wit inspect 96   3500 true -32 wit inspect 4.5 220 unknown 0 wit inspect 1.9 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 4.4 340 true -32 wit inspect 4.5 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c false(unreach-call) 1 wit inspect .17 11 1.5 false(unreach-call) 1 wit inspect 16   1200 true -32 wit inspect 4.5 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c false(unreach-call) 1 wit inspect .19 14 1.9 out of memory 0 wit inspect 40   7000 true -32 wit inspect 3.4 230 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c false(unreach-call) 1 wit inspect .42 52 5.2 timeout 0 wit inspect 97   3500 true -32 wit inspect 3.2 230 unknown 0 wit inspect 1.9 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 3.1 260 true -32 wit inspect 4.3 220 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17 11 1.5 false(unreach-call) 1 wit inspect 4.3 270 true -32 wit inspect 4.4 220 unknown 0 wit inspect 2.7 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 5.0 290 true -32 wit inspect 4.4 230 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.7 false(unreach-call) 1 wit inspect 3.1 270 true -32 wit inspect 4.9 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.9 false(unreach-call) 1 wit inspect 3.2 300 true -32 wit inspect 3.3 230 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.5 false(unreach-call) 1 wit inspect 4.3 260 true -32 wit inspect 3.0 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .56 18 - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.8 false(unreach-call) 1 wit inspect 3.9 280 true -32 wit inspect 4.5 220 unknown 0 wit inspect 2.6 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .18 12 2.2 false(unreach-call) 1 wit inspect 2.7 270 true -32 wit inspect 3.1 220 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.5 false(unreach-call) 1 wit inspect 4.0 260 true -32 wit inspect 4.6 230 unknown 0 wit inspect 2.1 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .17 11 1.7 false(unreach-call) 1 wit inspect 3.7 280 true -32 wit inspect 4.1 210 unknown 0 wit inspect 1.9 190 false(unreach-call) 1 wit inspect .60 19 - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.7 false(unreach-call) 1 wit inspect 3.2 260 true -32 wit inspect 4.7 220 unknown 0 wit inspect 2.0 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.3 false(unreach-call) 1 wit inspect 2.5 260 true -32 wit inspect 3.0 220 unknown 0 wit inspect 2.7 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.6 false(unreach-call) 1 wit inspect 3.8 270 true -32 wit inspect 3.0 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 3.9 270 true -32 wit inspect 3.3 230 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14 11 1.9 false(unreach-call) 1 wit inspect 3.8 260 true -32 wit inspect 4.3 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .15 11 1.9 timeout 0 wit inspect 91   2600 true -32 wit inspect 4.4 210 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .15 11 2.0 false(unreach-call) 1 wit inspect 9.9 640 true -32 wit inspect 3.0 220 unknown 0 wit inspect 2.0 210 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .17 11 1.5 false(unreach-call) 1 wit inspect 4.1 270 true -32 wit inspect 2.9 220 unknown 0 wit inspect 2.1 200 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .18 11 1.3 false(unreach-call) 1 wit inspect 17   1600 true -32 wit inspect 2.9 220 unknown 0 wit inspect 2.0 200 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .15 11 1.9 false(unreach-call) 1 wit inspect 5.1 270 true -32 wit inspect 3.0 220 unknown 0 wit inspect 2.0 180 false(unreach-call) 1 wit inspect .60 19 - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .17 11 1.8 false(unreach-call) 1 wit inspect 3.8 260 true -32 wit inspect 2.8 220 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.5 false(unreach-call) 1 wit inspect 2.5 270 true -32 wit inspect 3.1 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17 11 1.7 false(unreach-call) 1 wit inspect 4.2 270 true -32 wit inspect 3.0 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .56 18 - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15 11 1.5 false(unreach-call) 1 wit inspect 4.2 270 true -32 wit inspect 4.3 230 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 4.2 280 true -32 wit inspect 2.9 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .56 18 - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.6 false(unreach-call) 1 wit inspect 4.5 260 true -32 wit inspect 3.2 220 unknown 0 wit inspect 1.9 190 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect .14 11 1.6 false(unreach-call) 1 wit inspect 3.4 260 true -32 wit inspect 3.2 220 unknown 0 wit inspect 1.9 180 false(unreach-call) 1 wit inspect .57 18 - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 5.9   270  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.0   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c true 2 wit inspect .16 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 66     4500  
recursive-simple/fibo_15_true-unreach-call.c true 1 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 timeout 0 wit inspect 960     5400  
recursive-simple/fibo_20_true-unreach-call.c true 1 wit inspect .22 13 2.7 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  260 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_25_true-unreach-call.c true 1 wit inspect .73 35 9.0 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 timeout 0 wit inspect 960     6000  
recursive-simple/fibo_2calls_10_true-unreach-call.c true 2 wit inspect .16 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 140     4500  
recursive-simple/fibo_2calls_15_true-unreach-call.c true 1 wit inspect .14 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 timeout 0 wit inspect 960     5700  
recursive-simple/fibo_2calls_20_true-unreach-call.c true 1 wit inspect .16 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  270 timeout 0 wit inspect 960     6500  
recursive-simple/fibo_2calls_25_true-unreach-call.c true 1 wit inspect .37 20 4.9 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.3  250 timeout 0 wit inspect 960     6300  
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.9   360  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  260 true 2 wit inspect 19     540  
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c true 2 wit inspect .17 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 27     630  
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  270 true 2 wit inspect 27     710  
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c true 2 wit inspect .17 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 56     1700  
recursive-simple/fibo_5_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 19     560  
recursive-simple/fibo_7_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 19     800  
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .023 4.9
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    2100 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .020 4.9
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .16 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.1  250 true 2 wit inspect 14     450  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    1700 9800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .017 5.0
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    1700 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900    1700 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 15     530  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 22     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 20     730  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 43     820  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 9.6   430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.1  250 true 2 wit inspect 19     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  260 true 2 wit inspect 24     690  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 37     750  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 49     910  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 9.5   360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect .13 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.7  250 true 2 wit inspect 10     300  
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 96 103 17000   76000 220000 44 38 660 39000 44 -1408 170 9800 44 0 94 8700 44 44 25 810 52 6 120   9100 52 52 7500 66000
    correct results 70 96 12   930 130 38 38 200 14000 0 0 44 44 25 810 3 6 9.3 770 26 52 730 26000
        correct true 26 52 3.9 280 42 0 0 0 0 3 6 9.3 770 26 52 730 26000
        correct false 44 44 8.2 650 92 38 38 200 14000 0 0 44 44 25 810 0 0
    correct-unconfimed results 7 7 2.2 110 27 0 0 0 0 0 0
        correct-unconfirmed true 7 7 2.2 110 27 0 0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0 0
    incorrect results 0 0 44 -1408 170 9800 0 0 0 0
        incorrect true 0 0 44 -1408 170 9800 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 103 38 -1408 0 44 6 52
Run set symbiotic.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Recursive