Tool 2LS 0.7.2-sv-comp19 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:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-2ls.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 error (5) 0 --- inspect .10  .099 25 .68 0     0     error (invalid witness file) 0 --- inspect .68 .40 41 0   0   error (2) 0 --- inspect .023 .025 5.8 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0    error (invalid witness file) 0 --- inspect .0058 .0072 .53 0     0    - --- inspect
recursive/Addition03_false-no-overflow.c error (5) 0 --- inspect .10  .10  24 .75 0     0     error (invalid witness file) 0 --- inspect .63 .39 42 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0    error (invalid witness file) 0 --- inspect .0021 .0026 .40 0     0    - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) 0 --- inspect .090 .090 24 .86 0     0     error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0    error (invalid witness file) 0 --- inspect .0051 .0063 .52 0     0    - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) 0 --- inspect .090 .089 24 .87 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .089 .089 24 .87 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) 0 --- inspect .086 .087 24 1.4  0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .042 .043 5.6 0    0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) 0 --- inspect .12  .12  24 .71 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .084 .085 24 .88 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .027 5.5 0    0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .11  .11  24 .70 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .087 .087 23 1.0  0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .11  .10  24 .75 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .10  .10  23 .66 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .031 5.6 0    0  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .094 .094 24 .74 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) 0 --- inspect .095 .094 24 .83 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .095 .095 24 .68 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .083 .083 24 .87 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .083 .082 24 .85 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.8 0    0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .085 .084 24 .80 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .087 .087 24 .88 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .088 .087 24 .97 0     0     - --- 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 (5) 0 --- inspect .11  .11  24 .80 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) 0 --- inspect .11  .11  24 .94 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .086 .087 24 .86 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .085 .085 24 .88 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .086 .086 24 .81 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.8 0    0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .10  .099 24 .63 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .031 5.5 0    0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 --- inspect .086 .086 24 .76 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive-simple/id_b3_o2_false-no-overflow.c error (5) 0 --- inspect .084 .085 24 .81 0     0     error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .65 48 0   0    error (invalid witness file) 0 --- inspect .0018 .0024 .40 0     0    - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c error (5) 0 --- inspect .094 .093 24 .65 0     0     error (invalid witness file) 0 --- inspect .77 .46 41 0   0   error (2) 0 --- inspect .052 .053 5.5 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0023 .0032 .53 0     0    - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c error (5) 0 --- inspect .12  .12  24 .77 0     0     error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .66 46 0   0    error (invalid witness file) 0 --- inspect .0021 .0027 .53 0     0    - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c error (5) 0 --- inspect .085 .086 24 .81 0     0     error (invalid witness file) 0 --- inspect .70 .42 40 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0    error (invalid witness file) 0 --- inspect .0018 .0023 .52 0     0    - --- inspect
recursive-simple/sum_non_false-no-overflow.c error (5) 0 --- inspect .11  .11  24 .71 0     0     error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0    error (invalid witness file) 0 --- inspect .0049 .0065 .52 0     0    - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .087 .086 24 .74 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .10  .10  24 .59 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .094 .094 24 .75 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .091 .092 24 .72 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .093 .092 23 1.2  0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .032 5.6 0    0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .082 .083 24 .79 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .091 .092 24 .87 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .025 5.7 0    0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .12  .12  24 .64 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 error (5) 0 --- inspect .092 .092 24 .72 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .089 .088 24 .72 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .096 .097 24 .85 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .095 .094 24 .67 0     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 error (5) 0 --- inspect .088 .088 24 .75 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .051 .052 5.5 0    0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .092 .092 23 .76 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .091 .091 24 .70 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.5 0    0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c error (5) 0 --- inspect .087 .086 23 .95 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .36  .35  24 3.8  0     0     timeout 0 wit inspect 92    78    1000 0   0   true -32 --- inspect 8.7   4.8   310   .62 0   true -32 --- inspect 5.1  2.9  260 0   .93 false(no-overflow) 1 --- inspect .71   .71   21    .086 1.5  - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .37  .36  24 4.0  0     0     timeout 0 wit inspect 92    78    920 0   0   true -32 --- inspect 8.4   5.1   310   .62 0   true -32 --- inspect 5.4  3.0  270 0   1.1  false(no-overflow) 1 --- inspect .71   .71   21    .086 1.4  - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .37  .36  24 4.3  0     0     true -32 wit inspect 6.7  3.6  280 0   0   true -32 --- inspect 8.2   5.0   300   .62 0   true -32 --- inspect 5.2  3.0  260 0   .96 false(no-overflow) 1 --- inspect .71   .71   21    .082 1.4  - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  24 1.0  0     0     false(no-overflow) 1 wit inspect 4.1  2.4  280 0   0   false(no-overflow) 1 --- inspect 7.3   4.1   310   .62 0   unknown 0 --- inspect 3.6  2.2  250 0   .96 false(no-overflow) 1 --- inspect .60   .60   20    .049 0    - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .10  24 1.4  0     0     false(no-overflow) 1 wit inspect 6.5  4.0  290 0   0   false(no-overflow) 1 --- inspect 7.2   4.5   310   .66 0   unknown 0 --- inspect 3.9  2.3  250 0   0    false(no-overflow) 1 --- inspect .61   .62   20    .053 1.5  - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .12  .11  24 1.1  0     0     false(no-overflow) 1 wit inspect 8.6  5.4  320 0   0   false(no-overflow) 1 --- inspect 7.3   4.6   310   .62 0   unknown 0 --- inspect 3.9  2.4  250 0   1.1  false(no-overflow) 1 --- inspect .62   .63   20    .053 1.4  - --- inspect
bitvector/jain_5_false-no-overflow.i timeout 0 --- inspect 900     900     1000 8800    .016 0     error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0   0    error (invalid witness file) 0 --- inspect .0039 .0049 .53 0     0    - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .14  .13  24 .99 0     0     false(no-overflow) 1 wit inspect 7.4  4.6  320 0   0   false(no-overflow) 1 --- inspect 7.4   4.2   310   .66 0   unknown 0 --- inspect 3.9  2.3  250 0   .80 false(no-overflow) 1 --- inspect .64   .64   20    .057 0    - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .16  .15  23 .97 0     0     false(no-overflow) 1 wit inspect 7.3  4.6  320 0   0   false(no-overflow) 1 --- inspect 7.3   4.2   310   .62 0   unknown 0 --- inspect 3.8  2.3  250 0   .96 false(no-overflow) 1 --- inspect .63   .63   20    .057 1.3  - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .13  .12  24 1.2  0     0     false(no-overflow) 1 wit inspect 4.6  2.5  250 0   0   error 0 --- inspect 7.9   4.4   310   .66 0   false(no-overflow) 1 --- inspect 3.8  2.3  250 0   .80 false(no-overflow) 1 --- inspect .60   .61   20    .049 .86 - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  .12  24 1.0  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   5.3   310   .62 0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .11  .11  25 1.7  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   5.0   310   .62 0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .12  .12  25 .90 0     .049 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.7   310   .62 0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  24 1.0  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.5   5.2   310   .62 0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  23 .87 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.6   310   .62 0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  24 .82 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   5.0   310   .62 0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect .37  .37  23 4.1  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16     11     490   .62 0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .098 .096 24 1.2  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.9   3.9   310   .62 0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .10  .098 23 1.2  0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   3.9   300   .62 0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .11  .10  24 .80 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   3.7   290   .66 0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .10  .099 24 .83 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.1   4.0   290   .62 0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .094 .092 24 .91 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   4.1   290   .66 0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .099 .098 23 .82 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   4.1   290   .62 0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect .10  .097 24 .82 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.6   4.6   290   .62 0  
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect .11  .11  24 .99 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 6.7   4.0   310   .62 0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect .13  .12  24 .73 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.4   4.4   300   .66 0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect .13  .13  23 .74 0     0     - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 6.8   4.4   300   .45 0  
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .10  24 .81 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2   4.4   300   .62 0  
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .13  .12  23 .67 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   3.6   300   .66 0  
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .10  24 .99 0     0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.3   4.0   300   .62 0  
psyco/psyco_abp_1_false-no-overflow.c timeout 0 --- inspect 900     900     7000 8200    .016 0     error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .022 .023 5.8 0    0   error (invalid witness file) 0 --- inspect .99 .65 47 0   0    error (invalid witness file) 0 --- inspect .0062 .0080 .53 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 1800    1800    9800 17000   .033 .049 19 -26 240   190   4400 0   0   19 -91 70 41 2800 5.7 0   19 -95 48   29   2700 0   7.6  19 9 5.9 5.9 190 .57 9.4 60 34 150 94 6500 12 0  
    correct results 26 43 4.0  3.8  620 38   0     .049 6 6 39   24   1800 0   0   5 5 37 22 1500 3.2 0   1 1 3.8 2.3 250 0   .80 9 9 5.8 5.8 180 .57 9.4 17 34 130 81 5300 11 0  
        correct true 17 34 2.1  2.1  400 19   0     .049 0 0 0 0 17 34 130 81 5300 11 0  
        correct false 9 9 1.9  1.8  210 19   0     0     6 6 39   24   1800 0   0   5 5 37 22 1500 3.2 0   1 1 3.8 2.3 250 0   .80 9 9 5.8 5.8 180 .57 9.4 0
    correct-unconfimed results 3 3 .37 .36 71 2.5 0     0     0 0 0 0 0
        correct-unconfirmed true 3 3 .37 .36 71 2.5 0     0     0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 1 -32 6.7 3.6 280 0   0   3 -96 25 15 920 1.9 0   3 -96 16   8.9 790 0   3.0  0 0
        incorrect true 0 1 -32 6.7 3.6 280 0   0   3 -96 25 15 920 1.9 0   3 -96 16   8.9 790 0   3.0  0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 46 -26 -91 -95 9 34
Run set 2ls.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-nooverflow.NoOverflows-Other