Tool ULTIMATE Kojak 0.1.23-635dfa2a 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-08 11:04:44 CET 2018-12-09 20:15:59 CET 2018-12-09 20:59:07 CET 2018-12-09 21:01:30 CET 2018-12-12 21:11:08 CET 2018-12-09 19:35:17 CET 2018-12-09 20:36:45 CET
Run set ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive
Options --full-output -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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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 timeout 0 --- inspect 900   800   1100 9200 .64 0      error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .60 46 0   0      error (invalid witness file) 0 --- inspect .0021 .0027 .53 0     0      - --- inspect - --- inspect
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 9.1 3.0 370 78 .66 .0041 false(unreach-call) 1 wit inspect 4.3  2.4  260 0   0      false(unreach-call) 1 --- inspect 7.3   4.2   310   .62 0      unknown 0 --- inspect 3.6  2.1  250 0   .0041 error (2) 0 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 8.4 2.8 360 63 .66 0      true -32 wit inspect 4.7  2.6  250 0   0      false(unreach-call) 1 --- inspect 7.0   4.4   310   .62 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 8.0 3.2 350 61 .66 0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0      false(unreach-call) 1 --- inspect 7.0   3.9   310   .62 .0041 unknown 0 --- inspect 3.5  2.1  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 14   5.4 510 120 .66 0      unknown 0 --- inspect 9.4  5.5  360 0   .0041 false(unreach-call) 1 --- inspect 18     10     630   .62 0      unknown 0 --- inspect 5.3  2.9  270 0   0      true -32 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 25   8.7 1000 230 .66 0      false(unreach-call) 1 wit inspect 61    40    2100 0   0      timeout 0 --- inspect 97     72     3500   .63 0      unknown 0 --- inspect 21    12    710 0   0      true -32 --- inspect .63   .63   22    .049 0      - --- inspect - --- inspect
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c false(unreach-call) 1 wit inspect 7.7 2.6 370 62 .66 0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 6.8   3.9   310   .62 0      unknown 0 --- inspect 3.5  2.0  240 0   0      true -32 --- inspect .59   .59   20    .049 .0041 - --- inspect - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   830   1100 9900 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.8 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   680   1400 11000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   690   1400 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 41 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   760   960 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   750   2700 9000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   800   920 6900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0      error (2) 0 --- inspect .029 .029 5.6 0    0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   520   970 9100 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 43 0   0      error (2) 0 --- inspect .027 .028 5.7 0    0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   790   5200 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   770   4800 13000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .021 .024 5.6 0    0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 11   4.1 480 77 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.1  250 0   0      true 2 --- inspect 10     6.1   340   .66 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   530   820 9700 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900   640   1300 10000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 11   3.8 520 83 .66 .020  - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.3  2.3  250 0   0      true 2 --- inspect 13     7.8   350   .66 .0041
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   560   1000 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   720   960 10000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 9.0 3.3 410 70 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 9.1   5.1   320   .66 0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 15   6.8 700 150 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 16     9.5   510   .66 0     
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.9 2.9 370 64 .66 0      true -32 wit inspect 4.6  2.6  250 0   0      false(unreach-call) 1 --- inspect 7.2   4.4   310   .62 0      false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0      false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
recursive-simple/afterrec_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.9 3.1 360 67 .66 0      true -32 wit inspect 4.1  2.3  250 0   0      false(unreach-call) 1 --- inspect 8.3   4.7   310   .62 0      false(unreach-call) 1 --- inspect 3.5  2.0  240 0   0      false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
recursive-simple/fibo_10_false-unreach-call_true-termination.c timeout 0 --- inspect 900   640   1400 9600 .64 0      error (invalid witness file) 0 --- inspect .88 .53 42 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .64 47 0   0      error (invalid witness file) 0 --- inspect .0031 .0033 .40 0     0      - --- inspect - --- inspect
recursive-simple/fibo_15_false-unreach-call.c timeout 0 --- inspect 900   640   1400 12000 .64 0      error (invalid witness file) 0 --- inspect .74 .45 41 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .61 47 0   0      error (invalid witness file) 0 --- inspect .0048 .0059 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_20_false-unreach-call.c timeout 0 --- inspect 900   520   2100 10000 .64 0      error (invalid witness file) 0 --- inspect .77 .48 40 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0      error (invalid witness file) 0 --- inspect .98 .62 48 0   0      error (invalid witness file) 0 --- inspect .0018 .0024 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_25_false-unreach-call.c timeout 0 --- inspect 900   640   1400 12000 .64 0      error (invalid witness file) 0 --- inspect .63 .39 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0052 .0073 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_10_false-unreach-call.c timeout 0 --- inspect 900   550   1300 9600 .65 0      error (invalid witness file) 0 --- inspect .84 .51 41 0   0      error (2) 0 --- inspect .021 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .97 .62 47 0   0      error (invalid witness file) 0 --- inspect .0053 .0066 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_15_false-unreach-call.c timeout 0 --- inspect 900   510   1200 11000 .65 0      error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .93 .62 47 0   0      error (invalid witness file) 0 --- inspect .0013 .0015 .40 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 0 --- inspect 900   550   1200 9800 .64 0      error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0054 .0065 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 0 --- inspect 900   510   1200 11000 .65 0      error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0      error (invalid witness file) 0 --- inspect .93 .61 47 0   0      error (invalid witness file) 0 --- inspect .0064 .0099 .66 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.7 3.5 380 84 .66 0      false(unreach-call) 1 wit inspect 5.0  2.7  260 0   0      false(unreach-call) 1 --- inspect 7.9   4.4   310   .66 0      false(unreach-call) 1 --- inspect 3.8  2.3  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c timeout 0 --- inspect 900   530   910 12000 .65 0      error (invalid witness file) 0 --- inspect .67 .41 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .62 48 0   0      error (invalid witness file) 0 --- inspect .0056 .0070 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c timeout 0 --- inspect 900   630   990 12000 .64 .0041 error (invalid witness file) 0 --- inspect .73 .46 42 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0069 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c timeout 0 --- inspect 900   560   1200 11000 .64 0      error (invalid witness file) 0 --- inspect .71 .43 43 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .63 48 0   0      error (invalid witness file) 0 --- inspect .0060 .0080 .53 0     0      - --- inspect - --- inspect
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c timeout 0 --- inspect 900   500   1100 10000 .14 0      error (invalid witness file) 0 --- inspect .61 .36 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect 1.0  .68 48 0   0      error (invalid witness file) 0 --- inspect .0019 .0028 .52 0     0      - --- inspect - --- inspect
recursive-simple/fibo_5_false-unreach-call_true-termination.c timeout 0 --- inspect 900   600   1100 11000 .65 0      error (invalid witness file) 0 --- inspect .72 .45 41 0   0      error (2) 0 --- inspect .020 .021 5.5 0    0      error (invalid witness file) 0 --- inspect .96 .62 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0026 .54 0     0      - --- inspect - --- inspect
recursive-simple/fibo_7_false-unreach-call_true-termination.c timeout 0 --- inspect 900   580   1700 10000 .65 0      error (invalid witness file) 0 --- inspect .72 .44 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0      error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0058 .54 0     0      - --- inspect - --- inspect
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 8.9 3.1 370 66 .66 0      false(unreach-call) 1 wit inspect 5.0  2.8  260 0   0      false(unreach-call) 1 --- inspect 7.4   4.2   310   .62 0      unknown 0 --- inspect 4.0  2.3  250 0   0      true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   4.5 570 110 .66 0      false(unreach-call) 1 wit inspect 5.9  3.2  270 0   0      false(unreach-call) 1 --- inspect 6.9   4.0   300   .62 0      false(unreach-call) 1 --- inspect 3.9  2.3  250 0   0      false(unreach-call) 1 --- inspect .56   .56   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 9.0 3.1 370 69 .66 0      false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0      false(unreach-call) 1 --- inspect 7.5   4.2   310   .62 0      unknown 0 --- inspect 3.8  2.2  250 0   0      true -32 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 27   14   860 250 .66 0      false(unreach-call) 1 wit inspect 5.7  3.1  260 0   0      true -32 --- inspect 6.9   4.3   300   .62 0      false(unreach-call) 1 --- inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 63   41   1300 740 .62 0      false(unreach-call) 1 wit inspect 6.3  3.5  270 0   .029  true -32 --- inspect 8.1   4.4   300   .62 0      false(unreach-call) 1 --- inspect 4.1  2.3  260 0   0      false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 130   94   1800 1800 .62 0      false(unreach-call) 1 wit inspect 7.0  3.7  280 0   0      true -32 --- inspect 7.1   4.0   300   .62 0      false(unreach-call) 1 --- inspect 4.2  2.4  250 0   0      false(unreach-call) 1 --- inspect .59   .59   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 250   200   1800 2400 .62 0      false(unreach-call) 1 wit inspect 6.6  3.6  280 0   0      true -32 --- inspect 7.8   4.2   300   .66 0      false(unreach-call) 1 --- inspect 4.4  2.5  260 0   .0041 false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   4.2 560 110 .66 0      false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0      false(unreach-call) 1 --- inspect 7.0   4.0   300   .62 0      false(unreach-call) 1 --- inspect 4.1  2.3  250 0   0      false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   810   900 7100 .64 0      error (invalid witness file) 0 --- inspect .72 .43 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .94 .61 47 0   0      error (invalid witness file) 0 --- inspect .0067 .0091 .52 0     0      - --- inspect - --- inspect
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   800   760 7100 .64 .0041 error (invalid witness file) 0 --- inspect .75 .45 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .66 47 0   0      error (invalid witness file) 0 --- inspect .0056 .0067 .54 0     0      - --- inspect - --- inspect
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 23   12   730 200 .66 0      false(unreach-call) 1 wit inspect 5.6  3.1  280 0   .0041 true -32 --- inspect 7.1   4.4   290   .62 0      unknown 0 --- inspect 4.0  2.3  250 0   0      true -32 --- inspect .59   .59   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   810   950 10000 .64 .0041 error (invalid witness file) 0 --- inspect .78 .48 40 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0      error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0020 .39 0     0      - --- inspect - --- inspect
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 67   46   740 550 .62 0      false(unreach-call) 1 wit inspect 6.9  3.8  280 0   .0082 true -32 --- inspect 7.2   4.4   290   .62 0      unknown 0 --- inspect 4.3  2.5  260 0   0      true -32 --- inspect .58   .58   21    .049 0      - --- inspect - --- inspect
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 10   3.5 430 87 .66 0      false(unreach-call) 1 wit inspect 5.7  3.2  260 0   0      false(unreach-call) 1 --- inspect 6.7   3.8   300   .66 0      unknown 0 --- inspect 3.8  2.2  240 0   0      true -32 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
recursive-simple/sum_10x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 13   3.9 540 110 .66 0      false(unreach-call) 1 wit inspect 5.5  3.0  270 0   .016  true -32 --- inspect 7.6   4.5   290   .66 0      false(unreach-call) 1 --- inspect 4.0  2.3  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_15x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 15   5.3 500 120 .66 0      false(unreach-call) 1 wit inspect 6.6  3.6  270 0   0      true -32 --- inspect 7.1   4.0   300   .62 0      false(unreach-call) 1 --- inspect 4.1  2.4  250 0   0      false(unreach-call) 1 --- inspect .58   .58   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_20x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 18   5.8 660 170 .66 0      false(unreach-call) 1 wit inspect 6.5  3.5  280 0   0      true -32 --- inspect 7.9   4.4   300   .62 0      false(unreach-call) 1 --- inspect 4.2  2.4  260 0   .0041 false(unreach-call) 1 --- inspect .58   .57   21    .045 0      - --- inspect - --- inspect
recursive-simple/sum_25x0_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 22   7.3 720 190 .66 0      false(unreach-call) 1 wit inspect 7.6  4.1  280 0   0      true -32 --- inspect 7.3   4.1   290   .62 0      false(unreach-call) 1 --- inspect 4.5  2.6  260 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 9.0 2.9 380 66 .66 0      false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0      false(unreach-call) 1 --- inspect 7.2   4.0   300   .62 0      false(unreach-call) 1 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c false(unreach-call) 1 wit inspect 8.5 2.7 370 61 .66 0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0      false(unreach-call) 1 --- inspect 6.8   4.3   310   .62 0      unknown 0 --- inspect 3.6  2.1  250 0   0      false(unreach-call) 1 --- inspect .60   .60   20    .049 .0041 - --- inspect - --- inspect
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c true 2 wit inspect 7.7 2.6 380 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0   0      true 2 --- inspect 7.7   4.2   320   .66 0     
recursive-simple/afterrec_true-unreach-call_true-termination.c true 2 wit inspect 7.4 2.6 350 62 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 9.7   5.4   310   .62 0     
recursive-simple/fibo_10_true-unreach-call_true-termination.c timeout 0 --- inspect 900   820   5200 14000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .027 .027 5.6 0    0     
recursive-simple/fibo_15_true-unreach-call.c timeout 0 --- inspect 900   840   5400 13000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0      error (2) 0 --- inspect .028 .029 5.6 0    0     
recursive-simple/fibo_20_true-unreach-call.c timeout 0 --- inspect 900   840   5600 13000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive-simple/fibo_25_true-unreach-call.c timeout 0 --- inspect 900   840   5800 14000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .030 .030 5.6 0    0     
recursive-simple/fibo_2calls_10_true-unreach-call.c timeout 0 --- inspect 900   810   5100 15000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 41 0   0      error (2) 0 --- inspect .036 .037 5.6 0    0     
recursive-simple/fibo_2calls_15_true-unreach-call.c timeout 0 --- inspect 900   820   5100 14000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 42 0   0      error (2) 0 --- inspect .034 .035 5.7 0    0     
recursive-simple/fibo_2calls_20_true-unreach-call.c timeout 0 --- inspect 900   810   5100 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .41 42 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
recursive-simple/fibo_2calls_25_true-unreach-call.c timeout 0 --- inspect 900   820   5100 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 40 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0     
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c timeout 0 --- inspect 900   650   890 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c timeout 0 --- inspect 900   540   900 8800 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   630   860 13000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .40 40 0   0      error (2) 0 --- inspect .026 .026 5.6 0    0     
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c timeout 0 --- inspect 900   520   1700 10000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c timeout 0 --- inspect 900   700   2700 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 42 0   0      error (2) 0 --- inspect .025 .026 5.6 0    0     
recursive-simple/fibo_5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   590   1400 12000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0     
recursive-simple/fibo_7_true-unreach-call_true-termination.c timeout 0 --- inspect 900   560   3000 12000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 11   4.5 510 100 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 13     7.8   450   .66 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 14   6.2 630 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 14     8.3   520   .66 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 12   4.9 560 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 14     8.9   500   .62 0     
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c timeout 0 --- inspect 900   500   1100 9700 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0      error (2) 0 --- inspect .028 .028 5.6 0    0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 10   3.8 520 96 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.4  2.4  250 0   0      true 2 --- inspect 15     8.9   380   .66 .0041
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.4 3.2 410 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 9.7   5.3   320   .62 .0041
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 10   3.8 420 73 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 10     6.1   310   .66 0     
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c true 2 wit inspect 21   9.8 610 230 .66 .020  - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 20     12     510   .62 0     
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c true 2 wit inspect 30   16   850 300 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 28     17     660   .62 0     
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c true 2 wit inspect 45   25   790 460 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 4.6  2.6  250 0   0      true 2 --- inspect 35     21     680   .62 0     
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c true 2 wit inspect 57   33   930 640 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 47     30     740   .56 0     
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c true 2 wit inspect 15   5.9 650 140 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 14     8.2   440   .66 0     
recursive-simple/sum_10x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   520   1100 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
recursive-simple/sum_15x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   620   1100 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
recursive-simple/sum_20x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   700   1200 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .022 .023 5.7 0    0     
recursive-simple/sum_25x0_true-unreach-call_true-termination.c timeout 0 --- inspect 900   750   1400 12000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0      error (2) 0 --- inspect .026 .027 5.7 0    0     
recursive-simple/sum_2x3_true-unreach-call_true-termination.c timeout 0 --- inspect 900   720   1100 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.7 3.2 400 78 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (recursion) 0 wit inspect 3.6  2.0  250 0   .0041 true 2 --- inspect 10     5.8   330   .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 62 48000 35000 130000 580000 62 .057  44 -74 210 130   9500 0   .061 44 -305 290 180 11000 16   .0041 44 14 140 80 7800 0   .012  44 -272 15   15   540 1.2  .0082 52 4 90   52   5900 0   .0041 52 36 300 180 8200 11 .012
    correct results 44 62 1100 630 27000 11000 29 .045  22 22 180 100   7700 0   .057 15 15 120 68 4900 9.4 .0041 14 14 56 32 3500 0   .0082 16 16 9.2 9.2 330 .74 .0041 2 4 7.2 4.0 510 0   0      18 36 300 180 8000 11 .012
        correct true 18 36 300 140 10000 2900 12 .041  0 0 0 0 2 4 7.2 4.0 510 0   0      18 36 300 180 8000 11 .012
        correct false 26 26 800 480 17000 7900 17 .0041 22 22 180 100   7700 0   .057 15 15 120 68 4900 9.4 .0041 14 14 56 32 3500 0   .0082 16 16 9.2 9.2 330 .74 .0041 0 0
    incorrect results 0 3 -96 13 7.5 750 0   0     10 -320 74 43 3000 6.3 0      0 9 -288 5.3 5.3 190 .44 .0041 0 0
        incorrect true 0 3 -96 13 7.5 750 0   0     10 -320 74 43 3000 6.3 0      0 9 -288 5.3 5.3 190 .44 .0041 0 0
        incorrect false 0 0 0 0 0 0 0
score (96 tasks, max score: 148) 62 -74 -305 14 -272 4 36
Run set ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive cpa-seq-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-reachsafety.ReachSafety-Recursive