Tool ULTIMATE Taipan 0.1.23-635dfa2a 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-08 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-09 21:17:48 CET 2018-12-12 21:23:28 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other
Options --full-output -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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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 8.4 2.7 370 57 .66 0      false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0   false(no-overflow) 1 --- inspect 8.2   4.6   310   .62 0      unknown 0 --- inspect 3.7  2.2  250 0   0      error (2) 0 --- inspect .60   .61   20    .049 1.4    - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 7.7 2.9 360 62 .66 0      false(no-overflow) 1 wit inspect 3.9  2.2  260 0   0   false(no-overflow) 1 --- inspect 7.0   4.4   300   .62 0      unknown 0 --- inspect 3.8  2.2  250 0   .80   error (2) 0 --- inspect .61   .61   20    .049 0      - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 8.4 3.2 370 69 .66 0      false(no-overflow) 1 wit inspect 3.6  2.0  250 0   0   false(no-overflow) 1 --- inspect 7.6   4.8   310   .62 0      unknown 0 --- inspect 3.7  2.2  250 0   .0041 true -32 --- inspect .60   .60   20    .049 0      - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   610   7800 7500 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   670   7500 11000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   680   7200 8500 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   670   7500 7200 .62 .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .029 5.6 0    0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   720   2000 11000 .64 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 timeout 0 --- inspect 900   720   1800 13000 .64 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 timeout 0 --- inspect 900   760   1400 12000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0    0     
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.8 3.0 350 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   4.3   310   .62 0     
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 13   4.9 530 110 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     9.1   490   .62 0     
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 14   4.9 520 130 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     9.5   500   .62 0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   750   5500 14000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 140   74   6100 1400 .60 .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 35     21     1200   .62 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   750   5200 11000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.7 0    0     
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   750   4900 10000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.7 0    0     
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   760   5200 10000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 9.9 3.2 420 74 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10     5.8   330   .66 .0082
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.7 3.2 380 73 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.9   5.7   320   .62 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 910   200   14000 5200 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 910   230   14000 5100 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0    0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.7 3.1 350 64 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7   5.4   310   .66 0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 17   6.2 660 140 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     9.8   520   .62 0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   720   5200 9000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .030 5.7 0    0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (7) 0 --- inspect 140   120   2300 2000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (7) 0 --- inspect 110   87   2400 1400 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect 7.8 3.0 360 56 .66 .0041 false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0   false(no-overflow) 1 --- inspect 7.9   4.5   310   .66 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .59   .59   20    .045 0      - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect 8.2 2.7 370 67 .66 0      false(no-overflow) 1 wit inspect 3.8  2.1  260 0   0   false(no-overflow) 1 --- inspect 9.3   5.5   310   .62 0      unknown 0 --- inspect 3.9  2.3  250 0   0      true -32 --- inspect .59   .59   20    .045 0      - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect 8.0 2.7 380 56 .66 0      false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0   false(no-overflow) 1 --- inspect 7.1   4.6   310   .62 .0041 unknown 0 --- inspect 4.1  2.4  250 0   0      true -32 --- inspect .60   .60   20    .045 0      - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect 8.2 2.8 370 72 .66 0      false(no-overflow) 1 wit inspect 3.9  2.2  260 0   0   false(no-overflow) 1 --- inspect 8.1   4.6   310   .62 0      unknown 0 --- inspect 4.0  2.4  250 0   0      true -32 --- inspect .61   .61   20    .049 0      - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect 8.9 2.9 370 73 .66 0      false(no-overflow) 1 wit inspect 3.7  2.1  250 0   0   false(no-overflow) 1 --- inspect 8.7   4.9   310   .62 0      unknown 0 --- inspect 3.6  2.2  240 0   .82   true -32 --- inspect .63   .63   20    .049 .0041 - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.9 3.0 370 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8   4.3   300   .62 0     
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.0 2.6 360 50 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3   4.1   310   .62 .0082
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.7 2.6 350 57 .66 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2   4.4   300   .66 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.1 2.6 370 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   3.9   300   .66 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.9 2.6 340 55 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   3.8   300   .66 0     
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.9 3.3 390 81 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.3   5.2   320   .62 .0041
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.8 3.4 390 77 .66 .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.4   5.3   320   .62 0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 9.8 3.3 400 79 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.5   5.4   320   .62 .0041
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.2 2.6 370 58 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.8   4.7   300   .66 0     
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.5 2.6 370 55 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   3.7   300   .62 0     
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.7 2.9 360 56 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   3.7   300   .62 0     
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.2 2.7 360 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.3   3.7   290   .62 0     
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.0 2.5 340 56 .66 .53   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.8   290   .66 0     
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 8.1 2.7 370 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.9   4.3   280   .62 0     
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.9 2.7 370 61 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8   4.2   300   .66 .0082
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 7.7 2.9 360 60 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.9   4.0   300   .62 0     
bitvector/byte_add_1_false-no-overflow.i error (7) 0 --- inspect 12   4.4 490 97 .66 .0082 error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0      error (invalid witness file) 0 --- inspect .98 .65 47 0   0      error (invalid witness file) 0 --- inspect .0050 .0065 .53 0     0      - --- inspect
bitvector/byte_add_2_false-no-overflow.i error (7) 0 --- inspect 13   4.2 510 110 .66 .0082 error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .025 .027 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .62 48 0   0      error (invalid witness file) 0 --- inspect .0059 .0074 .52 0     0      - --- inspect
bitvector/byte_add_false-no-overflow.i error 0 --- inspect 64   22   850 540 .62 0      error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .95 .60 47 0   0      error (invalid witness file) 0 --- inspect .0021 .0027 .52 0     0      - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 7.6 2.6 360 62 .66 0      false(no-overflow) 1 wit inspect 5.3  3.1  290 0   0   false(no-overflow) 1 --- inspect 6.8   4.3   310   .62 0      unknown 0 --- inspect 3.8  2.3  250 0   0      false(no-overflow) 1 --- inspect .61   .61   20    .045 0      - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 7.5 2.6 350 63 .66 .0041 false(no-overflow) 1 wit inspect 4.7  2.8  290 0   0   false(no-overflow) 1 --- inspect 6.9   4.3   300   .62 0      unknown 0 --- inspect 4.0  2.4  250 0   0      false(no-overflow) 1 --- inspect .59   .59   20    .049 0      - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 7.1 2.6 330 57 .66 0      false(no-overflow) 1 wit inspect 4.8  2.9  290 0   0   false(no-overflow) 1 --- inspect 8.3   4.7   310   .62 0      unknown 0 --- inspect 3.8  2.3  250 0   0      false(no-overflow) 1 --- inspect .62   .62   20    .049 0      - --- inspect
bitvector/jain_5_false-no-overflow.i error (7) 0 --- inspect 680   660   2400 8900 .62 0      error (invalid witness file) 0 --- inspect .68 .43 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .96 .61 47 0   0      error (invalid witness file) 0 --- inspect .0049 .0061 .52 0     0      - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 8.1 3.1 360 69 .66 0      false(no-overflow) 1 wit inspect 4.8  2.8  280 0   0   false(no-overflow) 1 --- inspect 6.9   4.4   310   .62 0      unknown 0 --- inspect 4.7  2.8  250 0   .79   false(no-overflow) 1 --- inspect .60   .60   20    .053 1.4    - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 7.7 2.6 370 61 .66 0      false(no-overflow) 1 wit inspect 4.8  2.8  290 0   0   false(no-overflow) 1 --- inspect 8.3   4.9   300   .62 0      unknown 0 --- inspect 3.9  2.4  250 0   .93   false(no-overflow) 1 --- inspect .61   .60   20    .053 0      - --- inspect
bitvector/modulus_false-no-overflow.i error 0 --- inspect 7.0 2.5 340 61 .66 0      error (invalid witness file) 0 --- inspect .61 .39 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0      error (invalid witness file) 0 --- inspect .98 .64 49 0   0      error (invalid witness file) 0 --- inspect .0047 .020  .52 0     0      - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 8.2 2.9 350 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.5   5.7   310   .62 .012 
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 7.7 2.8 350 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.4   4.8   310   .62 0     
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 8.6 2.9 360 72 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2   5.0   310   .62 0     
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.7 3.0 360 69 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.2   4.7   310   .62 .012 
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.9 2.9 380 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   5.1   310   .62 0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.9 3.0 380 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.5   5.2   310   .62 0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 14   5.2 510 130 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16     10     510   .62 .0082
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 8.5 2.8 370 57 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.9   3.8   300   .66 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 6.9 2.6 330 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   4.2   290   .66 0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 8.8 2.8 370 68 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   4.1   290   .66 .0041
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 7.6 2.5 370 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   4.1   290   .66 .0082
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.1 2.6 330 65 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7   4.2   300   .66 0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 7.1 2.9 330 57 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.9   290   .66 0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 7.4 2.9 330 54 .66 .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   4.2   300   .66 0     
bitvector/modulus_true-unreach-call_true-no-overflow.i error 0 --- inspect 7.3 2.6 340 57 .66 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 error 0 --- inspect 7.7 2.6 360 54 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i error 0 --- inspect 7.3 2.6 340 57 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0     
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.9 2.6 370 66 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.5   4.2   300   .66 .0082
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 7.2 2.8 330 59 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.4   4.1   290   .62 0     
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.6 2.6 340 56 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.9   4.3   290   .66 0     
psyco/psyco_abp_1_false-no-overflow.c timeout 0 --- inspect 900   770   5400 12000 .63 .36   error (invalid witness file) 0 --- inspect .68 .42 41 0   0   error (2) 0 --- inspect .026 .026 5.6 0    0      error (invalid witness file) 0 --- inspect 1.1  .71 46 0   0      error (invalid witness file) 0 --- inspect .0054 .0065 .52 0     0      - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 79 95 15000 11000 130000 160000 51   .96   19 13 59 34 3700 0   0   19 13 100 61 4000 8.1 .0041 19 0 57 34 3500 0   3.3 19 -187 7.9 7.9 270 .63 2.8    60 82 370 220 14000 26 .086
    correct results 54 95 590 230 26000 5000 35   .56   13 13 55 32 3500 0   0   13 13 100 61 4000 8.1 .0041 0 5 5 3.0 3.0 100 .25 1.4    41 82 370 220 14000 26 .086
        correct true 41 82 490 200 21000 4100 27   .55   0 0 0 0 41 82 370 220 14000 26 .086
        correct false 13 13 100 36 4700 830 8.5 .0082 13 13 55 32 3500 0   0   13 13 100 61 4000 8.1 .0041 0 5 5 3.0 3.0 100 .25 1.4    0
    incorrect results 0 0 0 0 6 -192 3.6 3.6 120 .28 .0041 0
        incorrect true 0 0 0 0 6 -192 3.6 3.6 120 .28 .0041 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 95 13 13 0 -187 82
Run set utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-nooverflow.NoOverflows-Other