Tool CBMC 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-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc.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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 .14  .13  9.6 .62 .0082 0      false(no-overflow) 1 wit inspect 28    15    570 0   0   false(no-overflow) 1 --- inspect 7.6   4.3   310   .66  0   false(no-overflow) 1 --- inspect 4.5  2.6  260 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .049 1.4    - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .083 .074 9.7 .87 .0082 0      false(no-overflow) 1 wit inspect 4.7  2.6  260 0   0   false(no-overflow) 1 --- inspect 9.7   5.7   310   .62  0   false(no-overflow) 1 --- inspect 4.0  2.4  250 0   1.5  false(no-overflow) 1 --- inspect .60   .62   20    .049 .85   - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .079 .068 9.6 .62 .0082 0      false(no-overflow) 1 wit inspect 6.1  3.4  260 0   0   false(no-overflow) 1 --- inspect 7.9   4.9   310   .66  0   false(no-overflow) 1 --- inspect 4.0  2.4  250 0   1.9  false(no-overflow) 1 --- inspect .59   .59   20    .049 .92   - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     240   4200    .95   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     230   3200    1.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.7 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     230   3200    .88   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     230   3100    .88   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 760     760     15000   9000    36      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 770     770     15000   7400    36      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     15000   9800    36      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 .092 .086 6.2 .42 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6   4.3   300   .66 0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     2800   9300    5.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     2800   7900    5.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     200   7500    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .12  .12  7.6 1.2  .15   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 34     21     1000   .62 0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     190   5100    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     180   3500    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0    0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     180   4000    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     1600   4100    18      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .031 5.8 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     1600   3400    18      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     330   3500    .50   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (42) 0 --- inspect 880     880     200   3100    .090  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     4800   8100    .30   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     6800   9700    .33   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.7 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     1400   3500    28      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.7 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .37  .37  12   4.3  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 97     61     900   .62 0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .44  .43  12   4.2  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 95     60     930   .62 0  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .097 .081 9.2 .39 .0082 0      false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 9.4   5.6   310   .62  0   false(no-overflow) 1 --- inspect 3.8  2.2  250 0   1.6  false(no-overflow) 1 --- inspect .60   .60   20    .045 .74   - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .073 .061 9.0 .51 .0082 0      false(no-overflow) 1 wit inspect 5.2  2.9  260 0   0   false(no-overflow) 1 --- inspect 7.8   4.5   310   .66  0   false(no-overflow) 1 --- inspect 3.8  2.3  250 0   .80 false(no-overflow) 1 --- inspect .60   .61   20    .045 .91   - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .11  .093 8.5 .37 .0082 0      false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 9.7   5.5   310   .086 0   false(no-overflow) 1 --- inspect 3.7  2.1  250 0   1.5  false(no-overflow) 1 --- inspect .61   .61   20    .045 0      - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .15  .13  9.1 .42 .0082 0      false(no-overflow) 1 wit inspect 4.8  2.7  260 0   0   false(no-overflow) 1 --- inspect 7.6   4.3   310   .66  0   false(no-overflow) 1 --- inspect 4.0  2.3  250 0   1.6  false(no-overflow) 1 --- inspect .60   .60   20    .049 1.4    - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .074 .065 9.3 .63 .0082 0      false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 9.5   5.7   310   .62  0   false(no-overflow) 1 --- inspect 3.7  2.2  250 0   1.8  false(no-overflow) 1 --- inspect .59   .60   20    .049 1.4    - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     5000   4800    6.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     5000   5400    7.1    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     5000   6700    6.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     5000   5900    6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     9900   6100    7.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     640   13000    3.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     640   13000    3.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.5 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     5000   6600    8.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 640     640     15000   4500    3.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 700     700     15000   3900    3.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.5 0    0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 660     650     15000   4200    2.9    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 690     690     15000   4100    3.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 720     720     15000   3700    3.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 710     710     15000   4700    3.0    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     11000   4700    3.3    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c out of memory 0 --- inspect 820     820     15000   8000    3.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .13  .12  9.8 1.0  .061  0      true -32 wit inspect 47    27    950 0   0   error 0 --- inspect 26     15     710   .62  0   unknown 0 --- inspect 6.5  3.5  280 0   0    false(no-overflow) 1 --- inspect .70   .70   21    .086 .89   - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .14  .13  10   1.1  .057  0      true -32 wit inspect 44    26    1000 0   0   error 0 --- inspect 28     16     550   .66  0   unknown 0 --- inspect 5.7  3.1  270 0   0    false(no-overflow) 1 --- inspect .71   .71   21    .086 0      - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .13  .12  9.5 1.5  .061  0      true -32 wit inspect 6.0  3.3  260 0   0   error 0 --- inspect 36     24     720   .62  0   unknown 0 --- inspect 5.1  2.8  260 0   0    false(no-overflow) 1 --- inspect .72   .72   21    .086 .0041 - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .070 .059 9.3 .38 .0082 0      false(no-overflow) 1 wit inspect 5.6  3.3  290 0   0   false(no-overflow) 1 --- inspect 7.4   4.2   310   .62  0   unknown 0 --- inspect 3.7  2.2  250 0   0    false(no-overflow) 1 --- inspect .61   .62   20    .049 0      - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .095 .086 9.9 .78 .0082 0      false(no-overflow) 1 wit inspect 4.8  2.8  290 0   0   false(no-overflow) 1 --- inspect 9.0   4.9   310   .66  0   unknown 0 --- inspect 3.8  2.3  250 0   1.1  false(no-overflow) 1 --- inspect .61   .61   20    .053 1.4    - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .086 .075 9.3 .72 .0082 0      false(no-overflow) 1 wit inspect 4.6  2.7  290 0   0   false(no-overflow) 1 --- inspect 7.1   4.1   300   .66  0   unknown 0 --- inspect 3.7  2.2  250 0   1.2  false(no-overflow) 1 --- inspect .64   .64   20    .053 .13   - --- inspect
bitvector/jain_5_false-no-overflow.i out of memory 0 --- inspect 260     260     15000   3200    10      0      error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (2) 0 --- inspect .022 .023 5.7 0     0   error (invalid witness file) 0 --- inspect .97 .65 47 0   0    error (invalid witness file) 0 --- inspect .0049 .0062 .40 0     0      - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .084 .075 9.4 .73 .0082 0      false(no-overflow) 1 wit inspect 5.0  3.0  290 0   0   false(no-overflow) 1 --- inspect 7.1   4.0   310   .66  0   unknown 0 --- inspect 3.7  2.2  250 0   1.1  false(no-overflow) 1 --- inspect .61   .62   20    .057 1.5    - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .081 .071 9.2 .71 .0082 0      false(no-overflow) 1 wit inspect 5.2  3.0  290 0   0   false(no-overflow) 1 --- inspect 7.0   4.5   300   .62  0   unknown 0 --- inspect 3.8  2.3  250 0   1.1  false(no-overflow) 1 --- inspect .61   .62   20    .057 1.4    - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .071 .062 10   .56 .0082 0      false(no-overflow) 1 wit inspect 3.9  2.1  250 0   0   error 0 --- inspect 7.3   4.6   320   .62  0   false(no-overflow) 1 --- inspect 3.7  2.1  250 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .049 1.4    - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  .11  6.3 1.2  .082  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.4   5.5   310   .66 0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  .12  6.5 1.1  .082  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.6   5.3   310   .66 0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  .11  6.8 1.7  .090  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.3   310   .62 0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .25  .25  8.3 2.1  .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.5   320   .66 0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .49  .49  21   6.2  .057  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7   4.5   310   .62 0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .52  .51  21   7.0  .057  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.5   5.2   310   .66 0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .062 .058 6.9 .58 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     470   .66 0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .16  .15  6.4 .93 .082  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8   5.4   310   .66 0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 --- inspect 880     880     650   3500    7.7    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 --- inspect 880     880     960   4500    8.6    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .028 5.6 0    0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 --- inspect 880     880     1300   5000    10      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 --- inspect 250     250     15000   2900    8.0    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i error (42) 0 --- inspect 880     880     1300   3800    10      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 error (42) 0 --- inspect 880     880     1300   4300    14      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 45     45     1100   430    3.8    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 36     27     510   .66 0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .099 .095 6.7 .67 .053  0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.1   4.5   300   .62 0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .11  .10  6.8 .78 .061  0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 8.6   4.7   300   .62 0  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .22  .22  7.2 2.2  .17   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.3   5.6   300   .66 0  
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 --- inspect 880     880     5200   3400    5.6    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 --- inspect 880     880     5300   3700    5.2    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0  
psyco/psyco_abp_1_false-no-overflow.c error (42) 0 --- inspect 880     880     1600   6000    14      0      error (invalid witness file) 0 --- inspect .67 .41 41 0   0   error (2) 0 --- inspect .024 .026 5.6 0     0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0    error (invalid witness file) 0 --- inspect .0053 .0072 .51 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 38000   38000   270000 250000 360    .0082 19 -82 190 110 6400 0   0   19 13 200 120 6300 10   0   19 9 73 42 4400 0   15 19 17 11 11 350 .96 14 60 26 380 240 7500 10   0  
    correct results 30 43 4.8 4.5 290 45 1.5  0      14 14 90 50 4100 0   0   13 13 110 62 4000 7.8 0   9 9 35 21 2200 0   11 17 17 11 11 350 .96 14 13 26 330 200 6100 8.4 0  
        correct true 13 26 3.1 3.0 130 33 1.2  0      0 0 0 0 13 26 330 200 6100 8.4 0  
        correct false 17 17 1.7 1.5 160 12 .29 0      14 14 90 50 4100 0   0   13 13 110 62 4000 7.8 0   9 9 35 21 2200 0   11 17 17 11 11 350 .96 14 0
    correct-unconfimed results 3 3 45   45   1100 430 3.9  0      0 0 0 0 0
        correct-unconfirmed true 3 3 45   45   1100 430 3.9  0      0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 3 -96 96 56 2200 0   0   0 0 0 0
        incorrect true 0 3 -96 96 56 2200 0   0   0 0 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 46 -82 13 9 17 26
Run set cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-nooverflow.NoOverflows-Other