Tool VeriFuzz 1.0.0 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-09 02:47:33 CET 2018-12-09 17:43:44 CET 2018-12-09 18:26:53 CET 2018-12-09 18:31:36 CET 2018-12-12 22:04:17 CET 2018-12-09 18:23:50 CET
Run set verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-verifuzz.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/verifuzz.2018-12-09_0247.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/verifuzz.2018-12-09_0247.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.6 2.3 150 41 .63 0      false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0      false(no-overflow) 1 --- inspect 7.1   4.0   300   .66 0      false(no-overflow) 1 --- inspect 3.4  2.0  240 0   .82 false(no-overflow) 1 --- inspect .59   .59   20    .049 0      - --- inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 3.5 2.1 160 35 .64 0      false(no-overflow) 1 wit inspect 4.1  2.2  270 0   0      false(no-overflow) 1 --- inspect 6.8   3.8   300   .66 0      false(no-overflow) 1 --- inspect 3.6  2.1  250 0   .80 false(no-overflow) 1 --- inspect .63   .63   20    .049 .0041 - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 3.5 2.2 150 43 .64 0      false(no-overflow) 1 wit inspect 3.7  2.0  250 0   0      false(no-overflow) 1 --- inspect 7.0   4.0   310   .66 0      false(no-overflow) 1 --- inspect 3.5  2.0  250 0   0    false(no-overflow) 1 --- inspect .60   .59   20    .049 0      - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 12000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.7 0   0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   910   150 13000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 13000 .60 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   910   150 13000 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   910   150 11000 .67 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   910   160 11000 .77 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   900   150 8800 .78 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (1) 0 --- inspect 3.0 1.7 150 32 .30 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 11000 .87 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 11000 .91 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   200 11000 .78 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   200 10000 .58 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   200 13000 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   200 13000 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 13000 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.7 0   0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   900   150 12000 1.7  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   200 13000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 --- inspect 900   910   200 13000 4.2  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   150 12000 .99 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   910   200 10000 1.0  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 --- inspect 4.2 1.9 200 39 .31 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   200 12000 .86 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 --- inspect 900   920   200 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 2.4 200 42 .63 .0041 false(no-overflow) 1 wit inspect 3.7  2.1  250 0   0      false(no-overflow) 1 --- inspect 7.2   4.1   310   .62 0      false(no-overflow) 1 --- inspect 3.6  2.1  240 0   .82 false(no-overflow) 1 --- inspect .60   .60   20    .045 .93   - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 2.3 200 39 .63 0      false(no-overflow) 1 wit inspect 4.2  2.3  260 0   .0041 false(no-overflow) 1 --- inspect 6.6   3.8   310   .62 .0082 false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    false(no-overflow) 1 --- inspect .60   .60   20    .045 0      - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 2.3 200 43 .63 0      false(no-overflow) 1 wit inspect 4.0  2.2  260 0   0      false(no-overflow) 1 --- inspect 7.4   4.2   310   .66 0      false(no-overflow) 1 --- inspect 3.6  2.1  250 0   .80 false(no-overflow) 1 --- inspect .59   .59   20    .045 0      - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect 3.7 2.2 150 34 .63 0      false(no-overflow) 1 wit inspect 3.9  2.2  260 0   0      false(no-overflow) 1 --- inspect 6.9   4.3   300   .66 .012  false(no-overflow) 1 --- inspect 3.6  2.1  250 0   0    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 3.8 2.2 150 33 .68 .15   false(no-overflow) 1 wit inspect 4.1  2.3  260 0   0      false(no-overflow) 1 --- inspect 7.5   4.3   310   .66 0      false(no-overflow) 1 --- inspect 3.6  2.1  240 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 timeout 0 --- inspect 900   900   200 13000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 11000 .54 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 11000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   210 12000 1.2  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 1.3  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 11000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   250 9800 1.2  46      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.5 0   0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 12000 .59 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 13000 1.2  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   200 10000 .70 1.4    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 11000 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c timeout 0 --- inspect 900   900   150 11000 1.7  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
bitvector/byte_add_1_false-no-overflow.i false(no-overflow) 1 wit inspect 5.1 2.8 210 46 1.3  0      false(no-overflow) 1 wit inspect 9.0  4.7  410 0   0      true -32 --- inspect 8.3   5.0   310   .66 0      true -32 --- inspect 4.0  2.3  250 0   .80 false(no-overflow) 1 --- inspect .62   .62   20    .057 0      - --- inspect
bitvector/byte_add_2_false-no-overflow.i false(no-overflow) 1 wit inspect 5.0 2.7 210 49 1.3  0      false(no-overflow) 1 wit inspect 9.8  5.2  410 0   0      true -32 --- inspect 7.9   4.5   310   .62 0      true -32 --- inspect 4.0  2.3  250 0   .80 false(no-overflow) 1 --- inspect .61   .61   20    .057 .033  - --- inspect
bitvector/byte_add_false-no-overflow.i false(no-overflow) 1 wit inspect 5.2 2.8 210 47 1.6  0      false(no-overflow) 1 wit inspect 9.8  5.2  420 0   0      true -32 --- inspect 7.7   4.4   310   .62 0      true -32 --- inspect 3.9  2.3  250 0   .80 false(no-overflow) 1 --- inspect .61   .61   20    .057 0      - --- inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 3.5 2.1 160 35 .54 0      false(no-overflow) 1 wit inspect 8.6  6.3  560 0   0      false(no-overflow) 1 --- inspect 6.8   4.3   300   .66 0      false(no-overflow) 1 --- inspect 3.8  2.2  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 3.5 2.1 150 35 .55 0      false(no-overflow) 1 wit inspect 8.1  5.7  420 0   0      false(no-overflow) 1 --- inspect 7.2   4.5   310   .66 0      false(no-overflow) 1 --- inspect 3.8  2.2  250 0   0    false(no-overflow) 1 --- inspect .60   .60   20    .049 .033  - --- inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 3.4 2.0 150 31 .56 0      false(no-overflow) 1 wit inspect 7.5  5.4  390 0   0      false(no-overflow) 1 --- inspect 7.0   4.4   310   .66 0      false(no-overflow) 1 --- inspect 3.7  2.2  250 0   0    false(no-overflow) 1 --- inspect .60   .59   20    .049 0      - --- inspect
bitvector/jain_5_false-no-overflow.i timeout 0 --- inspect 900   920   150 11000 .67 0      error (invalid witness file) 0 --- inspect .59 .35 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0      error (invalid witness file) 0 --- inspect .91 .59 46 0   0    error (invalid witness file) 0 --- inspect .0017 .0022 .52 0     0      - --- inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 3.4 2.1 150 37 .56 0      false(no-overflow) 1 wit inspect 9.7  7.5  470 0   0      true -32 --- inspect 6.8   3.8   300   .66 0      false(no-overflow) 1 --- inspect 3.9  2.2  250 0   .80 false(no-overflow) 1 --- inspect .62   .62   20    .053 0      - --- inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 3.5 2.1 150 37 .56 0      false(no-overflow) 1 wit inspect 10    7.9  450 0   0      true -32 --- inspect 6.9   3.9   300   .66 0      false(no-overflow) 1 --- inspect 4.0  2.3  250 0   1.5  false(no-overflow) 1 --- inspect .59   .59   20    .053 0      - --- inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect 4.5 2.4 200 42 .63 0      false(no-overflow) 1 wit inspect 3.7  2.0  250 0   0      error 0 --- inspect 6.8   3.9   310   .66 0      false(no-overflow) 1 --- inspect 3.5  2.1  250 0   0    false(no-overflow) 1 --- inspect .60   .60   20    .049 0      - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   920   210 13000 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   920   210 10000 .59 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   920   210 13000 .78 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   200 12000 .77 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   200 9900 .77 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   200 10000 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i timeout 0 --- inspect 900   920   200 11000 .77 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   150 12000 .78 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   920   160 12000 .76 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   920   150 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   920   150 12000 .59 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.5 0   0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   160 11000 .79 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .020 5.6 0   0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   920   150 11000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i timeout 0 --- inspect 900   920   150 13000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   200 9900 .88 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   150 11000 .78 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   150 13000 .58 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/parity_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   920   160 12000 .82 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   900   200 10000 .50 47      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 --- inspect 900   900   150 11000 .55 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
psyco/psyco_abp_1_false-no-overflow.c error (1) 0 --- inspect 4.7 2.2 200 39 .30 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0      error (invalid witness file) 0 --- inspect .91 .60 47 0   0    error (invalid witness file) 0 --- inspect .0015 .0020 .40 0     0      - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 79 17 53000 54000 14000 680000 63 94    19 17 110 68 5900 0   .0041 19 -149 120 71 5200 11   .020 19 -82 65 38   4300 0   8.7 19 17 10 10 350 .85 1.0  60 0 1.2 1.3 340 0   0  
    correct results 17 17 68 39 3000 670 13 .16 17 17 110 68 5800 0   .0041 11 11 78 46 3400 7.1 .020 14 14 51 30   3500 0   6.3 17 17 10 10 340 .85 1.0  0
        correct true 0 0 0 0 0 0
        correct false 17 17 68 39 3000 670 13 .16 17 17 110 68 5800 0   .0041 11 11 78 46 3400 7.1 .020 14 14 51 30   3500 0   6.3 17 17 10 10 340 .85 1.0  0
    incorrect results 0 0 5 -160 38 22 1500 3.2 0     3 -96 12 6.8 760 0   2.4 0 0
        incorrect true 0 0 5 -160 38 22 1500 3.2 0     3 -96 12 6.8 760 0   2.4 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 17 17 -149 -82 17 0
Run set verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-verifuzz.sv-comp19_prop-nooverflow.NoOverflows-Other