Tool VerifierIntegerAssignmentPrograms File not exits 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] 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]
Date of execution 2017-12-03 03:42:11 CET 2017-12-03 04:30:19 CET 2017-12-03 04:52:11 CET 2017-12-03 04:56:53 CET 2017-12-03 05:05:18 CET 2017-12-03 04:20:47 CET 2017-12-03 04:35:31 CET
Run set viap.sv-comp18.ReachSafety-Arrays cpa-seq-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays uautomizer-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays fshell-witness2test-validate-violation-witnesses-viap.sv-comp18-violation-witness.ReachSafety-Arrays cpa-seq-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays uautomizer-validate-correctness-witnesses-viap.sv-comp18-correctness-witness.ReachSafety-Arrays
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.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/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/viap.2017-12-03_0342.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
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 unknown 0 wit inspect 46   120 620 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .92 50 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unknown 0 wit inspect 230   370 2300 error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0025 .30 - wit inspect - wit inspect
array-examples/sorting_bubblesort_false-unreach-call_ground.i unknown 0 wit inspect 230   330 2200 error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unknown 0 wit inspect 470   420 5600 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/sorting_selectionsort_false-unreach-call_ground.i unknown 0 wit inspect 260   280 3700 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
array-examples/standard_allDiff2_false-unreach-call_ground.i unknown 0 wit inspect 530   420 5300 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-examples/standard_copy1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 15   540 190 timeout 0 wit inspect 92    2000 true -32 wit inspect 6.5   260   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
array-examples/standard_copy2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 18   710 240 timeout 0 wit inspect 92    2000 true -32 wit inspect 5.3   220   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
array-examples/standard_copy3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 21   880 270 timeout 0 wit inspect 91    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
array-examples/standard_copy4_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 23   1000 320 timeout 0 wit inspect 92    2000 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
array-examples/standard_copy5_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 26   1200 310 timeout 0 wit inspect 91    2000 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
array-examples/standard_copy6_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 28   1400 410 timeout 0 wit inspect 92    2000 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
array-examples/standard_copy7_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 31   1600 490 timeout 0 wit inspect 92    2100 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
array-examples/standard_copy8_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 34   1800 440 timeout 0 wit inspect 91    2100 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
array-examples/standard_copy9_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 36   2000 550 timeout 0 wit inspect 92    2100 true -32 wit inspect 5.1   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
array-examples/standard_copyInitSum2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 17   1100 260 timeout 0 wit inspect 97    5300 timeout 0 wit inspect 97     6700   timeout 0 wit inspect 98    5500 false(unreach-call) 1 wit inspect 82      6300    - wit inspect - wit inspect
array-examples/standard_init1_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 12   480 160 timeout 0 wit inspect 97    3900 timeout 0 wit inspect 96     6100   timeout 0 wit inspect 97    3800 false(unreach-call) 1 wit inspect 26      2100    - wit inspect - wit inspect
array-examples/standard_init2_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 14   790 210 timeout 0 wit inspect 96    5100 timeout 0 wit inspect 96     6100   timeout 0 wit inspect 96    4800 false(unreach-call) 1 wit inspect 62      4200    - wit inspect - wit inspect
array-examples/standard_init3_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 17   1100 210 timeout 0 wit inspect 98    5300 out of memory 0 wit inspect 87     7000   timeout 0 wit inspect 98    5300 false(unreach-call) 1 wit inspect 80      6300    - wit inspect - wit inspect
array-examples/standard_init4_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 20   1400 290 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 98     6700   timeout 0 wit inspect 98    5500 timeout 0 wit inspect 91      7000    - wit inspect - wit inspect
array-examples/standard_init5_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 23   1800 290 timeout 0 wit inspect 98    5900 timeout 0 wit inspect 96     5400   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 82      7000    - wit inspect - wit inspect
array-examples/standard_init6_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 26   2100 350 timeout 0 wit inspect 98    5400 timeout 0 wit inspect 97     5400   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 73      7000    - wit inspect - wit inspect
array-examples/standard_init7_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 28   2400 400 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 98     5500   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 87      7000    - wit inspect - wit inspect
array-examples/standard_init8_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 31   2700 380 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 97     5600   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 75      7000    - wit inspect - wit inspect
array-examples/standard_init9_false-unreach-call_ground.i false(unreach-call) 0 wit inspect 34   3100 420 timeout 0 wit inspect 98    5500 timeout 0 wit inspect 97     5600   timeout 0 wit inspect 98    5500 out of memory 0 wit inspect 76      7000    - wit inspect - wit inspect
array-examples/standard_minInArray_false-unreach-call_ground.i false(unreach-call) 1 wit inspect 12   580 160 timeout 0 wit inspect 96    4100 timeout 0 wit inspect 96     6300   timeout 0 wit inspect 97    3800 false(unreach-call) 1 wit inspect 38      2700    - wit inspect - wit inspect
array-examples/standard_partition_false-unreach-call_ground.i unknown 0 wit inspect 29   110 430 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/standard_running_false-unreach-call.i unknown 0 wit inspect 530   1200 5200 error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unknown 0 wit inspect 70   160 1000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .023 4.9
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unknown 0 wit inspect 46   120 680 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.8
array-examples/relax_true-unreach-call.i unknown 0 wit inspect 11   92 170 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .023 4.9
array-examples/sanfoundry_02_true-unreach-call_ground.i true 2 wit inspect 360   1100 3600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .024 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i unknown 0 wit inspect 340   730 4000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .023 4.8
array-examples/sanfoundry_24_true-unreach-call_true-termination.i true 2 wit inspect 15   130 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .024 5.0
array-examples/sanfoundry_27_true-unreach-call_ground.i true 2 wit inspect 120   840 1100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .026 4.8
array-examples/sanfoundry_43_true-unreach-call_ground.i unknown 0 wit inspect 13   93 160 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .025 4.8
array-examples/sorting_bubblesort_true-unreach-call_ground.i unknown 0 wit inspect 230   320 1900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
array-examples/sorting_selectionsort_true-unreach-call_ground.i unknown 0 wit inspect 260   250 3600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 5.0
array-examples/standard_compareModified_true-unreach-call_ground.i true 2 wit inspect 120   550 1300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .024 5.0
array-examples/standard_compare_true-unreach-call_ground.i true 2 wit inspect 120   900 1400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .025 4.9
array-examples/standard_copy1_true-unreach-call_ground.i true 2 wit inspect 33   140 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .022 4.9
array-examples/standard_copy2_true-unreach-call_ground.i true 2 wit inspect 36   140 460 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .027 4.8
array-examples/standard_copy3_true-unreach-call_ground.i true 2 wit inspect 38   140 610 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .023 4.9
array-examples/standard_copy4_true-unreach-call_ground.i true 2 wit inspect 41   140 600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy5_true-unreach-call_ground.i true 2 wit inspect 44   140 570 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .025 4.8
array-examples/standard_copy6_true-unreach-call_ground.i true 2 wit inspect 46   140 620 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9
array-examples/standard_copy7_true-unreach-call_ground.i true 2 wit inspect 50   140 730 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .024 5.0
array-examples/standard_copy8_true-unreach-call_ground.i true 2 wit inspect 53   170 760 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .033 4.8
array-examples/standard_copy9_true-unreach-call_ground.i true 2 wit inspect 55   150 710 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .025 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i true 2 wit inspect 25   130 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .023 5.0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i true 2 wit inspect 30   170 390 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .023 5.0
array-examples/standard_copyInitSum_true-unreach-call_ground.i true 2 wit inspect 26   130 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
array-examples/standard_copyInit_true-unreach-call_ground.i true 2 wit inspect 22   130 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .021 5.0
array-examples/standard_find_true-unreach-call_ground.i true 2 wit inspect 25   180 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 45 error (2) 0 wit inspect .024 4.9
array-examples/standard_init1_true-unreach-call_ground.i true 2 wit inspect 20   130 330 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .025 4.9
array-examples/standard_init2_true-unreach-call_ground.i true 2 wit inspect 22   130 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_init3_true-unreach-call_ground.i true 2 wit inspect 25   140 380 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .022 4.8
array-examples/standard_init4_true-unreach-call_ground.i true 2 wit inspect 28   140 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .024 4.8
array-examples/standard_init5_true-unreach-call_ground.i true 2 wit inspect 30   140 390 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .020 4.9
array-examples/standard_init6_true-unreach-call_ground.i true 2 wit inspect 33   140 490 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .018 4.8
array-examples/standard_init7_true-unreach-call_ground.i true 2 wit inspect 35   150 490 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-examples/standard_init8_true-unreach-call_ground.i true 2 wit inspect 38   140 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_init9_true-unreach-call_ground.i true 2 wit inspect 40   170 520 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .028 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i true 2 wit inspect 130   1200 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .020 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i true 2 wit inspect 130   1400 1600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .022 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i true 2 wit inspect 18   130 250 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .025 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i unknown 0 wit inspect 220   740 2300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i unknown 0 wit inspect 24   120 350 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_partition_true-unreach-call_ground.i unknown 0 wit inspect 31   120 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .025 4.8
array-examples/standard_password_true-unreach-call_ground.i true 2 wit inspect 120   1200 1500 - 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_reverse_true-unreach-call_ground.i true 2 wit inspect 20   120 280 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_running_true-unreach-call.i true 2 wit inspect 430   1200 3800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .025 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i true 2 wit inspect 9.3 150 130 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .022 4.9
array-examples/standard_seq_init_true-unreach-call_ground.i true 2 wit inspect 23   230 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .023 4.8
array-examples/standard_strcmp_true-unreach-call_ground.i true 2 wit inspect 130   670 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_strcpy_original_true-unreach-call.i true 2 wit inspect 23   140 330 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_strcpy_true-unreach-call_ground.i true 2 wit inspect 24   140 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .023 4.9
array-examples/standard_two_index_01_true-unreach-call.i true 2 wit inspect 18   140 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .024 4.8
array-examples/standard_two_index_02_true-unreach-call.i true 2 wit inspect 29   140 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .021 4.9
array-examples/standard_two_index_03_true-unreach-call.i true 2 wit inspect 18   140 220 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .019 5.0
array-examples/standard_two_index_04_true-unreach-call.i true 2 wit inspect 28   150 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .024 4.8
array-examples/standard_two_index_05_true-unreach-call.i true 2 wit inspect 28   140 390 - 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_06_true-unreach-call.i true 2 wit inspect 18   140 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .75 46 error (2) 0 wit inspect .018 4.9
array-examples/standard_two_index_07_true-unreach-call.i true 2 wit inspect 27   140 320 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .024 4.9
array-examples/standard_two_index_08_true-unreach-call.i true 2 wit inspect 27   140 360 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
array-examples/standard_two_index_09_true-unreach-call.i true 2 wit inspect 27   140 400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .023 4.8
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i error (1) 0 wit inspect 29   350 370 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.9
array-examples/standard_vector_difference_true-unreach-call_ground.i true 2 wit inspect 21   130 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12   520 160 timeout 0 wit inspect 96    3900 timeout 0 wit inspect 92     7000   timeout 0 wit inspect 97    3800 false(unreach-call) 1 wit inspect 29      2100    - wit inspect - wit inspect
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unknown 0 wit inspect 15   110 210 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .029 4.8 error (invalid witness file) 0 wit inspect .68 50 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 220   1300 2300 error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
array-industry-pattern/array_range_init_false-unreach-call.i false(unreach-call) 1 wit inspect 12   100 160 timeout 0 wit inspect 92    830 timeout 0 wit inspect 97     4700   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i unknown 0 wit inspect 220   1400 2700 error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i false(unreach-call) 0 wit inspect 22   110 270 timeout 0 wit inspect 93    2200 true -32 wit inspect 3.7   240   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i true 2 wit inspect 21   210 270 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .024 5.0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i true 2 wit inspect 54   340 780 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.8
array-industry-pattern/array_of_struct_break_true-unreach-call.i true 2 wit inspect 18   230 230 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .023 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unknown 0 wit inspect 3.4 92 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .021 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unknown 0 wit inspect 4.3 92 59 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unknown 0 wit inspect 3.3 92 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .024 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unknown 0 wit inspect 2.5 92 32 - 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-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unknown 0 wit inspect 24   130 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .025 4.8
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unknown 0 wit inspect 3.3 92 40 - 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-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unknown 0 wit inspect 3.4 92 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .023 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i true 2 wit inspect 14   130 180 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .018 5.0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 25   120 320 exception 0 wit inspect 2.3  160 true -32 wit inspect 6.6   230   exception 0 wit inspect 2.6  170 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
reducercommutativity/rangesum10_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 25   110 310 exception 0 wit inspect 3.0  170 true -32 wit inspect 5.5   240   exception 0 wit inspect 2.4  170 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
reducercommutativity/rangesum20_false-unreach-call.i false(unreach-call) 1 wit inspect 25   96 340 exception 0 wit inspect 1.6  160 true -32 wit inspect 4.9   230   exception 0 wit inspect 1.8  170 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
reducercommutativity/rangesum40_false-unreach-call.i false(unreach-call) 1 wit inspect 25   98 330 exception 0 wit inspect 2.6  160 true -32 wit inspect 5.7   230   exception 0 wit inspect 1.8  170 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
reducercommutativity/rangesum60_false-unreach-call.i false(unreach-call) 1 wit inspect 25   120 420 exception 0 wit inspect 3.1  170 true -32 wit inspect 5.2   230   exception 0 wit inspect 2.5  170 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
reducercommutativity/rangesum_false-unreach-call_true-termination.i unknown 0 wit inspect 360   340 4500 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
reducercommutativity/avg05_true-unreach-call_true-termination.i true 2 wit inspect 41   240 450 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.8
reducercommutativity/avg10_true-unreach-call_true-termination.i true 2 wit inspect 25   250 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.9
reducercommutativity/avg20_true-unreach-call.i true 2 wit inspect 320   660 4300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .024 4.9
reducercommutativity/avg40_true-unreach-call.i true 2 wit inspect 25   250 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .023 4.9
reducercommutativity/avg60_true-unreach-call.i true 2 wit inspect 25   260 340 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .033 4.9
reducercommutativity/avg_true-unreach-call_true-termination.i unknown 0 wit inspect 330   270 4700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .025 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i true 2 wit inspect 180   250 2100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8
reducercommutativity/max10_true-unreach-call_true-termination.i true 2 wit inspect 250   450 3200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .021 4.8
reducercommutativity/max20_true-unreach-call.i true 2 wit inspect 370   680 4200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .026 5.0
reducercommutativity/max40_true-unreach-call.i true 2 wit inspect 250   640 3100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .024 4.9
reducercommutativity/max60_true-unreach-call.i true 2 wit inspect 250   450 3100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
reducercommutativity/max_true-unreach-call_true-termination.i unknown 0 wit inspect 340   560 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .027 4.8
reducercommutativity/sep05_true-unreach-call_true-termination.i unknown 0 wit inspect 350   440 4600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .027 4.8
reducercommutativity/sep10_true-unreach-call.i unknown 0 wit inspect 350   470 4800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .022 4.8
reducercommutativity/sep20_true-unreach-call.i unknown 0 wit inspect 350   510 4200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .023 4.8
reducercommutativity/sep40_true-unreach-call.i unknown 0 wit inspect 350   510 4500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .027 4.8
reducercommutativity/sep60_true-unreach-call.i unknown 0 wit inspect 350   470 4100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .023 4.8
reducercommutativity/sep_true-unreach-call_true-termination.i unknown 0 wit inspect 240   500 2900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .021 5.0
reducercommutativity/sum05_true-unreach-call_true-termination.i true 2 wit inspect 43   240 500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .025 4.9
reducercommutativity/sum10_true-unreach-call_true-termination.i true 2 wit inspect 26   250 310 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .023 4.8
reducercommutativity/sum20_true-unreach-call.i true 2 wit inspect 320   600 3600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .025 4.9
reducercommutativity/sum40_true-unreach-call.i true 2 wit inspect 26   250 330 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
reducercommutativity/sum60_true-unreach-call.i true 2 wit inspect 25   250 300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .025 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i unknown 0 wit inspect 330   460 4600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 5.0
array-tiling/mlceu_false-unreach-call.i unknown 0 wit inspect 17   120 260 error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .030 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
array-tiling/skippedu_false-unreach-call.i unknown 0 wit inspect 89   490 1100 error (invalid witness file) 0 wit inspect .70 42 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
array-tiling/mbpr2_true-unreach-call.i true 2 wit inspect 38   200 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .019 4.9
array-tiling/mbpr3_true-unreach-call.i true 2 wit inspect 57   200 750 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 46 error (2) 0 wit inspect .028 4.8
array-tiling/mbpr4_true-unreach-call.i true 2 wit inspect 100   360 1500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9
array-tiling/mbpr5_true-unreach-call.i true 2 wit inspect 330   6200 4100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .018 4.8
array-tiling/nr2_true-unreach-call.i true 2 wit inspect 31   230 430 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8
array-tiling/nr3_true-unreach-call.i true 2 wit inspect 30   220 490 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .024 4.8
array-tiling/nr4_true-unreach-call.i true 2 wit inspect 30   230 410 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 45 error (2) 0 wit inspect .024 4.9
array-tiling/nr5_true-unreach-call.i true 2 wit inspect 30   230 380 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .021 5.0
array-tiling/pnr2_true-unreach-call.i true 2 wit inspect 30   220 420 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .026 4.9
array-tiling/pnr3_true-unreach-call.i true 2 wit inspect 31   220 420 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.8
array-tiling/pnr4_true-unreach-call.i true 2