Tool ULTIMATE Kojak 0.1.23-3204b741 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*
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: 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]
Date of execution 2017-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Recursive
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 timeout 0 wit inspect 900   2600 12000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.8 310 46 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.1   260   unknown 0 wit inspect 3.9  190 true -32 wit inspect .67   18    - wit inspect - wit inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 5.2 300 40 true -32 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.1  180 true -32 wit inspect .77   18    - wit inspect - wit inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 4.4 260 36 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 12   510 94 false(unreach-call) 1 wit inspect 46    1300 false(unreach-call) 1 wit inspect 21     600   unknown 0 wit inspect 5.2  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 0 wit inspect 25   1600 210 timeout 0 wit inspect 98    2900 timeout 0 wit inspect 98     4200   unknown 0 wit inspect 32    1800 true -32 wit inspect .72   19    - wit inspect - wit inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 4.2 250 34 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.1   240   unknown 0 wit inspect 2.9  180 true -32 wit inspect .79   18    - wit inspect - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .024 4.9
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   2400 9100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   2600 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.8
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .019 4.8
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   5000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 5.0
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 6.7 420 55 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 8.1   290  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .018 4.8
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   3300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 6.5 440 53 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 8.9   350  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.8
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   1700 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.9 270 43 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 5.4   260  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 11   600 100 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 33     830  
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 270 39 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 5.3   240   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.3 240 38 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c timeout 0 wit inspect 900   4300 10000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0018 .27 - wit inspect - wit inspect
recursive-simple/fibo_15_false-unreach-call.c timeout 0 wit inspect 900   3500 11000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
recursive-simple/fibo_20_false-unreach-call.c timeout 0 wit inspect 900   3600 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
recursive-simple/fibo_25_false-unreach-call.c timeout 0 wit inspect 900   3400 13000 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0019 .27 - wit inspect - wit inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c timeout 0 wit inspect 900   2100 10000 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 0 wit inspect 900   2000 13000 error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 wit inspect 900   2500 11000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 wit inspect 900   2300 12000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .037 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.2 340 47 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.1   260   unknown 0 wit inspect 3.5  190 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c timeout 0 wit inspect 900   1700 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0013 .34 - wit inspect - wit inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c timeout 0 wit inspect 900   1400 12000 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .34 - wit inspect - wit inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c timeout 0 wit inspect 900   1900 13000 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .94 49 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c timeout 0 wit inspect 900   3600 10000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c timeout 0 wit inspect 900   2600 12000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.2  51 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c timeout 0 wit inspect 900   2800 12000 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .82 48 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 6.3 350 48 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 3.5  180 true -32 wit inspect .62   18    - wit inspect - wit inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.7 500 78 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.4   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   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 6.0 330 48 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.9   250   unknown 0 wit inspect 3.8  180 true -32 wit inspect .63   18    - wit inspect - wit inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 24   940 200 false(unreach-call) 1 wit inspect 3.7  260 true -32 wit inspect 5.3   220   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .76   19    - wit inspect - wit inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 50   1400 680 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 5.2   230   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 100   2400 1300 false(unreach-call) 1 wit inspect 5.2  280 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 170   3200 2100 false(unreach-call) 1 wit inspect 4.8  280 true -32 wit inspect 4.6   240   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.3 470 75 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 5.1   250   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2500 10000 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3300 11000 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0017 .28 - wit inspect - wit inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 16   680 170 false(unreach-call) 1 wit inspect 3.7  260 true -32 wit inspect 4.3   210   unknown 0 wit inspect 3.4  210 true -32 wit inspect .78   18    - wit inspect - wit inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2300 12000 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 91   1100 1200 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 3.4   230   unknown 0 wit inspect 3.1  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 6.7 420 53 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.2   240   unknown 0 wit inspect 2.7  180 true -32 wit inspect .63   18    - wit inspect - wit inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   480 110 false(unreach-call) 1 wit inspect 5.4  280 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   530 110 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 4.6   250   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .80   19    - wit inspect - wit inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 16   700 140 false(unreach-call) 1 wit inspect 4.6  280 true -32 wit inspect 6.1   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 19   790 170 false(unreach-call) 1 wit inspect 5.2  290 true -32 wit inspect 4.9   260   unknown 0 wit inspect 4.3  210 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
recursive-simple/sum_2x3_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 300 44 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .74   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 4.3 250 37 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.5   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 4.2 260 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.3   270  
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 4.4 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.8   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_15_true-unreach-call.c timeout 0 wit inspect 900   5900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_20_true-unreach-call.c timeout 0 wit inspect 900   6100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 46 error (2) 0 wit inspect .018 4.9
recursive-simple/fibo_25_true-unreach-call.c timeout 0 wit inspect 900   6400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 5.0
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 5.0
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 wit inspect 900   4900 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .021 4.9
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 45 error (2) 0 wit inspect .018 5.0
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4100 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .019 4.8
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4600 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.9
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3400 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.8
recursive-simple/fibo_7_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4600 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 5.0
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.2 480 62 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.2  250 true 2 wit inspect 12     430  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 11   570 100 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 11     480  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 14   650 130 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 13     500  
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1700 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .018 4.8
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.6 470 61 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 8.4   350  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.3 390 52 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 2.9  250 true 2 wit inspect 6.6   260  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.5 390 50 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.4  250 true 2 wit inspect 6.5   260  
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 17   720 170 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 14     530  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 24   840 240 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.0  250 true 2 wit inspect 23     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 34   1000 350 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 true 2 wit inspect 28     740  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 44   1400 450 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.5  250 true 2 wit inspect 37     810  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 11   560 90 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.6  250 true 2 wit inspect 12     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   2900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 5.0
recursive-simple/sum_20x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   3500 15000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 wit inspect 900   4500 15000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .020 4.8
recursive-simple/sum_2x3_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.8
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 6.8 370 59 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.3  250 true 2 wit inspect 8.6   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 61 48000 200000 620000 44 -74 250   11000 44 -305 240 11000 44 0 140 7700 44 -304 18   490 52 4 84   5900 52 36 250 8200
    correct results 43 61 840 27000 9100 22 22 130   6900 15 15 95 4100 0 16 16 11   300 2 4 7.8 500 18 36 250 8000
        correct true 18 36 230 10000 2100 0 0 0 0 2 4 7.8 500 18 36 250 8000
        correct false 25 25 610 17000 6900 22 22 130   6900 15 15 95 4100 0 16 16 11   300 0 0
    correct-unconfimed results 1 0 25 1600 210 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 25 1600 210 0 0 0 0 0 0
    incorrect results 0 3 -96 9.1 770 10 -320 48 2400 0 10 -320 6.9 180 0 0
        incorrect true 0 3 -96 9.1 770 10 -320 48 2400 0 10 -320 6.9 180 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 61 -74 -305 0 -304 4 36
Run set ukojak.sv-comp18.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Recursive