Tool DepthK 3.1 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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] 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-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other
Options -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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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 .19 .18 33 1.7 1.0  0      false(no-overflow) 1 wit inspect 4.5  2.5  260 0   0   false(no-overflow) 1 --- inspect 8.1   4.5   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .13 33 1.7 1.0  0      false(no-overflow) 1 wit inspect 5.7  3.1  270 0   0   false(no-overflow) 1 --- inspect 7.3   4.2   310   .66 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 1.4    - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .14 34 1.6 1.0  0      false(no-overflow) 1 wit inspect 3.9  2.1  260 0   0   false(no-overflow) 1 --- inspect 7.6   4.3   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   .80 false(no-overflow) 1 --- inspect .62   .61   20    .049 .14   - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 220    200    15000 2500   31    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 560   440   7000 .64 0   
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    200    15000 2800   26    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 470   370   7000 .64 0   
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 220    200    15000 2700   31    0      - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 620   490   7000 .62 .19
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 220    200    15000 2600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 710   560   7000 .63 0   
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    210    15000 3200   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   800   3200 .63 0   
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    210    15000 2800   26    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   800   3600 .63 0   
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    210    15000 2800   26    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   790   2900 .63 0   
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .78 .53 66 9.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.3 3.6 300 .66 0   
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .90 .65 65 8.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14   8.8 490 .66 0   
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .91 .64 69 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15   9.4 460 .62 0   
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c out of memory 0 wit inspect 180    170    15000 2600   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   900   5000 1.0  0   
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .79 .54 66 8.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 34   22   1100 .62 0   
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 180    170    15000 2300   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   890   5300 .64 0   
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 180    170    15000 2500   26    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   890   5800 .65 0   
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 180    170    15000 2200   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   890   6400 .62 0   
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 170    160    15000 2500   26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 10   6.1 330 .66 0   
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 170    160    15000 2300   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12   7.2 340 .66 0   
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 200    190    15000 2500   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   810   1400 .63 0   
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c out of memory 0 wit inspect 220    210    15000 2700   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   820   1500 .64 0   
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 250    230    15000 3200   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.4 5.4 310 .62 0   
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 220    200    15000 2100   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15   9.7 480 .66 0   
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory 0 wit inspect 180    180    15000 2400   31    0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960   850   4500 1.0  0   
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .91 .64 66 9.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 83   53   850 .62 0   
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect .87 .62 66 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 90   57   980 .62 0   
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .14 34 1.5 1.0  0      false(no-overflow) 1 wit inspect 4.8  2.7  260 0   0   false(no-overflow) 1 --- inspect 7.5   4.7   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .60   .59   20    .045 0      - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .14 33 1.4 .85 0      false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 7.1   4.1   320   .66 0   false(no-overflow) 1 --- inspect 3.5  2.1  240 0   0    false(no-overflow) 1 --- inspect .63   .62   20    .045 0      - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .14 33 1.5 1.0  0      false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0   false(no-overflow) 1 --- inspect 7.8   4.4   310   .62 0   false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .045 0      - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .15 .14 33 1.9 1.0  0      false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0   false(no-overflow) 1 --- inspect 7.7   4.4   310   .62 0   false(no-overflow) 1 --- inspect 3.5  2.0  240 0   .80 false(no-overflow) 1 --- inspect .64   .64   20    .049 0      - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .14 .14 33 1.6 1.0  0      error 0 wit inspect 5.5  3.0  270 0   0   false(no-overflow) 1 --- inspect 8.9   5.1   310   .62 0   false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .049 0      - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .84 .58 66 8.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7 4.2 300 .66 0   
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .81 .56 67 9.1 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7 3.8 300 .62 0   
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .80 .55 67 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.0 300 .66 0   
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .82 .56 66 8.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 3.9 300 .66 0   
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .79 .53 67 9.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8 3.8 300 .66 0   
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .98 .70 66 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11   6.6 320 .66 0   
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .95 .69 66 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.9 5.5 310 .62 0   
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .95 .70 66 12   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.7 5.4 310 .62 0   
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .79 .53 66 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.2 4.0 290 .62 0   
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .77 .53 65 9.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.3 4.0 300 .66 0   
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .81 .54 65 8.2 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0 4.5 300 .66 0   
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .80 .54 66 8.6 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5 4.2 290 .66 0   
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .76 .52 65 8.2 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.3 300 .66 0   
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .80 .54 67 8.9 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6 4.2 290 .66 0   
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .80 .54 66 8.6 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.4 4.1 300 .66 0   
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect .79 .54 66 10   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5 3.6 300 .66 0   
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect .42 .41 35 5.6 31    0      false(no-overflow) 1 wit inspect 11    5.7  420 0   0   true -32 --- inspect 16     8.9   530   .62 0   true -32 --- inspect 4.8  2.7  260 0   0    false(no-overflow) 1 --- inspect .62   .63   20    .057 0      - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect .40 .40 36 4.9 31    0      false(no-overflow) 1 wit inspect 8.4  4.5  360 0   0   error 0 --- inspect 24     14     590   .62 0   true -32 --- inspect 4.9  2.8  260 0   .13 false(no-overflow) 1 --- inspect .63   .63   20    .057 1.5    - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect .45 .44 35 5.4 26    0      false(no-overflow) 1 wit inspect 14    7.6  440 0   0   true -32 --- inspect 8.4   4.9   300   .62 0   true -32 --- inspect 4.8  2.7  270 0   .13 false(no-overflow) 1 --- inspect .61   .61   20    .057 .39   - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .14 .14 33 1.7 1.0  0      false(no-overflow) 1 wit inspect 4.4  2.6  280 0   0   false(no-overflow) 1 --- inspect 6.5   3.8   300   .62 0   unknown 0 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .65   .64   20    .045 0      - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .16 .16 33 1.6 1.0  0      false(no-overflow) 1 wit inspect 5.1  3.0  280 0   0   false(no-overflow) 1 --- inspect 7.0   4.0   310   .62 0   unknown 0 --- inspect 3.7  2.3  250 0   0    false(no-overflow) 1 --- inspect .60   .60   20    .049 0      - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .14 .14 34 1.7 1.0  0      false(no-overflow) 1 wit inspect 4.9  2.9  280 0   0   false(no-overflow) 1 --- inspect 7.7   4.4   310   .66 0   unknown 0 --- inspect 3.8  2.2  250 0   0    false(no-overflow) 1 --- inspect .62   .62   20    .049 0      - --- inspect
bitvector/jain_5_false-no-overflow.i unknown 0 --- inspect 87    86    55 1300   3000    .041  error (invalid witness file) 0 --- inspect .65 .39 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .66 48 0   0    error (invalid witness file) 0 --- inspect .0025 .0033 .53 0     0      - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .14 .14 33 1.5 1.0  0      false(no-overflow) 1 wit inspect 4.7  2.8  280 0   0   false(no-overflow) 1 --- inspect 7.7   4.3   310   .66 0   unknown 0 --- inspect 3.8  2.3  250 0   .80 false(no-overflow) 1 --- inspect .60   .60   20    .049 0      - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .18 .18 34 1.5 1.0  0      false(no-overflow) 1 wit inspect 4.3  2.5  280 0   0   false(no-overflow) 1 --- inspect 7.1   4.1   310   .62 0   unknown 0 --- inspect 3.6  2.2  250 0   0    false(no-overflow) 1 --- inspect .61   .61   20    .049 .78   - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .16 .16 33 1.3 1.0  0      false(no-overflow) 1 wit inspect 4.5  2.5  250 0   0   error 0 --- inspect 6.8   3.9   300   .66 0   false(no-overflow) 1 --- inspect 4.2  2.5  250 0   0    false(no-overflow) 1 --- inspect .59   .59   20    .049 0      - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect .86 .61 66 9.4 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.0 5.4 320 .66 0   
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect .87 .60 66 9.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.9 5.5 310 .66 0   
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect .89 .63 67 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0 4.5 310 .62 0   
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.0  .79 66 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.4 5.3 320 .62 0   
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .95 .70 67 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.8 4.5 310 .66 0   
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .96 .71 67 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3 4.7 310 .62 0   
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 2.2  1.9  66 25   150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16   10   460 .62 0   
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .82 .55 66 11   31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8 4.3 310 .62 0   
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect .77 .53 66 8.0 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8 4.1 300 .62 0   
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect .78 .52 66 9.1 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5 4.0 290 .62 0   
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect .80 .56 65 7.5 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6 4.1 300 .62 0   
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .80 .55 65 7.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.4 3.6 290 .62 0   
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect .81 .53 67 9.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0 3.9 300 .62 0   
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect .81 .56 67 9.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7 3.7 300 .66 0   
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.3  1.0  66 16   26    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.1 4.5 320 .66 0   
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .80 .55 67 9.3 31    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.1 4.0 310 .66 0   
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .78 .53 66 9.1 26    0      - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 6.9 4.4 310 .66 0   
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .81 .56 67 9.8 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.1 4.0 310 .62 0   
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect .82 .55 66 8.6 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7 4.2 290 .66 0   
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect .82 .56 67 7.7 31    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6 3.8 280 .66 0   
psyco/psyco_abp_1_false-no-overflow.c unknown 0 --- inspect 900    900    640 13000   660    0      error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 48 0   0    error (invalid witness file) 0 --- inspect .0021 .0027 .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 17 4700   4500   270000 61000 5700 .045 19 16 99 55 5100 0   0   19 -51 150 88 5800 11   0   19 -87 68 40   4300 0   2.7  19 17 10 10 350 .84 4.2 60 86 13000 11000 84000 39 .19
    correct results 17 17 3.4 3.3 570 38 100 0     16 16 92 51 4700 0   0   13 13 98 56 4000 8.2 0   9 9 33 19   2200 0   1.6  17 17 10 10 340 .84 4.2 43 86 540 330 16000 28 0   
        correct true 0 0 0 0 0 43 86 540 330 16000 28 0   
        correct false 17 17 3.4 3.3 570 38 100 0     16 16 92 51 4700 0   0   13 13 98 56 4000 8.2 0   9 9 33 19   2200 0   1.6  17 17 10 10 340 .84 4.2 0
    incorrect results 0 0 2 -64 24 14 840 1.2 0   3 -96 15 8.2 780 0   .26 0 0
        incorrect true 0 0 2 -64 24 14 840 1.2 0   3 -96 15 8.2 780 0   .26 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 17 16 -51 -87 17 86
Run set depthk.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-nooverflow.NoOverflows-Other