Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 .12  .12  26 1.1  1.0  0   false(no-overflow) 1 wit inspect 4.8  2.7  260 0   0   false(no-overflow) 1 --- inspect 8.4   4.8   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 0      - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .091 .092 26 .85 1.0  0   false(no-overflow) 1 wit inspect 5.2  2.9  270 0   0   false(no-overflow) 1 --- inspect 8.4   5.0   310   .66 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .049 .51   - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .088 .088 26 .91 .85 0   false(no-overflow) 1 wit inspect 4.9  2.7  260 0   0   false(no-overflow) 1 --- inspect 8.1   4.6   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 0      - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 460     460     15000 4800    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0     
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 480     480     15000 5800    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 470     470     15000 5300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 --- inspect 470     460     15000 5300    .85 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 840     800     15000 7900    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0    0     
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 840     800     15000 8200    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 840     810     15000 9300    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .086 .087 26 1.1  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   4.2   300   .66 .0082
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     1100 12000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     1100 13000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900     890     8800 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.5 0    0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect .13  .12  26 1.4  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 41     25     1100   .62 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     890     8800 6700    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0     
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     890     8800 6200    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0     
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     890     8800 6700    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0     
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     6400 8000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.8 0    0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     6400 7400    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 --- inspect 760     750     15000 7400    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 --- inspect 230     220     15000 2600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     890 8100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     900     1200 7400    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900     890     13000 9100    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .032 .035 5.6 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.8   1.8   27 28    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 93     60     1100   .62 0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.8   1.8   27 24    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 80     51     1000   .62 0     
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .093 .094 26 .93 1.0  0   false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0   false(no-overflow) 1 --- inspect 7.7   4.4   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .045 0      - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .11  .11  26 .83 1.0  0   false(no-overflow) 1 wit inspect 4.2  2.4  260 0   0   false(no-overflow) 1 --- inspect 7.7   4.4   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.2  250 0   .80 false(no-overflow) 1 --- inspect .59   .60   20    .045 0      - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .11  .11  26 .77 1.0  0   false(no-overflow) 1 wit inspect 4.0  2.3  260 0   0   false(no-overflow) 1 --- inspect 7.8   4.4   310   .62 0   false(no-overflow) 1 --- inspect 3.4  2.0  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .045 1.5    - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .092 .096 26 1.4  1.0  0   false(no-overflow) 1 wit inspect 4.6  2.6  260 0   0   false(no-overflow) 1 --- inspect 9.0   5.4   310   .62 0   false(no-overflow) 1 --- inspect 3.9  2.3  250 0   .80 false(no-overflow) 1 --- inspect .59   .59   20    .049 1.4    - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .085 .085 26 1.2  .85 0   error 0 wit inspect 4.5  2.5  270 0   0   false(no-overflow) 1 --- inspect 8.5   5.0   310   .62 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .63   .64   20    .049 0      - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1100 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1100 11000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0    0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1100 9400    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1100 8900    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1100 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .032 5.6 0    0     
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     520 12000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     520 13000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.5 0    0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     900     530 13000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1000 9600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1000 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .028 5.7 0    0     
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1000 11000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1000 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0     
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     1000 9200    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0     
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     990 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.8 0    0     
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     980 9600    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900     890     980 11000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0    0     
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  27 1.2  .85 0   false(no-overflow) 1 wit inspect 11    6.0  420 0   0   true -32 --- inspect 18     10     530   .62 0   true -32 --- inspect 6.1  3.4  260 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .057 1.4    - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .12  .12  27 1.0  1.0  0   false(no-overflow) 1 wit inspect 10    5.2  360 0   0   error 0 --- inspect 28     16     510   .62 0   true -32 --- inspect 4.7  2.6  260 0   .80 false(no-overflow) 1 --- inspect .61   .62   20    .057 1.0    - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .14  .14  27 2.2  .85 0   false(no-overflow) 1 wit inspect 9.1  4.9  380 0   0   error 0 --- inspect 33     18     590   .62 0   true -32 --- inspect 4.9  2.7  270 0   .80 false(no-overflow) 1 --- inspect .61   .61   20    .057 .0041 - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .086 .087 26 .87 1.0  0   false(no-overflow) 1 wit inspect 5.0  3.0  280 0   0   false(no-overflow) 1 --- inspect 8.4   5.1   310   .62 0   unknown 0 --- inspect 3.6  2.2  250 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .045 .39   - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .083 .083 26 1.1  1.0  0   false(no-overflow) 1 wit inspect 4.6  2.7  290 0   0   false(no-overflow) 1 --- inspect 7.9   4.7   310   .62 0   unknown 0 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .049 0      - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .079 .079 26 .84 .85 0   false(no-overflow) 1 wit inspect 4.8  2.9  290 0   0   false(no-overflow) 1 --- inspect 7.1   4.5   300   .62 0   unknown 0 --- inspect 3.7  2.2  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect
bitvector/jain_5_false-no-overflow.i out of memory 0 --- inspect 830     820     15000 10000    .86 0   error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .026 .028 5.7 0    0   error (invalid witness file) 0 --- inspect .92 .59 46 0   0    error (invalid witness file) 0 --- inspect .0055 .0067 .52 0     0      - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .088 .089 26 .98 1.0  0   false(no-overflow) 1 wit inspect 5.5  3.2  280 0   0   false(no-overflow) 1 --- inspect 8.0   4.8   310   .66 0   unknown 0 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .59   .60   20    .049 1.5    - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .090 .092 26 1.0  .85 0   false(no-overflow) 1 wit inspect 4.4  2.5  290 0   0   false(no-overflow) 1 --- inspect 7.7   4.3   300   .66 0   unknown 0 --- inspect 3.8  2.3  250 0   0    false(no-overflow) 1 --- inspect .60   .60   20    .049 0      - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  26 .79 .85 0   false(no-overflow) 1 wit inspect 3.9  2.2  250 0   0   error 0 --- inspect 7.5   4.7   300   .62 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .049 1.4    - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .13  .13  27 1.6  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.4   310   .66 0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .13  .13  27 1.4  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9   5.3   310   .66 0     
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .17  .17  27 2.1  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8   5.8   310   .66 0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .52  .52  28 7.9  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10     6.2   310   .66 0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.2   9.2   42 140    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.4   4.8   310   .66 0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.2   9.2   43 110    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.8   5.7   310   .66 0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .084 .083 26 .84 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     11     470   .66 0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .095 .095 26 1.2  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   4.6   310   .66 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900     900     1400 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900     900     870 9800    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900     900     780 8500    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900     890     13000 11000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900     900     800 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900     900     1200 9500    .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 76     76     280 960    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 9.1   5.1   300   .66 .0082
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .12  .12  26 .93 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.4   4.2   310   .62 0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .13  .13  26 1.6  .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 8.9   5.2   300   .66 0     
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .76  .76  26 8.7  1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   4.5   300   .66 0     
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 --- inspect 900     900     1600 10000    .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0     
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900     900     1600 10000    1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
psyco/psyco_abp_1_false-no-overflow.c timeout 0 --- inspect 900     900     3700 11000    1.0  0   error (invalid witness file) 0 --- inspect .63 .39 41 0   0   error (2) 0 --- inspect .025 .027 5.5 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0    error (invalid witness file) 0 --- inspect .0047 .0061 .40 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 39000   38000   260000 430000 75   0   19 16 96 54 5000 0   0   19 -19 190 110 6000 11    0   19 -87 68 40   4300 0   3.2 19 17 10 10 350 .84 9.1 60 26 340 210 7600 10   .016 
    correct results 30 43 26   26   820 340 28   0   16 16 91 50 4600 0   0   13 13 100 61 4000 8.2  0   9 9 32 19   2200 0   1.6 17 17 10 10 350 .84 9.1 13 26 310 190 6400 8.4 .0082
        correct true 13 26 24   24   380 320 12   0   0 0 0 0 13 26 310 190 6400 8.4 .0082
        correct false 17 17 1.7 1.7 440 18 16   0   16 16 91 50 4600 0   0   13 13 100 61 4000 8.2  0   9 9 32 19   2200 0   1.6 17 17 10 10 350 .84 9.1 0
    correct-unconfimed results 3 3 77   77   330 960 2.9 0   0 0 0 0 0
        correct-unconfirmed true 3 3 77   77   330 960 2.9 0   0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 0 1 -32 18 10 530 .62 0   3 -96 16 8.8 780 0   1.6 0 0
        incorrect true 0 0 1 -32 18 10 530 .62 0   3 -96 16 8.8 780 0   1.6 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 46 16 -19 -87 17 26
Run set esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-nooverflow.NoOverflows-Other