Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc-path.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 .069 .059 9.2 .52 .016  0      false(no-overflow) 1 wit inspect 4.9  2.7  260 0   0   false(no-overflow) 1 --- inspect 9.6   5.6   310   .66 0   false(no-overflow) 1 --- inspect 3.5  2.0  240 0   .80 false(no-overflow) 1 --- inspect .59   .60   20    .049 1.4  - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .066 .058 9.5 .47 .0082 0      false(no-overflow) 1 wit inspect 4.4  2.4  260 0   0   false(no-overflow) 1 --- inspect 8.0   4.8   310   .66 0   false(no-overflow) 1 --- inspect 4.2  2.5  250 0   1.8  false(no-overflow) 1 --- inspect .60   .60   20    .049 1.4  - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .12  .11  8.8 .31 .0082 0      false(no-overflow) 1 wit inspect 5.0  2.8  250 0   0   false(no-overflow) 1 --- inspect 7.6   4.3   310   .62 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   6.1  false(no-overflow) 1 --- inspect .59   .59   20    .049 0    - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     10000   12000    1900      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 error (42) 0 --- inspect 880     880     10000   11000    2000      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0    
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 870     880     11000   12000    1900      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0    
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     11000   11000    1900      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0    
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     3600   11000    810      .0041 - --- 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 error (42) 0 --- inspect 870     880     3600   12000    820      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0    
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     7100   11000    400      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0    
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c witness invalid (true) 0 wit inspect .054 .055 6.7 .48 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65 0    
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     280   10000    93      .070  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0    
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     280   12000    94      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .026 5.7 0    0    
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (42) 0 --- inspect 880     880     13000   11000    1400      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0    
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .19  .18  8.1 1.1  .15   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 38     23     960   .66 0    
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     13000   12000    1500      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0    
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     13000   11000    1500      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0    
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     13000   12000    1500      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0    
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 870     880     6200   12000    1300      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0    
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     6300   13000    1300      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0    
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 870     880     6100   10000    1400      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .035 5.6 0    0    
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 860     860     15000   12000    1300      .0082 - --- 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     12000   8100    820      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .033 5.5 0    0    
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 870     880     6900   11000    1500      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0    
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (42) 0 --- inspect 880     880     14000   13000    2500      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0    
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 2.5   2.5   16   35    4.4    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 79     51     960   .62 0    
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 2.6   2.6   16   32    4.5    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 79     51     1000   .62 0    
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .088 .073 8.6 .38 .0082 0      false(no-overflow) 1 wit inspect 3.8  2.1  260 0   0   false(no-overflow) 1 --- inspect 7.3   4.6   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.2  250 0   6.5  false(no-overflow) 1 --- inspect .60   .62   20    .045 1.4  - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .066 .055 9.6 .50 .0082 0      false(no-overflow) 1 wit inspect 5.0  2.7  260 0   0   false(no-overflow) 1 --- inspect 7.3   4.7   310   .66 0   false(no-overflow) 1 --- inspect 3.7  2.2  250 0   1.5  false(no-overflow) 1 --- inspect .59   .60   20    .045 1.1  - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .14  .12  8.1 .31 .0082 0      false(no-overflow) 1 wit inspect 4.4  2.4  250 0   0   false(no-overflow) 1 --- inspect 8.3   4.6   310   .66 0   false(no-overflow) 1 --- inspect 3.6  2.0  250 0   1.4  false(no-overflow) 1 --- inspect .62   .63   20    .045 1.4  - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .068 .060 9.1 .40 .016  0      false(no-overflow) 1 wit inspect 4.9  2.8  260 0   0   false(no-overflow) 1 --- inspect 7.0   4.4   300   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   1.9  false(no-overflow) 1 --- inspect .60   .60   20    .049 .24 - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .061 .051 9.8 .64 .0082 0      false(no-overflow) 1 wit inspect 4.2  2.4  260 0   0   false(no-overflow) 1 --- inspect 8.2   4.7   310   .66 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   6.4  false(no-overflow) 1 --- inspect .63   .63   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     550   10000    .19   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0    
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     550   11000    .19   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0    
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 870     880     550   10000    .20   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .047 .050 5.5 0    0    
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     540   9700    .18   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0    
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     540   11000    .23   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 error (42) 0 --- inspect 880     880     380   10000    380      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0    
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     380   12000    370      0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0    
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 870     880     390   10000    380      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 error (42) 0 --- inspect 870     880     790   10000    .26   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0    
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     790   12000    .24   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0    0    
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     780   10000    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .028 5.7 0    0    
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     790   11000    .24   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0    
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     800   9100    .18   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .034 5.7 0    0    
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     790   9800    .24   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0    
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     730   10000    .43   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0    
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (42) 0 --- inspect 880     880     720   9000    .40   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0    
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .30  .29  12   3.1  1.8    0      true -32 wit inspect 40    24    1200 0   0   error 0 --- inspect 25     14     730   .62 0   unknown 0 --- inspect 6.2  3.4  290 0   0    false(no-overflow) 1 --- inspect .72   .74   21    .086 1.1  - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .29  .28  12   3.3  1.8    0      true -32 wit inspect 35    21    1200 0   0   error 0 --- inspect 26     15     740   .66 0   unknown 0 --- inspect 6.4  3.5  280 0   0    false(no-overflow) 1 --- inspect .70   .71   21    .086 1.4  - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .68  .67  24   9.0  5.1    0      true -32 wit inspect 36    22    1100 0   0   error 0 --- inspect 32     20     720   .66 0   unknown 0 --- inspect 7.6  4.1  310 0   0    false(no-overflow) 1 --- inspect .70   .70   21    .082 1.0  - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .065 .054 9.0 .37 .0082 0      false(no-overflow) 1 wit inspect 5.6  3.3  290 0   0   false(no-overflow) 1 --- inspect 7.1   4.0   310   .66 0   unknown 0 --- inspect 3.8  2.3  250 0   .80 false(no-overflow) 1 --- inspect .66   .67   20    .049 1.9  - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .067 .057 9.3 .48 .0082 0      false(no-overflow) 1 wit inspect 5.8  3.4  290 0   0   false(no-overflow) 1 --- inspect 6.9   3.9   300   .66 0   unknown 0 --- inspect 3.7  2.3  250 0   5.6  false(no-overflow) 1 --- inspect .62   .62   20    .053 1.3  - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .10  .091 9.2 .46 .0082 0      false(no-overflow) 1 wit inspect 6.5  3.9  350 0   0   false(no-overflow) 1 --- inspect 8.1   4.5   310   .66 0   unknown 0 --- inspect 4.0  2.3  250 0   1.2  false(no-overflow) 1 --- inspect .63   .65   20    .053 1.4  - --- inspect
bitvector/jain_5_false-no-overflow.i out of memory 0 --- inspect 190     190     15000   2800    10      0      error (invalid witness file) 0 --- inspect .68 .43 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0    error (invalid witness file) 0 --- inspect .0050 .0062 .53 0     0    - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .084 .073 9.4 .48 .0082 0      false(no-overflow) 1 wit inspect 4.8  2.9  290 0   0   false(no-overflow) 1 --- inspect 7.8   4.4   310   .66 0   unknown 0 --- inspect 3.6  2.1  250 0   1.4  false(no-overflow) 1 --- inspect .62   .63   20    .057 1.4  - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .075 .066 9.1 .49 .0082 0      false(no-overflow) 1 wit inspect 5.7  3.3  290 0   0   false(no-overflow) 1 --- inspect 7.3   4.1   310   .62 0   unknown 0 --- inspect 3.8  2.2  250 0   1.4  false(no-overflow) 1 --- inspect .62   .62   20    .057 .94 - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .061 .054 9.7 .69 .0082 0      false(no-overflow) 1 wit inspect 4.7  2.6  250 0   0   error 0 --- inspect 8.2   4.9   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   .32 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 .34  .33  12   5.1  2.5    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2   5.1   310   .62 0    
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .35  .34  14   4.3  2.5    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   4.7   310   .66 0    
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 1.5   1.4   42   21    13      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   5.1   310   .66 0    
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .24  .24  8.4 2.4  .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.5   5.6   310   .62 .086
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .72  .72  21   9.0  .20   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.0   5.1   310   .62 0    
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .76  .76  21   11    .20   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   5.1   310   .66 0    
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .073 .068 6.9 .48 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     460   .66 0    
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i witness invalid (true) 0 wit inspect .11  .10  6.4 .89 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.2   3.2   270   .61 0    
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 110     110     15000   1700    6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0    
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 120     110     15000   1700    6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0    
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 120     120     15000   1600    6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0    
bitvector/jain_5_true-unreach-call_true-no-overflow.i out of memory 0 --- inspect 190     190     15000   2800    .61   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0    0    
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 130     130     15000   1800    6.4    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0    
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i out of memory 0 --- inspect 130     130     15000   1600    2.5    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .029 5.6 0    0    
bitvector/modulus_true-unreach-call_true-no-overflow.i error (42) 0 --- inspect 880     880     12000   8800    .35   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0    
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .10  .099 6.4 .77 .053  0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.9   4.5   320   .62 0    
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 1.4   1.4   71   22    14      0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.8   4.3   310   .62 0    
bitvector/parity_true-unreach-call_true-no-overflow.i witness invalid (true) 0 wit inspect .41  .41  8.1 5.4  .14   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 6.4   3.4   270   .65 3.8  
bitvector/sum02_false-unreach-call_true-no-overflow.i error (42) 0 --- inspect 880     880     250   6400    .95   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0    
bitvector/sum02_true-unreach-call_true-no-overflow.i error (42) 0 --- inspect 870     880     260   8800    .94   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0    0    
psyco/psyco_abp_1_false-no-overflow.c out of memory 0 --- inspect 840     840     15000   9300    2500      .0041 error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .64 47 0   0    error (invalid witness file) 0 --- inspect .0049 .0060 .57 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 39 36000   36000   320000 440000 30000   .10 19 -82 180 110 7400 0   0   19 13 190 110 6500 11   0   19 9 74 43 4400 0   37 19 17 11 11 350 .95 20 60 20 300 190 7000 9.5 3.9  
    correct results 27 37 12   11   340 140 37   0    14 14 70 40 3800 0   0   13 13 100 59 4000 8.4 0   9 9 33 19 2200 0   27 17 17 11 11 350 .95 20 10 20 270 170 5300 6.4 .086
        correct true 10 20 9.2 9.2 170 120 28   0    0 0 0 0 10 20 270 170 5300 6.4 .086
        correct false 17 17 2.4 2.2 180 22 8.8 0    14 14 70 40 3800 0   0   13 13 100 59 4000 8.4 0   9 9 33 19 2200 0   27 17 17 11 11 350 .95 20 0
    correct-unconfimed results 2 2 1.5 1.5 77 23 14   0    0 0 0 0 0
        correct-unconfirmed true 2 2 1.5 1.5 77 23 14   0    0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 3 -96 110 66 3600 0   0   0 0 0 0
        incorrect true 0 3 -96 110 66 3600 0   0   0 0 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 39 -82 13 9 17 20
Run set cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-nooverflow.NoOverflows-Other