Tool Pinaka 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 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-06 20:14:43 CET 2018-12-07 17:00:25 CET 2018-12-07 18:15:01 CET 2018-12-07 18:51:03 CET 2018-12-12 20:55:30 CET 2018-12-07 17:47:50 CET
Run set pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pinaka.2018-12-06_2014.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pinaka.2018-12-06_2014.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)
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .37 .37 58 3.1 .0041 0     false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0   false(no-overflow) 1 --- inspect 8.3   4.6   310   .66 0   false(no-overflow) 1 --- inspect 3.5 2.1  250 0     .80 false(no-overflow) 1 --- inspect .59   .59   20    .049 0    - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .36 .36 58 3.4 .0041 0     false(no-overflow) 1 wit inspect 3.8  2.1  260 0   0   false(no-overflow) 1 --- inspect 7.3   4.5   300   .66 0   false(no-overflow) 1 --- inspect 3.5 2.1  250 0     0    false(no-overflow) 1 --- inspect .60   .60   20    .049 0    - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .37 .37 59 3.2 .0041 0     false(no-overflow) 1 wit inspect 3.8  2.1  250 0   0   false(no-overflow) 1 --- inspect 7.8   4.9   310   .66 0   false(no-overflow) 1 --- inspect 4.4 2.5  250 0     0    false(no-overflow) 1 --- inspect .59   .60   20    .049 1.4  - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 55    55    15000 690   .061  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 55    55    15000 770   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.7 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 55    55    15000 760   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 55    55    15000 620   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 73    72    15000 850   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 69    69    15000 830   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 47    47    15000 640   .061  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .35 .35 59 3.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7   5.0   310   .66 0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 89    89    15000 1300   .025  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 90    90    15000 1200   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 47    47    15000 670   .066  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .44 .44 59 3.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 34     21     1200   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 47    46    15000 620   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 45    44    15000 730   .066  .057 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 45    44    15000 680   .045  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.5 0    0  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 43    43    15000 660   .041  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.5 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 43    43    15000 620   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 43    43    15000 560   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 850    850    15000 5600   .0082 .070 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 180    180    15000 2500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 230    230    15000 3200   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900    900    4500 6300   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .62 .62 62 6.3 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 100     65     1000   .62 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .67 .68 68 6.6 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 83     54     850   .62 0  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .36 .36 58 3.7 .0041 0     false(no-overflow) 1 wit inspect 3.9  2.1  260 0   0   false(no-overflow) 1 --- inspect 7.3   4.6   310   .66 0   false(no-overflow) 1 --- inspect 4.0 2.3  250 0     .96 false(no-overflow) 1 --- inspect .59   .59   20    .045 1.1  - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .38 .38 59 3.4 .0041 0     false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 9.2   5.1   310   .66 0   false(no-overflow) 1 --- inspect 4.3 2.5  240 0     .96 false(no-overflow) 1 --- inspect .60   .60   20    .045 0    - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .36 .36 59 3.3 .0041 0     false(no-overflow) 1 wit inspect 3.9  2.2  260 0   0   false(no-overflow) 1 --- inspect 8.0   4.5   310   .66 0   false(no-overflow) 1 --- inspect 3.5 2.1  240 0     .80 false(no-overflow) 1 --- inspect .60   .60   20    .045 0    - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .37 .37 59 3.1 .0041 0     false(no-overflow) 1 wit inspect 3.9  2.2  250 0   0   false(no-overflow) 1 --- inspect 8.0   4.5   320   .10 0   false(no-overflow) 1 --- inspect 3.6 2.1  250 0     .80 false(no-overflow) 1 --- inspect .59   .60   20    .049 1.0  - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .37 .37 59 3.1 .0041 0     false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0   false(no-overflow) 1 --- inspect 11     6.3   310   .66 0   false(no-overflow) 1 --- inspect 4.7 2.8  250 0     .80 false(no-overflow) 1 --- inspect .59   .59   20    .049 0    - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2500   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2500   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.8 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    200    15000 2500   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 200    190    15000 2800   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 190    190    15000 2400   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 480    480    15000 6600   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 480    480    15000 6700   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 480    480    15000 6100   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2000   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.8 0    0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2000   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2300   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 170    170    15000 2200   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 90    90    15000 1100   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 86    85    15000 1200   .016  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .44 .44 59 4.1 0      0     false(no-overflow) 1 wit inspect 6.8  3.7  290 0   0   true -32 --- inspect 11     6.1   310   .66 0   true -32 --- inspect 6.3 3.5  260 0     1.0  false(no-overflow) 1 --- inspect .68   .68   21    .078 0    - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .47 .47 59 4.0 0      0     false(no-overflow) 1 wit inspect 7.2  3.9  290 0   0   true -32 --- inspect 8.7   4.9   310   .66 0   true -32 --- inspect 6.4 3.6  260 0     0    false(no-overflow) 1 --- inspect .68   .68   21    .078 1.4  - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .41 .41 59 4.2 0      0     false(no-overflow) 1 wit inspect 8.5  4.5  290 0   0   true -32 --- inspect 8.4   4.7   310   .66 0   true -32 --- inspect 6.1 3.4  260 0     .80 false(no-overflow) 1 --- inspect .69   .68   21    .078 0    - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .36 .36 58 3.3 0      0     false(no-overflow) 1 wit inspect 4.5  2.6  280 0   0   false(no-overflow) 1 --- inspect 6.6   4.1   300   .66 0   unknown 0 --- inspect 3.8 2.2  250 0     0    false(no-overflow) 1 --- inspect .64   .64   20    .049 0    - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .35 .35 58 3.1 0      0     false(no-overflow) 1 wit inspect 4.5  2.7  290 0   0   false(no-overflow) 1 --- inspect 9.1   5.4   310   .32 0   unknown 0 --- inspect 4.0 2.4  250 0     0    false(no-overflow) 1 --- inspect .61   .61   20    .053 0    - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .37 .37 58 3.3 0      0     false(no-overflow) 1 wit inspect 4.5  2.6  290 0   0   false(no-overflow) 1 --- inspect 7.2   4.1   300   .66 0   unknown 0 --- inspect 4.3 2.5  250 0     .80 false(no-overflow) 1 --- inspect .63   .63   20    .053 0    - --- inspect
bitvector/jain_5_false-no-overflow.i false(no-overflow) 1 wit inspect 67    67    1300 840   0      0     timeout 0 --- inspect 98    52    4900 0   0   timeout 0 --- inspect 98     52     5700   .70 0   timeout 0 --- inspect 98   51    4800 .078 0    false(no-overflow) 1 --- inspect 25      25      840    1.6   0    - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .36 .36 58 3.2 0      0     false(no-overflow) 1 wit inspect 4.4  2.7  280 0   0   false(no-overflow) 1 --- inspect 9.3   5.2   310   .66 0   unknown 0 --- inspect 3.7 2.2  250 0     0    false(no-overflow) 1 --- inspect .61   .63   20    .057 0    - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .36 .36 58 2.8 0      0     false(no-overflow) 1 wit inspect 4.1  2.4  280 0   0   false(no-overflow) 1 --- inspect 8.3   5.0   310   .66 0   unknown 0 --- inspect 4.8 2.8  250 0     0    false(no-overflow) 1 --- inspect .61   .61   20    .057 0    - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .35 .35 59 3.1 0      .057 false(no-overflow) 1 wit inspect 3.6  2.0  250 0   0   error 0 --- inspect 7.6   4.3   310   .62 0   false(no-overflow) 1 --- inspect 3.8 2.2  250 0     0    false(no-overflow) 1 --- inspect .60   .63   20    .049 .77 - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .54 .54 60 5.6 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   4.8   310   .66 0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .57 .57 59 6.1 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7   4.4   310   .66 0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 1.3  1.3  96 17   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2   4.7   310   .62 0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .47 .47 60 4.3 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10     5.9   310   .62 0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.0  6.0  680 83   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.8   4.5   310   .66 0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.0  6.0  690 77   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.6   300   .66 0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .37 .37 58 3.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     470   .62 0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .37 .37 58 3.2 0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4   4.2   310   .66 0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 32    32    15000 410   .44   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 32    31    15000 440   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 31    31    15000 410   .041  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 --- inspect 600    600    15000 7700   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 32    31    15000 420   .35   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 39    38    15000 500   .057  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
bitvector/modulus_true-unreach-call_true-no-overflow.i out of memory 0 --- inspect 59    59    15000 970   .049  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .40 .40 58 2.4 0      0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 8.3   4.7   310   .62 0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .96 .97 61 13   0      0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.1   4.3   300   .66 0  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.6  2.6  93 32   0      0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.8   300   .66 0  
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 --- inspect 900    900    510 5400   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900    900    490 6100   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
psyco/psyco_abp_1_false-no-overflow.c out of memory 0 --- inspect 62    61    15000 810   .053  0     error (invalid witness file) 0 --- inspect .78 .49 41 0   0   error (2) 0 --- inspect .027 .028 5.8 0    0   error (invalid witness file) 0 --- inspect 1.2 .78 48 0     0    error (invalid witness file) 0 --- inspect .0018 .0029 .52 0     0    - --- inspect
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)
total 79 46 9400   9400   650000 100000 2.1   .18  19 17 180 97 9500 0   0   19 -83 240 140 11000 11   0   19 -87 170 96 9100 .078 7.7 19 18 35 35 1200 2.5 5.7 60 26 330 210 7100 9.6 0  
    correct results 31 44 93   94   4400 1100 .049 .057 17 17 80 45 4600 0   0   13 13 110 63 4000 7.6 0   9 9 35 21 2200 0     5.1 18 18 35 35 1200 2.5 5.7 13 26 310 200 6300 8.3 0  
        correct true 13 26 20   20   2100 250 .016 0     0 0 0 0 13 26 310 200 6300 8.3 0  
        correct false 18 18 73   73   2300 890 .033 .057 17 17 80 45 4600 0   0   13 13 110 63 4000 7.6 0   9 9 35 21 2200 0     5.1 18 18 35 35 1200 2.5 5.7 0
    correct-unconfimed results 2 2 1.4 1.4 120 16 0     0     0 0 0 0 0
        correct-unconfirmed true 2 2 1.4 1.4 120 16 0     0     0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 0 3 -96 28 16 930 2.0 0   3 -96 19 10 780 0     1.8 0 0
        incorrect true 0 0 3 -96 28 16 930 2.0 0   3 -96 19 10 780 0     1.8 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 46 17 -83 -87 18 26
Run set pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-pinaka.sv-comp19_prop-nooverflow.NoOverflows-Other