Tool PeSCo 1.7-svn b8d6131600+ 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] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 3.2 1.4 280 30 0   0   false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0   false(no-overflow) 1 --- inspect 8.9 5.0 310 .66 0   false(no-overflow) 1 --- inspect 3.9 2.2  250 0   0    false(no-overflow) 1 --- inspect .60  .60  20 .049 0      - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 1.4 270 35 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.7 2.1  250 0   .80 false(no-overflow) 1 --- inspect .60  .60  20 .049 0      - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 1.3 270 26 0   0   false(no-overflow) 1 wit inspect 4.8  2.7  250 0   0   false(no-overflow) 1 --- inspect 8.7 5.3 310 .66 0   false(no-overflow) 1 --- inspect 3.5 2.1  250 0   0    false(no-overflow) 1 --- inspect .62  .62  20 .049 0      - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   880   4200 12000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 600     470     7000   .66 0     
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   880   4300 12000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 660     510     7000   .64 0     
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   880   3300 10000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 540     420     7000   .71 0     
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   880   4000 11000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect out of memory 0 --- inspect 630     490     7000   .63 0     
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   860   5500 11000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     790     3100   1.7  0     
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   5400 11000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   880   1900 11000 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 true 2 wit inspect 3.2 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.8   300   .66 0     
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   4000 12000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   5700 12000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0     
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 1 wit inspect 5.8 2.6 310 60 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     5700   .66 0     
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 670   660   770 6500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 33     20     1200   .66 0     
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 5.4 2.4 300 46 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     6500   .66 0     
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 4.8 2.1 300 43 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     5600   .66 0     
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 4.8 2.1 310 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     6500   .67 0     
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.6 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 12     6.5   330   .66 0     
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.7 1.6 290 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     6.0   330   .66 0     
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error 0 wit inspect 5.0 2.4 300 46 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     810     1100   .75 0     
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error 0 wit inspect 11   5.7 410 98 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     820     1500   .82 0     
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 3.5 1.6 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   4.8   310   .66 0     
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 4.0 1.8 300 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16     10     470   .62 0     
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   870   6200 10000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     850     4500   1.8  0     
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   4300 12000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   860   4000 10000 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 false(no-overflow) 1 wit inspect 3.2 1.4 280 32 0   0   false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0   false(no-overflow) 1 --- inspect 7.5 4.3 310 .62 0   false(no-overflow) 1 --- inspect 4.5 2.6  250 0   0    false(no-overflow) 1 --- inspect .61  .60  20 .045 0      - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 1.3 280 28 0   0   false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 7.4 4.6 310 .66 0   false(no-overflow) 1 --- inspect 3.9 2.3  250 0   0    false(no-overflow) 1 --- inspect .58  .58  20 .045 0      - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 1.4 280 27 0   0   false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 7.6 4.3 310 .62 0   false(no-overflow) 1 --- inspect 4.3 2.5  250 0   .80 false(no-overflow) 1 --- inspect .59  .59  20 .045 .0041 - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 1.4 280 31 0   0   false(no-overflow) 1 wit inspect 3.9  2.2  260 0   0   false(no-overflow) 1 --- inspect 7.8 4.5 320 .62 0   false(no-overflow) 1 --- inspect 3.5 2.1  250 0   0    false(no-overflow) 1 --- inspect .60  .61  20 .049 0      - --- inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 1.4 280 32 0   0   false(no-overflow) 1 wit inspect 4.3  2.4  260 0   0   false(no-overflow) 1 --- inspect 9.2 5.5 310 .66 0   false(no-overflow) 1 --- inspect 3.8 2.2  250 0   .80 false(no-overflow) 1 --- inspect .61  .61  20 .049 0      - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.3 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   4.7   300   .66 0     
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.3 1.5 280 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.8   300   .66 0     
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.4 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   4.3   300   .66 0     
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.3 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   4.1   300   .66 0     
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.2 1.4 280 28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.7   300   .66 0     
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.4 1.8 290 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1   5.6   320   .66 0     
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 4.4 1.9 300 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.1   5.1   320   .66 0     
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 5.1 2.3 310 48 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11     5.9   310   .62 0     
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.2 1.4 280 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.7   4.3   300   .66 0     
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.0 1.3 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   3.9   300   .66 .0041
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.4 270 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.2   4.0   300   .66 0     
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.3 270 28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.5   4.6   290   .66 0     
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.4 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   4.9   290   .66 0     
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.3 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.4   3.7   290   .66 0     
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.2 1.4 280 28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.8   4.3   300   .62 0     
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c true 2 wit inspect 3.1 1.3 280 27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.0   3.9   310   .66 0     
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect 6.6 2.6 320 56 0   0   false(no-overflow) 1 wit inspect 6.6  3.6  290 0   0   error 0 --- inspect 24   14   540 .62 0   true -32 --- inspect 4.8 2.7  260 0   0    false(no-overflow) 1 --- inspect .76  .75  21 .090 0      - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect 6.8 2.9 330 66 0   0   false(no-overflow) 1 wit inspect 6.1  3.3  270 0   0   error 0 --- inspect 30   17   570 .62 0   true -32 --- inspect 4.8 2.7  260 0   0    false(no-overflow) 1 --- inspect .74  .73  22 .090 0      - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect 7.2 2.9 350 74 0   0   false(no-overflow) 1 wit inspect 5.9  3.2  270 0   0   error 0 --- inspect 24   14   620 .62 0   true -32 --- inspect 6.2 3.5  280 0   .80 false(no-overflow) 1 --- inspect .72  .72  21 .086 0      - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 3.5 1.7 300 34 0   0   false(no-overflow) 1 wit inspect 4.4  2.6  280 0   0   false(no-overflow) 1 --- inspect 7.2 4.1 310 .66 0   false(no-overflow) 1 --- inspect 3.6 2.1  240 0   0    false(no-overflow) 1 --- inspect .63  .62  20 .049 0      - --- inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 3.4 1.6 300 34 0   0   false(no-overflow) 1 wit inspect 4.8  2.9  280 0   0   false(no-overflow) 1 --- inspect 7.1 4.5 310 .62 0   false(no-overflow) 1 --- inspect 3.6 2.1  250 0   .80 false(no-overflow) 1 --- inspect .61  .60  20 .053 0      - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 3.5 1.7 300 36 0   0   false(no-overflow) 1 wit inspect 4.3  2.5  290 0   0   false(no-overflow) 1 --- inspect 7.7 4.3 310 .62 0   false(no-overflow) 1 --- inspect 3.9 2.3  240 0   0    false(no-overflow) 1 --- inspect .62  .62  20 .053 1.4    - --- inspect
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   880   4000 11000 0   0   error (1) 0 --- inspect .65 .39 45 0   0   timeout 0 --- inspect 97   68   1100 1.5  0   unknown 0 --- inspect 1.1 .67 51 0   0    error (1) 0 --- inspect .075 .075 11 0     .0041 - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 3.5 1.7 300 31 0   0   false(no-overflow) 1 wit inspect 4.7  2.7  290 0   0   false(no-overflow) 1 --- inspect 7.9 4.5 310 .66 0   false(no-overflow) 1 --- inspect 3.8 2.2  250 0   .80 false(no-overflow) 1 --- inspect .62  .62  20 .057 0      - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 3.3 1.5 300 31 0   0   false(no-overflow) 1 wit inspect 4.2  2.4  290 0   0   false(no-overflow) 1 --- inspect 7.5 4.2 300 .62 0   false(no-overflow) 1 --- inspect 3.7 2.2  250 0   0    false(no-overflow) 1 --- inspect .63  .63  20 .057 0      - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect 2.9 1.3 270 30 0   0   false(no-overflow) 1 wit inspect 4.1  2.3  250 0   0   error 0 --- inspect 7.5 4.2 310 .62 0   false(no-overflow) 1 --- inspect 4.2 2.4  250 0   .26 false(no-overflow) 1 --- inspect .62  .62  20 .053 0      - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 3.8 1.6 270 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.6   5.4   310   .66 0     
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 4.0 1.7 290 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   5.2   310   .62 0     
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 4.0 1.6 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.6   310   .66 .0041
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.2 1.4 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.6   4.9   310   .62 0     
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.1 1.3 270 28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.3   4.8   310   .62 0     
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.1 1.3 270 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.0   5.0   310   .62 0     
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 4.4 1.8 300 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     470   .66 0     
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.0 1.3 270 27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 7.3   4.5   300   .62 0     
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.0 1.3 270 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   3.7   300   .66 0     
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.9 1.3 270 27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.8   290   .66 0     
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.1 1.3 270 25 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   3.8   300   .66 0     
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 270 26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   3.7   300   .66 0     
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 3.0 1.3 270 26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.7   4.2   290   .66 0     
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i true 2 wit inspect 2.9 1.3 270 26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   3.7   300   .62 0     
bitvector/modulus_true-unreach-call_true-no-overflow.i true 1 wit inspect 3.1 1.3 270 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.1   4.0   300   .66 0     
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 1 wit inspect 3.1 1.4 270 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.6   4.3   310   .66 0     
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 1 wit inspect 3.2 1.4 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error 0 --- inspect 7.8   4.3   310   .66 0     
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.1 1.3 270 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.5   3.7   300   .62 0     
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 3.0 1.3 270 27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 8.1   4.8   290   .66 0     
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.9 1.3 270 26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 6.6   3.7   300   .66 0     
psyco/psyco_abp_1_false-no-overflow.c timeout 0 wit inspect 910   880   8200 12000 0   0   error (1) 0 --- inspect .97 .56 48 0   0   timeout 0 --- inspect 97   61   3200 1.5  0   unknown 0 --- inspect 1.2 .75 51 0   0    error (1) 0 --- inspect .086 .087 12 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 102 14000 13000 84000 170000 0   0   19 17 80 45 4700 0   0   19 13 380 240 10000 14   0   19 -82 72 42   4400 0   5.1  19 17 11 11 370 .97 1.4 60 78 10000 8900 76000 37 .0082
    correct results 56 95 860 740 16000 8300 0   0   17 17 79 44 4600 0   0   13 13 100 60 4000 8.3 0   14 14 54 31   3500 0   4.3  17 17 11 11 350 .97 1.4 39 78 350 200 13000 25 .0082
        correct true 39 78 800 710 11000 7700 0   0   0 0 0 0 39 78 350 200 13000 25 .0082
        correct false 17 17 66 29 5000 630 0   0   17 17 79 44 4600 0   0   13 13 100 60 4000 8.3 0   14 14 54 31   3500 0   4.3  17 17 11 11 350 .97 1.4 0
    correct-unconfimed results 7 7 30 13 2000 280 0   0   0 0 0 0 0
        correct-unconfirmed true 7 7 30 13 2000 280 0   0   0 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0 0
    incorrect results 0 0 0 3 -96 16 8.9 800 0   .80 0 0
        incorrect true 0 0 0 3 -96 16 8.9 800 0   .80 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 102 17 13 -82 17 78
Run set pesco.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-nooverflow.NoOverflows-Other