Tool DIVINE 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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-divine-smt.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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 unknown 0 --- inspect .029 .030 4.6 .20 0   0   error (invalid witness file) 0 --- inspect .66 .41 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0052 .0064 .53 0   0   - --- inspect
recursive/Addition03_false-no-overflow.c unknown 0 --- inspect .031 .032 4.6 .16 0   0   error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .79 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0068 .53 0   0   - --- inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 --- inspect .031 .032 4.6 .16 0   0   error (invalid witness file) 0 --- inspect .73 .46 41 0   0   error (2) 0 --- inspect .024 .025 5.8 0   0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0060 .52 0   0   - --- inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c unknown 0 --- inspect .033 .035 4.6 .25 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0   0  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .033 .034 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 --- inspect .043 .044 4.6 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 --- inspect .034 .035 4.5 .18 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .034 .035 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .028 .029 4.7 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .028 .029 4.8 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .032 .033 4.6 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .031 .032 4.6 .21 0   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 unknown 0 --- inspect .032 .033 4.6 .24 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 --- inspect .036 .037 4.6 .21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .029 5.6 0   0  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .027 .028 4.7 .20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .039 .041 4.9 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .035 .037 4.6 .28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.8 0   0  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .030 .031 4.6 .23 0   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 unknown 0 --- inspect .032 .034 4.6 .20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .055 .056 4.7 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .050 .053 4.6 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 --- inspect .032 .032 4.6 .25 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0   0  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .028 .029 4.6 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .031 .032 4.6 .20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .047 .047 4.7 .17 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 --- inspect .029 .030 4.6 .17 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 unknown 0 --- inspect .041 .042 4.6 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
recursive-simple/id_b3_o2_false-no-overflow.c unknown 0 --- inspect .032 .033 4.6 .29 0   0   error (invalid witness file) 0 --- inspect .64 .40 43 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0068 .41 0   0   - --- inspect
recursive-simple/id_b3_o5_false-no-overflow.c unknown 0 --- inspect .028 .029 4.5 .25 0   0   error (invalid witness file) 0 --- inspect .74 .44 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0   0   error (invalid witness file) 0 --- inspect 1.0  .66 46 0   0   error (invalid witness file) 0 --- inspect .0069 .011  .40 0   0   - --- inspect
recursive-simple/id_b5_o10_false-no-overflow.c unknown 0 --- inspect .030 .031 4.7 .19 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0   0   error (invalid witness file) 0 --- inspect 1.1  .69 46 0   0   error (invalid witness file) 0 --- inspect .0013 .0015 .40 0   0   - --- inspect
recursive-simple/sum_non_eq_false-no-overflow.c unknown 0 --- inspect .029 .030 4.7 .26 0   0   error (invalid witness file) 0 --- inspect .68 .41 43 0   0   error (2) 0 --- inspect .027 .028 5.6 0   0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0   error (invalid witness file) 0 --- inspect .0062 .0075 .53 0   0   - --- inspect
recursive-simple/sum_non_false-no-overflow.c unknown 0 --- inspect .030 .031 4.6 .17 0   0   error (invalid witness file) 0 --- inspect .65 .40 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0   0   error (invalid witness file) 0 --- inspect .0061 .0077 .53 0   0   - --- inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .033 .035 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.7 0   0  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .027 .028 4.6 .27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .044 .045 4.7 .20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .039 .040 4.8 .24 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .030 .031 4.6 .21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .043 .045 4.6 .18 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .026 .028 4.7 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.5 0   0  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .028 .029 4.7 .26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0   0  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .056 .057 4.6 .16 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0   0  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .027 .028 4.7 .30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .031 .033 4.6 .25 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .051 .052 4.6 .14 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.5 0   0  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .033 .034 4.6 .21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0   0  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .035 .036 4.6 .24 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0   0  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .035 .037 4.5 .28 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 --- inspect .026 .026 4.6 .24 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.6 0   0  
bitvector/byte_add_1_false-no-overflow.i unknown 0 --- inspect .028 .029 4.6 .22 0   0   error (invalid witness file) 0 --- inspect .61 .39 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0038 .0049 .53 0   0   - --- inspect
bitvector/byte_add_2_false-no-overflow.i unknown 0 --- inspect .057 .059 4.7 .22 0   0   error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .78 47 0   0   error (invalid witness file) 0 --- inspect .0049 .018  .41 0   0   - --- inspect
bitvector/byte_add_false-no-overflow.i unknown 0 --- inspect .053 .054 4.6 .19 0   0   error (invalid witness file) 0 --- inspect .77 .46 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .80 48 0   0   error (invalid witness file) 0 --- inspect .0014 .0016 .40 0   0   - --- inspect
bitvector/jain_1_false-no-overflow.i unknown 0 --- inspect .055 .056 4.6 .15 0   0   error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .99 .65 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0064 .52 0   0   - --- inspect
bitvector/jain_2_false-no-overflow.i unknown 0 --- inspect .030 .031 4.6 .19 0   0   error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .79 49 0   0   error (invalid witness file) 0 --- inspect .0048 .0064 .52 0   0   - --- inspect
bitvector/jain_4_false-no-overflow.i unknown 0 --- inspect .041 .042 4.6 .21 0   0   error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .027 .028 5.6 0   0   error (invalid witness file) 0 --- inspect 1.2  .76 46 0   0   error (invalid witness file) 0 --- inspect .0052 .0067 .52 0   0   - --- inspect
bitvector/jain_5_false-no-overflow.i unknown 0 --- inspect .028 .029 4.6 .17 0   0   error (invalid witness file) 0 --- inspect .63 .38 40 0   0   error (2) 0 --- inspect .026 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0026 .0032 .52 0   0   - --- inspect
bitvector/jain_6_false-no-overflow.i unknown 0 --- inspect .057 .058 4.6 .17 0   0   error (invalid witness file) 0 --- inspect .64 .38 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect 1.1  .75 49 0   0   error (invalid witness file) 0 --- inspect .0042 .0048 .40 0   0   - --- inspect
bitvector/jain_7_false-no-overflow.i unknown 0 --- inspect .029 .030 4.7 .19 0   0   error (invalid witness file) 0 --- inspect .81 .50 40 0   0   error (2) 0 --- inspect .028 .029 5.7 0   0   error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .53 0   0   - --- inspect
bitvector/modulus_false-no-overflow.i unknown 0 --- inspect .037 .038 4.6 .16 0   0   error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .92 .59 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0065 .52 0   0   - --- inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect .029 .030 4.6 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.8 0   0  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect .048 .049 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect .032 .034 4.6 .18 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .034 .035 4.6 .30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .027 .028 4.6 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0   0  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .027 .028 4.6 .21 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unknown 0 --- inspect .031 .032 4.8 .26 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .028 .030 4.7 .16 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect .048 .049 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect .027 .027 4.7 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect .045 .046 4.6 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .029 .030 4.6 .20 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .038 .039 5.6 0   0  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect .036 .039 4.6 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 --- inspect .033 .035 4.6 .27 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .043 .044 4.6 .15 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .023 .024 4.6 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .032 .033 4.6 .22 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .036 .038 4.6 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 --- inspect .028 .028 4.6 .19 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 --- inspect .029 .030 4.7 .23 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
psyco/psyco_abp_1_false-no-overflow.c unknown 0 --- inspect .034 .035 4.6 .21 0   0   error (invalid witness file) 0 --- inspect .75 .47 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect 1.1  .70 48 0   0   error (invalid witness file) 0 --- inspect .0030 .0079 .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 0 2.8 2.9 370 16 0   0   19 0 13 8.2 780 0   0   19 0 .45 .46 110 0   0   19 0 21 13 900 0   0   19 0 .084 .12 9.3 0   0   60 0 1.4 1.5 340 0   0  
    correct results 0 0 0 0 0 0
        correct true 0 0 0 0 0 0
        correct false 0 0 0 0 0 0
    incorrect results 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0
score (79 tasks, max score: 139) 0 0 0 0 0 0
Run set divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-nooverflow.NoOverflows-Other