Tool skink CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.[sv-comp18.ReachSafety-Arrays; sv-comp18.ReachSafety-BitVectors; sv-comp18.ReachSafety-ControlFlow; sv-comp18.ReachSafety-Floats; sv-comp18.ReachSafety-Heap; sv-comp18.ReachSafety-Loops; sv-comp18.ReachSafety-Recursive] cpa-seq-validate-violation-witnesses-skink.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-Recursive] uautomizer-validate-violation-witnesses-skink.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-Recursive] cpa-witness2test-validate-violation-witnesses-skink.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-Recursive] fshell-witness2test-validate-violation-witnesses-skink.[sv-comp18-violation-witness.ReachSafety-Arrays; sv-comp18-violation-witness.ReachSafety-BitVectors; sv-comp18-violation-witness.ReachSafety-ControlFlow; sv-comp18-violation-witness.ReachSafety-Floats; sv-comp18-violation-witness.ReachSafety-Heap; sv-comp18-violation-witness.ReachSafety-Loops; sv-comp18-violation-witness.ReachSafety-Recursive] cpa-seq-validate-correctness-witnesses-skink.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-Recursive] uautomizer-validate-correctness-witnesses-skink.[sv-comp18-correctness-witness.ReachSafety-Arrays; sv-comp18-correctness-witness.ReachSafety-BitVectors; sv-comp18-correctness-witness.ReachSafety-ControlFlow; sv-comp18-correctness-witness.ReachSafety-Floats; sv-comp18-correctness-witness.ReachSafety-Heap; sv-comp18-correctness-witness.ReachSafety-Loops; sv-comp18-correctness-witness.ReachSafety-Recursive]
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
/localhome/dbeyer/comp/sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 6.0 330 56 timeout 0 wit inspect 94    2600 true -32 wit inspect 5.0   280   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 wit inspect 34   690 390 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 wit inspect 34   700 390 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 wit inspect 110   860 1200 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 wit inspect 110   810 1200 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 5.8 320 53 timeout 0 wit inspect 92    2000 true -32 wit inspect 3.9   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect 12      18    - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i unknown 0 wit inspect 43   710 460 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i unknown 0 wit inspect 5.7 320 52 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i unknown 0 wit inspect 5.9 320 50 error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0033 .29 - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i unknown 0 wit inspect 6.0 320 54 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i unknown 0 wit inspect 5.7 320 50 error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i unknown 0 wit inspect 6.1 320 52 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i unknown 0 wit inspect 5.5 300 46 error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i unknown 0 wit inspect 5.8 320 46 error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0039 .29 - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i unknown 0 wit inspect 5.5 300 49 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unknown 0 wit inspect 6.1 320 54 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .033 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0036 .28 - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i unknown 0 wit inspect 40   720 460 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i unknown 0 wit inspect 26   690 270 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0019 .28 - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i unknown 0 wit inspect 22   720 200 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i unknown 0 wit inspect 22   690 220 error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i unknown 0 wit inspect 22   680 190 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0030 .29 - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i unknown 0 wit inspect 24   690 240 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i unknown 0 wit inspect 24   690 270 error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0035 .29 - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i unknown 0 wit inspect 25   700 240 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i unknown 0 wit inspect 26   690 240 error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i unknown 0 wit inspect 42   710 510 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unknown 0 wit inspect 26   680 240 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0038 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unknown 0 wit inspect 24   700 240 error (invalid witness file) 0 wit inspect .67 45 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i true 2 wit inspect 4.1 270 36 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6100 true 2 wit inspect 7.1   270  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 wit inspect 31   690 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 8.1 410 67 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i unknown 0 wit inspect 31   700 320 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unknown 0 wit inspect 160   720 1700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 46 error (2) 0 wit inspect .019 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 4.5 270 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  490 true 2 wit inspect 7.9   260  
array-examples/sanfoundry_27_true-unreach-call_ground.i unknown 0 wit inspect 60   720 640 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i true 2 wit inspect 4.4 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  270 true 2 wit inspect 5.1   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 0 wit inspect 34   720 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .024 5.0
array-examples/sorting_selectionsort_true-unreach-call_ground.i timeout 0 wit inspect 900   1700 8800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i unknown 0 wit inspect 26   680 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i unknown 0 wit inspect 45   710 470 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy1_true-unreach-call_ground.i unknown 0 wit inspect 5.8 320 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i unknown 0 wit inspect 5.8 320 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy3_true-unreach-call_ground.i unknown 0 wit inspect 5.6 320 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy4_true-unreach-call_ground.i unknown 0 wit inspect 5.8 320 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy5_true-unreach-call_ground.i unknown 0 wit inspect 5.6 320 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.8
array-examples/standard_copy6_true-unreach-call_ground.i unknown 0 wit inspect 6.4 400 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_copy7_true-unreach-call_ground.i unknown 0 wit inspect 5.7 320 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .025 5.0
array-examples/standard_copy8_true-unreach-call_ground.i unknown 0 wit inspect 5.3 310 45 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .018 4.9
array-examples/standard_copy9_true-unreach-call_ground.i unknown 0 wit inspect 5.7 320 52 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .023 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unknown 0 wit inspect 5.8 310 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unknown 0 wit inspect 6.0 320 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i unknown 0 wit inspect 5.9 310 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i unknown 0 wit inspect 5.5 310 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_find_true-unreach-call_ground.i unknown 0 wit inspect 24   710 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 46 error (2) 0 wit inspect .021 4.9
array-examples/standard_init1_true-unreach-call_ground.i unknown 0 wit inspect 39   720 400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_init2_true-unreach-call_ground.i unknown 0 wit inspect 26   690 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_init3_true-unreach-call_ground.i unknown 0 wit inspect 21   710 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i unknown 0 wit inspect 21   670 200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_init5_true-unreach-call_ground.i unknown 0 wit inspect 23   680 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_init6_true-unreach-call_ground.i unknown 0 wit inspect 23   680 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_init7_true-unreach-call_ground.i unknown 0 wit inspect 25   700 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
array-examples/standard_init8_true-unreach-call_ground.i unknown 0 wit inspect 24   680 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 5.0
array-examples/standard_init9_true-unreach-call_ground.i unknown 0 wit inspect 25   690 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .027 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i unknown 0 wit inspect 41   740 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i unknown 0 wit inspect 42   730 440 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i unknown 0 wit inspect 45   710 530 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unknown 0 wit inspect 34   720 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unknown 0 wit inspect 33   690 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .035 4.9
array-examples/standard_partition_true-unreach-call_ground.i unknown 0 wit inspect 69   710 830 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_password_true-unreach-call_ground.i unknown 0 wit inspect 46   700 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .020 4.8
array-examples/standard_reverse_true-unreach-call_ground.i unknown 0 wit inspect 46   730 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_running_true-unreach-call.i unknown 0 wit inspect 29   710 290 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .019 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 25   700 240 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1000 true 2 wit inspect 11     330  
array-examples/standard_seq_init_true-unreach-call_ground.i unknown 0 wit inspect 40   700 450 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i unknown 0 wit inspect 240   710 3300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_strcpy_original_true-unreach-call.i unknown 0 wit inspect 30   710 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i unknown 0 wit inspect 26   690 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i unknown 0 wit inspect 5.6 310 47 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .018 4.8
array-examples/standard_two_index_02_true-unreach-call.i unknown 0 wit inspect 32   720 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9
array-examples/standard_two_index_03_true-unreach-call.i unknown 0 wit inspect 33   720 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .017 4.9
array-examples/standard_two_index_04_true-unreach-call.i unknown 0 wit inspect 31   700 330 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 5.0
array-examples/standard_two_index_05_true-unreach-call.i unknown 0 wit inspect 33   730 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .021 4.9
array-examples/standard_two_index_06_true-unreach-call.i unknown 0 wit inspect 32   780 320 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_07_true-unreach-call.i unknown 0 wit inspect 34   740 400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_08_true-unreach-call.i unknown 0 wit inspect 31   700 330 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .022 5.0
array-examples/standard_two_index_09_true-unreach-call.i unknown 0 wit inspect 32   740 350 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .021 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 100   710 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .022 5.0
array-examples/standard_vector_difference_true-unreach-call_ground.i unknown 0 wit inspect 49   720 510 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i unknown 0 wit inspect 25   690 280 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .85 48 error (invalid witness file) 0 wit inspect .0032 .30 - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 wit inspect 5.0 290 42 error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 150   730 1700 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i unknown 0 wit inspect 28   680 320 error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .034 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 41   710 420 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unknown 0 wit inspect 54   700 590 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i unknown 0 wit inspect 350   700 3900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .023 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i unknown 0 wit inspect 28   700 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i unknown 0 wit inspect 5.4 330 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .022 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unknown 0 wit inspect 5.3 300 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .025 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 wit inspect 5.7 310 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unknown 0 wit inspect 5.5 310 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 wit inspect 5.9 330 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 45 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 wit inspect 5.1 300 48 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .018 5.0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unknown 0 wit inspect 5.6 320 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unknown 0 wit inspect 5.9 350 55 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .020 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i unknown 0 wit inspect 140   710 1600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .020 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.0 390 53 false(unreach-call) 1 wit inspect 6.1  360 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 6.5 410 56 timeout 0 wit inspect 91    610 true -32 wit inspect 3.6   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 7.0 430 68 timeout 0 wit inspect 91    630 true -32 wit inspect 3.5   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 21   620 200 timeout 0 wit inspect 91    800 true -32 wit inspect 3.6   230   unknown 0 wit inspect 2.0  190 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i unknown 0 wit inspect 67   950 560 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0032 .29 - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unknown 0 wit inspect 8.6 440 72 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .90 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 16   840 140 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     4900  
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 17   690 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 timeout 0 wit inspect 960     6800  
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect 20   660 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     1700  
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect 23   900 240 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     4200  
reducercommutativity/avg60_true-unreach-call.i unknown 0 wit inspect 60   840 540 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i unknown 0 wit inspect 26   710 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 17   450 200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 99    930 timeout 0 wit inspect 960     1400  
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 18   450 200 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     3200  
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect 22   560 230 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4300 timeout 0 wit inspect 960     4500  
reducercommutativity/max40_true-unreach-call.i unknown 0 wit inspect 47   740 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .45 43 error (2) 0 wit inspect .019 4.8
reducercommutativity/max60_true-unreach-call.i unknown 0 wit inspect 24   690 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unknown 0 wit inspect 22   680 200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .48 44 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i true 2 wit inspect 6.7 350 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 870    1600 timeout 0 wit inspect 960     1800  
reducercommutativity/sep10_true-unreach-call.i true 2 wit inspect 9.8 420 84 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     6500  
reducercommutativity/sep20_true-unreach-call.i unknown 0 wit inspect 37   800 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.9
reducercommutativity/sep40_true-unreach-call.i unknown 0 wit inspect 41   920 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 43 error (2) 0 wit inspect .018 4.9
reducercommutativity/sep60_true-unreach-call.i unknown 0 wit inspect 21   690 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i unknown 0 wit inspect 19   680 190 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .027 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 16   650 180 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    850 true 2 wit inspect 350     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 17   420 170 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2200 timeout 0 wit inspect 960     5400  
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect 17   450 210 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4600 timeout 0 wit inspect 960     4600  
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect 21   670 190 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 timeout 0 wit inspect 960     4400  
reducercommutativity/sum60_true-unreach-call.i unknown 0 wit inspect 25   720 240 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i unknown 0 wit inspect 22   690 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
array-tiling/mlceu_false-unreach-call.i unknown 0 wit inspect 170   730 1900 error (invalid witness file) 0 wit inspect .68 46 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unknown 0 wit inspect 200   720 2200 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0026 .26 - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i unknown 0 wit inspect 57   730 640 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .024 4.9
array-tiling/mbpr3_true-unreach-call.i unknown 0 wit inspect 41   740 380 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
array-tiling/mbpr4_true-unreach-call.i unknown 0 wit inspect 34   850 350 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 5.0
array-tiling/mbpr5_true-unreach-call.i unknown 0 wit inspect 42   750 450 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .022 4.9
array-tiling/nr2_true-unreach-call.i unknown 0 wit inspect 140   730 1700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .020 4.9
array-tiling/nr3_true-unreach-call.i unknown 0 wit inspect 160   840 1900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .024 4.9
array-tiling/nr4_true-unreach-call.i unknown 0 wit inspect