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 1 6.0 330 56 0 94    2600 -32 5.0   280   0 2.7  210 1 .70   18    - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i 0 34   690 390 0 .65 41 0 .023 4.9 0 .82 47 0 .0010 .29 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i 0 34   700 390 0 .56 44 0 .019 4.8 0 .67 49 0 .0011 .26 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i 0 110   860 1200 0 .40 41 0 .020 4.9 0 .84 47 0 .0011 .28 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i 0 110   810 1200 0 .40 41 0 .020 4.9 0 .65 49 0 .0041 .26 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i 1 5.8 320 53 0 92    2000 -32 3.9   270   0 2.0  210 1 12      18    - -
array-examples/standard_copy1_false-unreach-call_ground.i 0 43   710 460 0 .56 44 0 .018 4.8 0 .83 47 0 .0010 .29 - -
array-examples/standard_copy2_false-unreach-call_ground.i 0 5.7 320 52 0 .59 43 0 .020 4.8 0 .84 47 0 .0011 .26 - -
array-examples/standard_copy3_false-unreach-call_ground.i 0 5.9 320 50 0 .63 43 0 .018 4.8 0 .66 49 0 .0033 .29 - -
array-examples/standard_copy4_false-unreach-call_ground.i 0 6.0 320 54 0 .55 44 0 .022 4.9 0 .85 47 0 .0012 .28 - -
array-examples/standard_copy5_false-unreach-call_ground.i 0 5.7 320 50 0 .68 42 0 .023 5.0 0 .86 47 0 .0036 .26 - -
array-examples/standard_copy6_false-unreach-call_ground.i 0 6.1 320 52 0 .53 41 0 .018 4.8 0 .85 47 0 .0035 .26 - -
array-examples/standard_copy7_false-unreach-call_ground.i 0 5.5 300 46 0 .71 46 0 .021 4.8 0 .66 49 0 .0012 .26 - -
array-examples/standard_copy8_false-unreach-call_ground.i 0 5.8 320 46 0 .64 41 0 .018 4.9 0 .84 47 0 .0039 .29 - -
array-examples/standard_copy9_false-unreach-call_ground.i 0 5.5 300 49 0 .54 44 0 .018 4.8 0 .65 49 0 .0011 .28 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i 0 6.1 320 54 0 .40 41 0 .033 4.9 0 .65 49 0 .0036 .28 - -
array-examples/standard_init1_false-unreach-call_ground.i 0 40   720 460 0 .53 44 0 .021 5.0 0 .83 47 0 .0041 .26 - -
array-examples/standard_init2_false-unreach-call_ground.i 0 26   690 270 0 .54 42 0 .018 4.8 0 .86 47 0 .0019 .28 - -
array-examples/standard_init3_false-unreach-call_ground.i 0 22   720 200 0 .40 43 0 .021 4.8 0 .84 47 0 .0014 .29 - -
array-examples/standard_init4_false-unreach-call_ground.i 0 22   690 220 0 .68 46 0 .018 4.8 0 .85 48 0 .0018 .26 - -
array-examples/standard_init5_false-unreach-call_ground.i 0 22   680 190 0 .56 43 0 .018 4.9 0 .81 47 0 .0030 .29 - -
array-examples/standard_init6_false-unreach-call_ground.i 0 24   690 240 0 .66 43 0 .023 4.9 0 .68 49 0 .0011 .26 - -
array-examples/standard_init7_false-unreach-call_ground.i 0 24   690 270 0 .68 41 0 .022 4.9 0 .66 49 0 .0035 .29 - -
array-examples/standard_init8_false-unreach-call_ground.i 0 25   700 240 0 .56 44 0 .020 4.9 0 .66 49 0 .0036 .29 - -
array-examples/standard_init9_false-unreach-call_ground.i 0 26   690 240 0 .67 45 0 .019 5.0 0 .83 47 0 .0011 .26 - -
array-examples/standard_minInArray_false-unreach-call_ground.i 0 42   710 510 0 .58 43 0 .022 4.9 0 .83 47 0 .0036 .26 - -
array-examples/standard_partition_false-unreach-call_ground.i 0 26   680 240 0 .41 43 0 .018 4.8 0 .85 48 0 .0038 .26 - -
array-examples/standard_running_false-unreach-call.i 0 24   700 240 0 .67 45 0 .021 4.9 0 .84 47 0 .0041 .26 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i 2 4.1 270 36 - - - - 0 900    6100 2 7.1   270  
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i 0 31   690 310 - - - - 0 .56 42 0 .020 4.9
array-examples/relax_true-unreach-call.i 0 8.1 410 67 - - - - 0 .59 42 0 .019 4.8
array-examples/sanfoundry_02_true-unreach-call_ground.i 0 31   700 320 - - - - 0 .57 43 0 .021 4.9
array-examples/sanfoundry_10_true-unreach-call_ground.i 0 160   720 1700 - - - - 0 .59 46 0 .019 4.9
array-examples/sanfoundry_24_true-unreach-call_true-termination.i 2 4.5 270 44 - - - - 2 6.4  490 2 7.9   260  
array-examples/sanfoundry_27_true-unreach-call_ground.i 0 60   720 640 - - - - 0 .56 43 0 .020 5.0
array-examples/sanfoundry_43_true-unreach-call_ground.i 2 4.4 290 41 - - - - 2 4.8  270 2 5.1   220  
array-examples/sorting_bubblesort_true-unreach-call_ground.i 0 34   720 410 - - - - 0 .59 42 0 .024 5.0
array-examples/sorting_selectionsort_true-unreach-call_ground.i 0 900   1700 8800 - - - - 0 .53 42 0 .019 4.9
array-examples/standard_compareModified_true-unreach-call_ground.i 0 26   680 240 - - - - 0 .56 41 0 .018 4.8
array-examples/standard_compare_true-unreach-call_ground.i 0 45   710 470 - - - - 0 .58 45 0 .020 4.8
array-examples/standard_copy1_true-unreach-call_ground.i 0 5.8 320 48 - - - - 0 .56 44 0 .018 4.8
array-examples/standard_copy2_true-unreach-call_ground.i 0 5.8 320 56 - - - - 0 .58 42 0 .019 4.8
array-examples/standard_copy3_true-unreach-call_ground.i 0 5.6 320 53 - - - - 0 .55 43 0 .019 4.9
array-examples/standard_copy4_true-unreach-call_ground.i 0 5.8 320 47 - - - - 0 .54 41 0 .019 4.8
array-examples/standard_copy5_true-unreach-call_ground.i 0 5.6 320 53 - - - - 0 .69 41 0 .020 4.8
array-examples/standard_copy6_true-unreach-call_ground.i 0 6.4 400 50 - - - - 0 .58 41 0 .019 4.8
array-examples/standard_copy7_true-unreach-call_ground.i 0 5.7 320 51 - - - - 0 .54 43 0 .025 5.0
array-examples/standard_copy8_true-unreach-call_ground.i 0 5.3 310 45 - - - - 0 .70 42 0 .018 4.9
array-examples/standard_copy9_true-unreach-call_ground.i 0 5.7 320 52 - - - - 0 .53 44 0 .023 5.0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i 0 5.8 310 53 - - - - 0 .56 44 0 .024 4.9
array-examples/standard_copyInitSum3_true-unreach-call_ground.i 0 6.0 320 58 - - - - 0 .55 42 0 .018 4.8
array-examples/standard_copyInitSum_true-unreach-call_ground.i 0 5.9 310 56 - - - - 0 .71 43 0 .022 4.9
array-examples/standard_copyInit_true-unreach-call_ground.i 0 5.5 310 51 - - - - 0 .56 44 0 .019 4.8
array-examples/standard_find_true-unreach-call_ground.i 0 24   710 250 - - - - 0 .58 46 0 .021 4.9
array-examples/standard_init1_true-unreach-call_ground.i 0 39   720 400 - - - - 0 .54 42 0 .019 4.8
array-examples/standard_init2_true-unreach-call_ground.i 0 26   690 250 - - - - 0 .56 43 0 .022 4.9
array-examples/standard_init3_true-unreach-call_ground.i 0 21   710 190 - - - - 0 .54 44 0 .023 4.9
array-examples/standard_init4_true-unreach-call_ground.i 0 21   670 200 - - - - 0 .54 43 0 .020 4.9
array-examples/standard_init5_true-unreach-call_ground.i 0 23   680 230 - - - - 0 .54 42 0 .018 4.8
array-examples/standard_init6_true-unreach-call_ground.i 0 23   680 230 - - - - 0 .44 43 0 .019 4.9
array-examples/standard_init7_true-unreach-call_ground.i 0 25   700 250 - - - - 0 .54 43 0 .020 4.9
array-examples/standard_init8_true-unreach-call_ground.i 0 24   680 230 - - - - 0 .55 43 0 .025 5.0
array-examples/standard_init9_true-unreach-call_ground.i 0 25   690 280 - - - - 0 .54 42 0 .027 4.8
array-examples/standard_maxInArray_true-unreach-call_ground.i 0 41   740 410 - - - - 0 .54 42 0 .019 4.8
array-examples/standard_minInArray_true-unreach-call_ground.i 0 42   730 440 - - - - 0 .73 42 0 .019 4.9
array-examples/standard_palindrome_true-unreach-call_ground.i 0 45   710 530 - - - - 0 .50 43 0 .019 4.9
array-examples/standard_partial_init_true-unreach-call_ground.i 0 34   720 410 - - - - 0 .68 43 0 .019 4.8
array-examples/standard_partition_original_true-unreach-call_ground.i 0 33   690 300 - - - - 0 .63 42 0 .035 4.9
array-examples/standard_partition_true-unreach-call_ground.i 0 69   710 830 - - - - 0 .46 44 0 .019 4.8
array-examples/standard_password_true-unreach-call_ground.i 0 46   700 520 - - - - 0 .52 44 0 .020 4.8
array-examples/standard_reverse_true-unreach-call_ground.i 0 46   730 430 - - - - 0 .43 43 0 .018 4.8
array-examples/standard_running_true-unreach-call.i 0 29   710 290 - - - - 0 .65 42 0 .019 4.8
array-examples/standard_sentinel_true-unreach-call_true-termination.i 2 25   700 240 - - - - 0 900    1000 2 11     330  
array-examples/standard_seq_init_true-unreach-call_ground.i 0 40   700 450 - - - - 0 .50 43 0 .022 4.9
array-examples/standard_strcmp_true-unreach-call_ground.i 0 240   710 3300 - - - - 0 .55 43 0 .019 4.9
array-examples/standard_strcpy_original_true-unreach-call.i 0 30   710 300 - - - - 0 .68 42 0 .019 4.9
array-examples/standard_strcpy_true-unreach-call_ground.i 0 26   690 230 - - - - 0 .55 42 0 .018 4.8
array-examples/standard_two_index_01_true-unreach-call.i 0 5.6 310 47 - - - - 0 .61 43 0 .018 4.8
array-examples/standard_two_index_02_true-unreach-call.i 0 32   720 310 - - - - 0 .57 44 0 .019 4.9
array-examples/standard_two_index_03_true-unreach-call.i 0 33   720 310 - - - - 0 .41 45 0 .017 4.9
array-examples/standard_two_index_04_true-unreach-call.i 0 31   700 330 - - - - 0 .63 41 0 .018 5.0
array-examples/standard_two_index_05_true-unreach-call.i 0 33   730 340 - - - - 0 .70 42 0 .021 4.9
array-examples/standard_two_index_06_true-unreach-call.i 0 32   780 320 - - - - 0 .60 41 0 .018 4.9
array-examples/standard_two_index_07_true-unreach-call.i 0 34   740 400 - - - - 0 .53 44 0 .019 4.8
array-examples/standard_two_index_08_true-unreach-call.i 0 31   700 330 - - - - 0 .50 44 0 .022 5.0
array-examples/standard_two_index_09_true-unreach-call.i 0 32   740 350 - - - - 0 .59 41 0 .021 4.9
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i 0 100   710 1400 - - - - 0 .56 44 0 .022 5.0
array-examples/standard_vector_difference_true-unreach-call_ground.i 0 49   720 510 - - - - 0 .54 43 0 .021 5.0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i 0 25   690 280 0 .57 44 0 .024 4.9 0 .85 48 0 .0032 .30 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i 0 5.0 290 42 0 .70 45 0 .022 4.9 0 .84 47 0 .0011 .26 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i 0 150   730 1700 0 .55 43 0 .018 4.9 0 .84 47 0 .0011 .28 - -
array-industry-pattern/array_range_init_false-unreach-call.i 0 28   680 320 0 .41 41 0 .034 4.8 0 .84 47 0 .0011 .26 - -
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i 0 41   710 420 0 .66 42 0 .018 4.8 0 .85 47 0 .0011 .26 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i 0 54   700 590 0 .56 44 0 .023 4.8 0 .67 49 0 .0011 .26 - -
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i 0 350   700 3900 - - - - 0 .58 41 0 .023 4.9
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i 0 28   700 300 - - - - 0 .53 42 0 .019 4.9
array-industry-pattern/array_of_struct_break_true-unreach-call.i 0 5.4 330 42 - - - - 0 .67 41 0 .022 4.8
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i 0 5.3 300 49 - - - - 0 .61 43 0 .025 4.8
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i 0 5.7 310 51 - - - - 0 .44 43 0 .019 4.8
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i 0 5.5 310 49 - - - - 0 .55 42 0 .020 4.8
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i 0 5.9 330 48 - - - - 0 .41 45 0 .020 4.9
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i 0 5.1 300 48 - - - - 0 .66 41 0 .018 5.0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i 0 5.6 320 57 - - - - 0 .61 41 0 .020 4.9
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i 0 5.9 350 55 - - - - 0 .61 41 0 .020 4.9
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i 0 140   710 1600 - - - - 0 .56 42 0 .020 4.9
reducercommutativity/rangesum05_false-unreach-call_true-termination.i 1 6.0 390 53 1 6.1  360 -32 4.9   230   0 2.1  210 1 .57   18    - -
reducercommutativity/rangesum10_false-unreach-call_true-termination.i 1 6.5 410 56 0 91    610 -32 3.6   240   0 2.0  210 1 .58   18    - -
reducercommutativity/rangesum20_false-unreach-call.i 1 7.0 430 68 0 91    630 -32 3.5   230   0 2.0  210 1 .61   18    - -
reducercommutativity/rangesum40_false-unreach-call.i 1 21   620 200 0 91    800 -32 3.6   230   0 2.0  190 1 .57   18    - -
reducercommutativity/rangesum60_false-unreach-call.i 0 67   950 560 0 .55 44 0 .019 4.9 0 .69 49 0 .0032 .29 - -
reducercommutativity/rangesum_false-unreach-call_true-termination.i 0 8.6 440 72 0 .57 42 0 .022 4.9 0 .90 47 0 .0010 .26 - -
reducercommutativity/avg05_true-unreach-call_true-termination.i 2 16   840 140 - - - - 0 900    1500 0 960     4900  
reducercommutativity/avg10_true-unreach-call_true-termination.i 2 17   690 170 - - - - 0 900    3500 0 960     6800  
reducercommutativity/avg20_true-unreach-call.i 2 20   660 180 - - - - 0 900    5000 0 960     1700  
reducercommutativity/avg40_true-unreach-call.i 2 23   900 240 - - - - 0 900    3700 0 960     4200  
reducercommutativity/avg60_true-unreach-call.i 0 60   840 540 - - - - 0 .58 41 0 .019 5.0
reducercommutativity/avg_true-unreach-call_true-termination.i 0 26   710 230 - - - - 0 .55 43 0 .019 4.8
reducercommutativity/max05_true-unreach-call_true-termination.i 2 17   450 200 - - - - 2 99    930 0 960     1400  
reducercommutativity/max10_true-unreach-call_true-termination.i 2 18   450 200 - - - - 0 900    2800 0 960     3200  
reducercommutativity/max20_true-unreach-call.i 2 22   560 230 - - - - 0 900    4300 0 960     4500  
reducercommutativity/max40_true-unreach-call.i 0 47   740 520 - - - - 0 .45 43 0 .019 4.8
reducercommutativity/max60_true-unreach-call.i 0 24   690 240 - - - - 0 .56 43 0 .020 4.9
reducercommutativity/max_true-unreach-call_true-termination.i 0 22   680 200 - - - - 0 .48 44 0 .019 4.9
reducercommutativity/sep05_true-unreach-call_true-termination.i 2 6.7 350 63 - - - - 2 870    1600 0 960     1800  
reducercommutativity/sep10_true-unreach-call.i 2 9.8 420 84 - - - - 0 900    1800 0 960     6500  
reducercommutativity/sep20_true-unreach-call.i 0 37   800 410 - - - - 0 .57 43 0 .025 4.9
reducercommutativity/sep40_true-unreach-call.i 0 41   920 410 - - - - 0 .77 43 0 .018 4.9
reducercommutativity/sep60_true-unreach-call.i 0 21   690 190 - - - - 0 .55 43 0 .019 4.9
reducercommutativity/sep_true-unreach-call_true-termination.i 0 19   680 190 - - - - 0 .54 41 0 .027 4.9
reducercommutativity/sum05_true-unreach-call_true-termination.i 2 16   650 180 - - - - 0 900    850 2 350     3500  
reducercommutativity/sum10_true-unreach-call_true-termination.i 2 17   420 170 - - - - 0 900    2200 0 960     5400  
reducercommutativity/sum20_true-unreach-call.i 2 17   450 210 - - - - 0 900    4600 0 960     4600  
reducercommutativity/sum40_true-unreach-call.i 2 21   670 190 - - - - 0 900    2500 0 960     4400  
reducercommutativity/sum60_true-unreach-call.i 0 25   720 240 - - - - 0 .60 43 0 .019 4.9
reducercommutativity/sum_true-unreach-call_true-termination.i 0 22   690 220 - - - - 0 .53 43 0 .018 4.8
array-tiling/mlceu_false-unreach-call.i 0 170   730 1900 0 .68 46 0 .018 4.8 0 .67 49 0 .0019 .30 - -
array-tiling/skippedu_false-unreach-call.i 0 200   720 2200 0 .57 44 0 .019 4.8 0 .68 49 0 .0026 .26 - -
array-tiling/mbpr2_true-unreach-call.i 0 57   730 640 - - - - 0 .54 43 0 .024 4.9
array-tiling/mbpr3_true-unreach-call.i 0 41   740 380 - - - - 0 .64 41 0 .019 4.9
array-tiling/mbpr4_true-unreach-call.i 0 34   850 350 - - - - 0 .66 44 0 .018 5.0
array-tiling/mbpr5_true-unreach-call.i 0 42   750 450 - - - - 0 .56 43 0 .022 4.9
array-tiling/nr2_true-unreach-call.i 0 140   730 1700 - - - - 0 .59 41 0 .020 4.9
array-tiling/nr3_true-unreach-call.i 0 160   840 1900 - - - - 0 .70 41 0 .024 4.9
array-tiling/nr4_true-unreach-call.i 0 170   750 1700 - - - - 0 .69 42 0 .019 4.9
array-tiling/nr5_true-unreach-call.i 0 180   760 2000 - - - - 0 .55 42 0 .020 4.8
array-tiling/pnr2_true-unreach-call.i 0 26   720 250 - - - - 0 .44 43 0 .020 4.9
array-tiling/pnr3_true-unreach-call.i 0 28   720 280 - - - - 0 .62 42 0 .021 5.0
array-tiling/pnr4_true-unreach-call.i 0 28   720 290 - - - - 0 .65 41 0 .021 4.9
array-tiling/pnr5_true-unreach-call.i 0 30   740 290 - - - - 0 .59 41 0 .019 4.8
array-tiling/poly1_true-unreach-call.i 2 120   1400 1100 - - - - 0 900    5200 0 960     930  
array-tiling/poly2_true-unreach-call.i 0 220   1400 2400 - - - - 0 .63 44 0 .019 4.9
array-tiling/pr2_true-unreach-call.i 2 4.3 270 43 - - - - 0 900    2300 0 960     910  
array-tiling/pr3_true-unreach-call.i 2 4.6 360 37 - - - - 0 900    2100 0 960     920  
array-tiling/pr4_true-unreach-call.i 2 4.4 270 43 - - - - 0 900    2100 0 960     740  
array-tiling/pr5_true-unreach-call.i 2 4.3 270 39 - - - - 0 900    1900 0 960     1200  
array-tiling/revcpyswp2_true-unreach-call.i 0 41   750 410 - - - - 0 .55 44 0 .025 4.8
array-tiling/rew_true-unreach-call.i 0 6.8 340 55 - - - - 0 .45 43 0 .023 5.0
array-tiling/rewnif_true-unreach-call.i 0 6.8 350 52 - - - - 0 .56 41 0 .024 4.8
array-tiling/rewnifrev2_true-unreach-call.i 0 160   720 2000 - - - - 0 .49 43 0 .020 4.9
array-tiling/rewnifrev_true-unreach-call.i 0 91   750 960 - - - - 0 .56 44 0 .021 5.0
array-tiling/rewrev_true-unreach-call.i 2 32   720 390 - - - - 0 900    2300 0 960     2500  
array-tiling/skipped_true-unreach-call.i 0 190   720 2500 - - - - 0 .46 43 0 .024 4.8
array-tiling/tcpy_true-unreach-call.i 0 170   760 2200 - - - - 0 .68 43 0 .019 4.9
array-programs/copysome1_false-unreach-call.i 0 31   690 300 0 .62 43 0 .047 4.8 0 .66 49 0 .0011 .26 - -
array-programs/copysome2_false-unreach-call.i 0 6.5 330 56 0 .71 42 0 .018 4.9 0 .66 50 0 .0013 .30 - -
array-programs/copysome1_true-unreach-call.i 0 31   690 350 - - - - 0 .68 43 0 .020 4.9
array-programs/copysome2_true-unreach-call.i 0 6.4 320 55 - - - - 0 .57 42 0 .022 4.8
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i 0 47   730 600 0 .55 41 0 .018 4.9 0 .64 49 0 .0041 .26 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i 0 110   730 1500 0 .68 41 0 .019 4.8 0 .66 49 0 .0015 .28 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i 0 35   700 370 - - - - 0 .60 41 0 .018 4.8
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i 0 31   710 360 - - - - 0 .70 44 0 .024 4.8
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 0 84   950 730 - - - - 0 .55 43 0 .020 4.8
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 2 27   900 250 - - - - 2 160    460 0 960     2600  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 0 82   870 1200 - - - - 0 .55 46 0 .018 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i 2 25   700 260 - - - - 2 7.2  310 2 44     590  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 2 7.6 370 66 - - - - 2 6.3  310 2 160     530  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i 2 20   690 190 - - - - 0 910    5700 2 5.3   260  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i 2 26   730 320 - - - - 0 780    7000 2 6.6   250  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i 2 4.5 260 38 - - - - 0 780    7000 2 5.2   260  
bitvector/jain_5_true-unreach-call_true-no-overflow.i 1 4.0 320 35 - - - - 0 900    1700 0 960     660  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i 2 4.0 250 39 - - - - 0 660    7000 2 21     270  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i 2 4.1 250 43 - - - - 0 910    6700 2 6.3   260  
bitvector/modulus_true-unreach-call_true-no-overflow.i 0 46   730 530 - - - - 0 .50 45 0 .022 4.8
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 2 3.9 240 37 - - - - 2 4.9  270 2 62     610  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 2 5.3 300 47 - - - - 2 4.7  280 0 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i 0 150   740 1800 - - - - 0 .68 44 0 .021 4.8
bitvector/sum02_true-unreach-call_true-no-overflow.i 0 130   770 1800 - - - - 0 .55 43 0 .019 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c 0 82   780 980 0 .53 43 0 .020 4.8 0 .82 47 0 .0037 .26 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c 0 45   720 530 0 .60 43 0 .018 4.8 0 .85 47 0 .0011 .29 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c 0 39   710 470 0 .54 45 0 .018 4.9 0 .85 47 0 .0014 .26 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 100   840 1300 - - - - 0 .56 44 0 .027 5.0
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c 0 89   760 940 - - - - 0 .63 41 0 .024 4.8
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 54   720 650 - - - - 0 .61 44 0 .024 5.0
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 900   1400 9200 - - - - 0 .67 42 0 .019 4.8
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c 0 62   730 610 - - - - 0 .72 44 0 .018 4.9
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 0 16   660 130 - - - - 0 .46 44 0 .020 4.9
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c 0 12   640 100 - - - - 0 .56 45 0 .019 4.8
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c 0 79   980 990 - - - - 0 .67 41 0 .019 4.9
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c 0 15   650 130 - - - - 0 .68 44 0 .020 4.9
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 17   650 140 - - - - 0 .53 42 0 .019 4.9
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 20   680 180 - - - - 0 .54 44 0 .019 4.8
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 19   660 170 - - - - 0 .67 42 0 .019 4.8
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 18   640 180 - - - - 0 .53 43 0 .019 4.8
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c 0 22   700 200 - - - - 0 .53 41 0 .020 4.9
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c 1 4.9 300 46 1 3.1  260 1 6.3   240   0 1.9  190 1 .59   18    - -
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c 1 4.9 290 41 1 3.2  270 1 4.9   220   0 1.9  180 1 .56   18    - -
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c 1 4.7 290 45 1 3.0  260 1 6.2   210   0 1.9  180 1 .56   18    - -
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c 0 3.8 240 35 0 .68 42 0 .018 4.8 0 .69 50 0 .0018 .28 - -
bitvector-regression/signextension2_false-unreach-call_true-termination.c 1 5.0 300 45 1 2.2  260 1 3.1   230   0 2.0  180 1 .61   18    - -
bitvector-regression/signextension_false-unreach-call_true-termination.c 1 4.9 300 44 1 3.2  250 1 3.1   220   0 2.7  190 1 .56   18    - -
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c 2 3.6 230 34 - - - - 2 3.0  250 2 5.5   250  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c 2 3.7 230 36 - - - - 2 2.3  250 2 9.2   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c 2 3.7 220 31 - - - - 2 3.4  250 2 5.7   260  
bitvector-regression/signextension_true-unreach-call_true-termination.c 2 3.9 240 33 - - - - 2 4.3  240 2 5.4   260  
bitvector-loops/diamond_false-unreach-call2.i 1 5.6 320 50 1 3.5  260 -32 3.8   260   0 2.2  210 -32 .61   18    - -
bitvector-loops/overflow_false-unreach-call1.i 1 4.9 300 41 0 92    1900 -32 3.7   260   0 1.9  190 1 4.0    18    - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i 0 13   460 130 -32 3.8  260 -32 4.1   230   0 2.8  210 -32 .57   18    - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 88   1600 590 0 .57 44 0 .023 5.0 0 .68 49 0 .0042 .26 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 52   960 530 0 .57 43 0 .019 5.0 0 .83 47 0 .0033 .29 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 50   1100 430 0 .57 42 0 .023 4.9 0 .64 49 0 .0018 .26 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 0 28   930 260 0 .64 46 0 .020 4.9 0 .69 50 0 .0036 .26 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 94   1500 570 - - - - 0 .72 46 0 .020 4.8
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 53   1200 410 - - - - 0 .57 41 0 .018 4.8
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 51   970 500 - - - - 0 .51 41 0 .021 4.9
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 49   1100 410 - - - - 0 .52 42 0 .018 5.0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 29   800 300 - - - - 0 .42 43 0 .024 4.8
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 27   820 230 - - - - 0 .58 44 0 .019 4.9
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 0 67   750 720 0 .70 45 0 .018 4.9 0 .82 47 0 .0011 .26 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 0 44   720 440 0 .70 45 0 .018 4.8 0 .83 47 0 .0011 .28 - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 0 53   720 560 0 .40 43 0 .021 4.8 0 .91 47 0 .0037 .28 - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 0 72   750 750 0 .61 43 0 .023 4.8 0 .82 47 0 .0012 .26 - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 0 110   820 1400 0 .54 42 0 .024 5.0 0 .84 48 0 .0017 .26 - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 0 9.9 500 93 0 .62 43 0 .018 4.9 0 .67 49 0 .0032 .26 - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 0 11   640 90 0 .57 43 0 .019 4.8 0 .84 47 0 .0016 .31 - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 0 150   1100 1800 0 .66 41 0 .020 4.9 0 .86 47 0 .0011 .28 - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 0 15   650 130 0 .70 42 0 .019 4.8 0 .66 49 0 .0036 .29 - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 0 14   640 120 0 .58 41 0 .023 4.9 0 .86 47 0 .0026 .29 - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 0 15   660 110 0 .70 41 0 .022 4.8 0 .83 47 0 .0012 .26 - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 0 14   660 120 0 .68 42 0 .037 4.8 0 .67 49 0 .0028 .26 - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 0 67   730 760 - - - - 0 .65 47 0 .020 4.8
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 46   720 520 - - - - 0 .73 43 0 .020 5.0
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 0 47   720 490 - - - - 0 .68 41 0 .020 5.0
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 0 33   700 370 - - - - 0 .55 43 0 .019 4.8
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 14   650 110 - - - - 0 .69 45 0 .023 4.9
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 31   690 310 - - - - 0 .54 41 0 .022 5.0
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 96   720 1000 - - - - 0 .69 42 0 .023 4.9
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 0 15   650 130 - - - - 0 .48 43 0 .018 4.8
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 16   640 140 - - - - 0 .59 43 0 .021 4.8
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 16   640 150 - - - - 0 .58 43 0 .019 4.9
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 20   670 160 - - - - 0 .59 41 0 .018 4.8
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 18   660 180 - - - - 0 .46 46 0 .019 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 0 16   700 130 - - - - 0 .53 43 0 .019 4.9
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 0 6.0 330 58 -32 4.4  270 -32 4.2   240   0 2.2  210 -32 .62   18    - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 5.7 320 53 -32 5.3  270 -32 4.4   240   0 3.3  210 -32 .62   18    - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.1 260 42 - - - - 2 3.6  280 2 16     640  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.3 270 43 - - - - 2 6.6  280 2 23     1200  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.4 270 41 - - - - 2 5.4  280 2 27     2000  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.2 270 44 - - - - 2 5.5  290 2 42     3800  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.3 280 35 - - - - 2 6.6  290 2 69     5800  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.4 290 43 - - - - 2 5.7  290 0 110     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.3 260 40 - - - - 2 5.2  290 2 7.6   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.2 310 44 - - - - 2 3.7  280 2 8.3   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.0 260 41 - - - - 2 5.0  280 2 9.8   370  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.1 260 38 - - - - 2 4.8  280 2 13     510  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.0 260 36 - - - - 2 5.4  280 2 16     530  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 69   1700 380 0 .53 43 0 .051 4.9 0 .84 47 0 .0036 .26 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 59   1400 290 0 .67 42 0 .021 4.8 0 .84 47 0 .0011 .26 - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 32   1100 170 0 .64 43 0 .019 4.9 0 .66 49 0 .0041 .26 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 20   760 120 0 .58 44 0 .023 4.8 0 .83 47 0 .0010 .29 - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 340   1700 1700 0 .72 46 0 .018 4.9 0 .91 47 0 .0023 .26 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 53   1500 260 - - - - 0 .56 43 0 .022 4.9
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 83   1700 390 - - - - 0 .68 44 0 .020 4.9
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 5.0 350 50 - - - - 0 .55 44 0 .020 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 32   1200 180 - - - - 0 .67 41 0 .018 4.8
ntdrivers/parport_true-unreach-call.i.cil.c 0 340   1700 1500 - - - - 0 .57 42 0 .021 4.8
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 9.6 540 85 0 .59 42 0 .018 4.8 0 .65 52 0 .0040 .26 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 9.8 540 87 0 .69 46 0 .018 4.8 0 .68 49 0 .0029 .29 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 9.5 550 85 0 .67 43 0 .023 4.9 0 .66 49 0 .0037 .26 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 10   560 90 0 .68 47 0 .018 4.9 0 .84 47 0 .0035 .26 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 12   700 95 0 .41 42 0 .021 4.8 0 .85 47 0 .0037 .26 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 12   680 100 0 .71 45 0 .019 4.8 0 .84 47 0 .0011 .29 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 11   680 95 0 .41 40 0 .023 4.9 0 .86 47 0 .0010 .26 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 11   670 93 0 .69 45 0 .050 5.0 0 .65 50 0 .0031 .29 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 12   690 97 0 .54 43 0 .020 4.9 0 .87 48 0 .0011 .28 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 11   670 89 0 .64 43 0 .018 4.9 0 .80 47 0 .0037 .26 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 12   680 110 0 .64 45 0 .023 4.9 0 .68 49 0 .0011 .28 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 11   670 94 0 .41 41 0 .018 4.8 0 .87 47 0 .0041 .29 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 11   660 100 0 .66 42 0 .018 4.8 0 .87 49 0 .0036 .29 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 12   670 96 0 .58 43 0 .023 4.8 0 .84 47 0 .0036 .26 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 12   760 99 0 .56 43 0 .018 5.0 0 .68 49 0 .0027 .26 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 12   680 91 0 .57 43 0 .045 4.8 0 .83 47 0 .0011 .26 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 12   670 100 0 .67 41 0 .018 4.9 0 .66 49 0 .0011 .26 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 12   670 100 0 .55 43 0 .018 4.9 0 .67 49 0 .0012 .26 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 12   680 99 0 .70 44 0 .019 5.0 0 .65 49 0 .0010 .26 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 10   530 84 - - - - 0 .52 41 0 .024 4.8
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 9.4 560 83 - - - - 0 .58 43 0 .025 5.0
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 9.6 550 80 - - - - 0 .55 42 0 .024 5.0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 9.7 650 84 - - - - 0 .70 43 0 .021 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 11   680 92 - - - - 0 .53 41 0 .022 5.0
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 12   680 94 - - - - 0 .54 44 0 .022 4.8
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 12   690 94 - - - - 0 .45 45 0 .019 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 11   670 99 - - - - 0 .53 41 0 .027 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 12   670 100 - - - - 0 .57 42 0 .024 5.0
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 12   680 100 - - - - 0 .60 41 0 .019 4.9
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 12   680 100 - - - - 0 .40 43 0 .018 4.9
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 12   670 84 - - - - 0 .53 43 0 .025 5.0
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 12   670 100 - - - - 0 .58 44 0 .019 4.9
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 11   670 84 - - - - 0 .59 43 0 .019 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 12   690 100 - - - - 0 .46 44 0 .019 4.8
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 11   670 91 - - - - 0 .57 44 0 .017 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 12   680 100 - - - - 0 .57 44 0 .025 4.9
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 1 7.4 350 71 1 86    360 -32 3.3   240   0 1.9  190 -32 .57   18    - -
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 1 7.1 360 62 1 64    370 -32 3.0   220   0 1.9  180 -32 .61   18    - -
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 1 7.1 340 73 1 52    360 -32 4.7   230   0 2.0  190 -32 .59   18    - -
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 1 10   350 97 1 26    360 -32 4.5   220   0 2.0  190 -32 .62   18    - -
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 1 6.8 360 59 1 17    360 -32 2.9   230   0 2.0  180 -32 .59   18    - -
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 0 15   350 170 0 91    460 -32 3.0   230   0 1.9  180 -32 .58   18    - -
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 1 13   370 120 1 83    460 -32 4.2   230   0 2.0  180 -32 .61   18    - -
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 1 12   340 140 1 47    460 -32 3.1   220   0 2.0  180 -32 .57   18    - -
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 0 18   360 190 0 .67 41 0 .023 4.9 0 .64 49 0 .0011 .26 - -
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 0 18   370 200 0 .61 42 0 .023 5.0 0 .65 49 0 .0011 .26 - -
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 0 17   370 190 0 .60 43 0 .023 4.9 0 .91 47 0 .0011 .26 - -
floats-cdfpl/sine_1_false-unreach-call_true-termination.i 0 5.7 330 52 0 .65 41 0 .042 4.9 0 .83 47 0 .0034 .28 - -
floats-cdfpl/sine_2_false-unreach-call_true-termination.i 1 7.2 340 71 1 55    350 1 25     570   0 1.9  180 -32 .61   18    - -
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 0 7.0 360 61 0 91    390 0 97     610   0 2.0  190 -32 .57   18    - -
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1 6.3 400 53 1 23    340 0 97     460   0 1.9  180 -32 .58   18    - -
floats-cdfpl/square_2_false-unreach-call_true-termination.i 1 6.4 400 64 0 91    390 1 89     410   0 2.8  190 -32 .57   18    - -
floats-cdfpl/square_3_false-unreach-call_true-termination.i 1 5.6 310 51 1 76    350 0 97     440   0 1.9  180 -32 .57   18    - -
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 2 7.9 350 77 - - - - 0 900    540 0 960     1000  
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 2 7.6 330 67 - - - - 0 900    570 0 960     1000  
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 2 8.3 360 78 - - - - 0 900    570 0 960     900  
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 2 21   350 230 - - - - 0 900    550 0 960     980  
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 2 20   380 200 - - - - 0 900    830 0 960     960  
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 2 15   350 170 - - - - 0 900    580 0 960     940  
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 0 18   400 180 - - - - 0 .52 41 0 .019 4.8
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 0 18   400 220 - - - - 0 .56 41 0 .022 4.8
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 0 23   370 280 - - - - 0 .54 42 0 .047 4.8
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 0 19   380 190 - - - - 0 .42 44 0 .019 4.9
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 0 21   380 250 - - - - 0 .47 43 0 .019 5.0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 0 17   370 190 - - - - 0 .57 42 0 .018 4.9
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 0 18   370 190 - - - - 0 .62 41 0 .020 4.9
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 2 6.9 350 68 - - - - 0 900    500 0 960     850  
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 2 6.7 310 57 - - - - 0 900    490 0 960     850  
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 2 7.2 350 69 - - - - 0 900    660 0 960     820  
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 2 7.5 340 63 - - - - 2 670    600 0 960     760  
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 2 6.3 320 54 - - - - 2 580    540 0 960     830  
floats-cdfpl/square_4_true-unreach-call_true-termination.i 2 6.4 350 58 - - - - 2 680    580 2 650     860  
floats-cdfpl/square_5_true-unreach-call_true-termination.i 2 6.1 330 56 - - - - 2 520    510 2 540     730  
floats-cdfpl/square_6_true-unreach-call_true-termination.i 2 6.0 320 54 - - - - 2 280    500 2 410     790  
floats-cdfpl/square_7_true-unreach-call_true-termination.i 2 6.6 330 54 - - - - 2 830    490 2 180     720  
floats-cdfpl/square_8_true-unreach-call_true-termination.i 2 6.3 340 49 - - - - 2 60    360 2 130     600  
floats-cbmc-regression/float-div1_true-unreach-call.i 0 5.0 290 49 - - - - 0 .54 42 0 .024 4.9
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 0 4.9 300 45 - - - - 0 .63 41 0 .028 4.9
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i 2 3.7 230 32 - - - - 2 2.3  240 2 11     230  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 0 3.5 260 32 - - - - 0 .63 45 0 .022 4.9
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i 2 3.8 230 34 - - - - 2 3.0  240 2 8.9   230  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 0 4.7 310 43 - - - - 0 .57 44 0 .025 4.8
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i 2 3.7 240 33 - - - - 2 3.2  250 2 12     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i 2 3.6 230 33 - - - - 2 3.0  250 2 11     250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 3.9 240 38 - - - - 2 5.0  260 2 12     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 4.1 270 41 - - - - 0 .68 44 0 .022 5.0
floats-cbmc-regression/float-to-double1_true-unreach-call.i 0 3.8 240 37 - - - - 0 .56 44 0 .019 4.9
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i 2 3.7 230 38 - - - - 2 3.0  250 2 8.9   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i 2 3.8 240 35 - - - - 2 4.1  250 2 14     280  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i 2 3.4 320 40 - - - - 2 3.0  250 2 10     240  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i 0 5.7 310 48 - - - - 0 .48 43 0 .019 4.9
floats-cbmc-regression/float13_true-unreach-call_true-termination.i 2 3.8 240 38 - - - - 2 3.2  250 2 11     250  
floats-cbmc-regression/float14_true-unreach-call.i 0 3.6 240 32 - - - - 0 .43 44 0 .020 4.8
floats-cbmc-regression/float18_true-unreach-call.i 2 3.8 240 33 - - - - 2 28    410 0 4.0   200  
floats-cbmc-regression/float19_true-unreach-call.i 0 3.7 250 34 - - - - 0 .67 43 0 .019 4.8
floats-cbmc-regression/float1_true-unreach-call_true-termination.i 2 3.6 230 32 - - - - 2 2.9  250 2 9.2   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i -16 6.2 330 57 - - - - 2 3.1  260 2 18     390  
floats-cbmc-regression/float21_true-unreach-call.i 0 4.1 270 39 - - - - 0 .54 43 0 .020 4.9
floats-cbmc-regression/float22_true-unreach-call_true-termination.i 2 3.8 250 37 - - - - -16 4.9  280 2 340     1000  
floats-cbmc-regression/float2_true-unreach-call_true-termination.i 2 3.6 230 32 - - - - 2 3.2  240 2 11     270  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i 2 5.9 310 47 - - - - 2 3.4  270 2 15     320  
floats-cbmc-regression/float4_true-unreach-call.i 0 3.9 270 35 - - - - 0 .41 44 0 .019 5.0
floats-cbmc-regression/float5_true-unreach-call_true-termination.i 2 6.8 330 63 - - - - 2 3.9  260 2 31     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i 0 6.1 300 50 - - - - 0 .57 43 0 .019 5.0
floats-cbmc-regression/float8_true-unreach-call.i 0 4.7 280 38 - - - - 0 .57 43 0 .023 4.8
floats-cbmc-regression/float_lib1_true-unreach-call.i 0 3.2 210 32 - - - - 0 .60 41 0 .020 4.9
floats-cbmc-regression/float_lib2_true-unreach-call.i 0 4.1 250 37 - - - - 0 .53 41 0 .017 4.8
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c 0 5.0 290 44 0 .59 44 0 .019 4.9 0 .86 47 0 .0037 .26 - -
float-benchs/cast_union_loose_false-unreach-call_true-termination.c 0 5.6 320 44 0 .62 43 0 .020 4.9 0 .85 47 0 .0035 .26 - -
float-benchs/cast_union_tight_false-unreach-call_true-termination.c 0 5.1 310 41 0 .54 41 0 .018 4.8 0 .64 49 0 .0011 .26 - -
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c 0 6.0 320 48 0 .42 43 0 .019 4.9 0 .69 50 0 .0010 .26 - -
float-benchs/inv_Newton_false-unreach-call.c 0 5.7 310 57 0 .68 41 0 .041 4.9 0 .69 50 0 .0023 .26 - -
float-benchs/inv_square_false-unreach-call_true-termination.c 0 5.4 310 51 0 .55 44 0 .024 4.8 0 .85 47 0 .0011 .29 - -
float-benchs/nan_double_false-unreach-call_true-termination.c 0 4.9 290 42 0 .41 41 0 .023 4.9 0 .84 47 0 .0013 .27 - -
float-benchs/nan_float_false-unreach-call_true-termination.c 0 4.6 290 46 0 .53 43 0 .018 4.8 0 .87 48 0 .0011 .26 - -
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 0 8.4 480 75 0 .55 42 0 .022 5.0 0 .65 49 0 .0011 .26 - -
float-benchs/sqrt_poly2_false-unreach-call.c 0 6.4 330 51 0 .56 43 0 .019 5.0 0 .84 49 0 .0039 .26 - -
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 0 5.6 310 51 - - - - 0 .52 45 0 .021 4.9
float-benchs/Rump_double_true-unreach-call_true-termination.c 2 4.0 250 38 - - - - 2 3.4  250 2 25     970  
float-benchs/Rump_float_true-unreach-call_true-termination.c 2 4.0 250 35 - - - - 2 3.1  250 2 13     420  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c 2 3.9 240 38 - - - - 2 3.0  250 2 9.4   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c 2 4.0 250 35 - - - - 2 3.8  250 2 9.9   270  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c 2 3.9 240 41 - - - - 2 3.1  250 2 12     250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 0 6.4 330 55 - - - - 0 .69 44 0 .021 4.9
float-benchs/bary_diverge_true-unreach-call_true-termination.c 0 6.7 330 56 - - - - 0 .55 43 0 .021 4.8
float-benchs/cast_float_union_true-unreach-call.c 2 4.1 250 36 - - - - 2 2.7  250 2 4.6   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 0 6.5 320 59 - - - - 0 .57 44 0 .018 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 0 6.2 320 53 - - - - 0 .54 43 0 .018 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 0 5.4 310 49 - - - - 0 .57 44 0 .020 4.8
float-benchs/drift_tenth_true-unreach-call_true-termination.c 2 4.0 240 37 - - - - 2 14    330 2 380     660  
float-benchs/exp_loop_true-unreach-call.c 0 6.4 310 53 - - - - 0 .45 43 0 .025 4.9
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 0 6.2 340 59 - - - - 0 .48 43 0 .021 4.8
float-benchs/filter1_true-unreach-call_true-termination.c 0 6.1 320 56 - - - - 0 .47 44 0 .019 4.9
float-benchs/filter2_alt_true-unreach-call.c 0 6.8 330 55 - - - - 0 .54 43 0 .024 4.9
float-benchs/filter2_iterated_true-unreach-call.c 0 6.7 350 58 - - - - 0 .56 44 0 .019 4.9
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 0 5.8 300 54 - - - - 0 .60 41 0 .019 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c 0 7.2 350 58 - - - - 0 .54 44 0 .019 4.8
float-benchs/filter2_true-unreach-call_true-termination.c 0 5.6 300 47 - - - - 0 .54 44 0 .035 5.0
float-benchs/filter_iir_true-unreach-call.c 0 7.3 360 56 - - - - 0 .56 44 0 .026 4.9
float-benchs/float_double_true-unreach-call_true-termination.c 2 3.8 230 41 - - - - 2 3.1  250 2 10     260  
float-benchs/image_filter_true-unreach-call.c 0 10   640 86 - - - - 0 .48 43 0 .025 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c 0 5.8 320 53 - - - - 0 .62 41 0 .024 5.0
float-benchs/interpolation_true-unreach-call_true-termination.c 0 5.9 320 45 - - - - 0 .73 44 0 .020 5.0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c 0 5.9 320 50 - - - - 0 .56 44 0 .025 4.8
float-benchs/inv_square_int_true-unreach-call_true-termination.c 0 5.6 300 45 - - - - 0 .45 43 0 .019 4.8
float-benchs/inv_square_true-unreach-call_true-termination.c 2 5.8 310 48 - - - - 2 3.2  260 2 43     300  
float-benchs/loop_true-unreach-call.c 0 5.3 300 44 - - - - 0 .39 43 0 .024 4.8
float-benchs/mea8000_true-unreach-call.c 0 15   730 120 - - - - 0 .66 45 0 .021 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c 0 5.5 300 47 - - - - 0 .52 41 0 .019 5.0
float-benchs/nan_float_range_true-unreach-call_true-termination.c 0 5.0 300 42 - - - - 0 .67 42 0 .019 4.9
float-benchs/rlim_exit_true-unreach-call_true-termination.c 0 5.7 320 51 - - - - 0 .51 42 0 .019 4.9
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 0 5.8 310 48 - - - - 0 .57 44 0 .024 4.8
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 0 8.0 470 69 - - - - 0 .63 43 0 .019 4.9
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 0 8.2 480 74 - - - - 0 .41 43 0 .020 4.9
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 0 8.5 470 76 - - - - 0 .66 42 0 .021 4.9
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 11   520 90 - - - - 0 .59 43 0 .019 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 8.4 470 69 - - - - 0 .53 44 0 .019 4.8
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 6.3 330 59 - - - - 0 .73 44 0 .023 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 6.2 330 59 - - - - 0 .63 43 0 .021 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 6.2 320 59 - - - - 0 .64 41 0 .024 4.9
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 6.4 320 63 - - - - 0 .58 41 0 .019 5.0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 6.0 300 54 - - - - 0 .53 43 0 .018 4.8
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 0 5.7 330 57 - - - - 0 .54 44 0 .019 4.8
float-benchs/water_pid_true-unreach-call_true-termination.c 0 5.5 300 45 - - - - 0 .54 45 0 .018 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c 0 5.6 300 46 - - - - 0 .69 44 0 .019 4.9
float-benchs/zonotope_3_true-unreach-call_true-termination.c 0 5.5 320 52 - - - - 0 .61 44 0 .025 4.9
float-benchs/zonotope_loose_true-unreach-call_true-termination.c 0 5.7 320 51 - - - - 0 .60 41 0 .018 4.8
float-benchs/zonotope_tight_true-unreach-call_true-termination.c 0 5.5 320 51 - - - - 0 .41 44 0 .018 5.0
floats-esbmc-regression/Double_div_true-unreach-call.i 0 5.2 300 46 - - - - 0 .69 42 0 .021 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i 0 5.2 290 44 - - - - 0 .72 41 0 .020 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 4.2 290 43 - - - - 0 .65 41 0 .023 5.0
floats-esbmc-regression/ceil_true-unreach-call.i 0 3.8 250 38 - - - - 0 .58 41 0 .020 4.9
floats-esbmc-regression/copysign_true-unreach-call.i 0 4.0 270 37 - - - - 0 .53 42 0 .020 4.9
floats-esbmc-regression/digits_for_true-unreach-call.i 0 2.9 200 32 - - - - 0 .72 41 0 .020 4.9
floats-esbmc-regression/digits_while_true-unreach-call.i 0 2.9 200 27 - - - - 0 .45 43 0 .019 4.8
floats-esbmc-regression/fabs_true-unreach-call.i 0 3.9 240 38 - - - - 0 .54 44 0 .019 4.9
floats-esbmc-regression/fdim_true-unreach-call.i 0 3.9 260 39 - - - - 0 .46 43 0 .020 4.9
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 4.2 280 39 - - - - 0 .53 44 0 .019 5.0
floats-esbmc-regression/floor_true-unreach-call.i 0 4.0 260 34 - - - - 0 .63 42 0 .024 5.0
floats-esbmc-regression/fmax_true-unreach-call.i 0 3.9 250 34 - - - - 0 .52 46 0 .020 4.8
floats-esbmc-regression/fmin_true-unreach-call.i 0 3.8 250 38 - - - - 0 .64 41 0 .019 4.8
floats-esbmc-regression/fmod2_true-unreach-call.i 0 3.9 270 36 - - - - 0 .54 41 0 .020 4.9
floats-esbmc-regression/fmod3_true-unreach-call.i 0 3.9 260 36 - - - - 0 .58 41 0 .022 4.8
floats-esbmc-regression/fmod_true-unreach-call.i 2 3.8 240 34 - - - - 2 4.3  250 0 4.1   190  
floats-esbmc-regression/isgreater_true-unreach-call.i 2 4.2 240 37 - - - - 2 4.0  250 2 10     260  
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 4.0 240 38 - - - - 2 3.1  260 2 9.8   270  
floats-esbmc-regression/isless_true-unreach-call.i 2 4.1 240 34 - - - - 2 3.9  260 2 11     270  
floats-esbmc-regression/islessequal_true-unreach-call.i 2 3.8 250 39 - - - - 2 4.9  250 2 11     280  
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 4.1 240 40 - - - - 2 4.1  260 2 10     270  
floats-esbmc-regression/isunordered_true-unreach-call.i 2 4.0 240 35 - - - - 2 4.2  260 2 11     280  
floats-esbmc-regression/lrint_true-unreach-call.i 0 4.5 300 38 - - - - 0 .55 44 0 .022 4.8
floats-esbmc-regression/modf_true-unreach-call.i 0 3.9 250 36 - - - - 0 .46 44 0 .025 4.8
floats-esbmc-regression/nan_true-unreach-call.i 0 4.2 260 40 - - - - 0 .48 43 0 .018 5.0
floats-esbmc-regression/nearbyint2_true-unreach-call.i 0 3.7 240 33 - - - - 0 .67 43 0 .024 4.9
floats-esbmc-regression/nearbyint_true-unreach-call.i 0 3.8 240 33 - - - - 0 .54 44 0 .019 5.0
floats-esbmc-regression/remainder_true-unreach-call.i 0 4.5 300 38 - - - - 0 .57 44 0 .020 5.0
floats-esbmc-regression/rint2_true-unreach-call.i 0 4.0 240 33 - - - - 0 .49 43 0 .025 4.8
floats-esbmc-regression/rint_true-unreach-call.i 0 3.9 240 33 - - - - 0 .61 42 0 .024 4.8
floats-esbmc-regression/round_nondet_true-unreach-call.i 0 3.9 290 36 - - - - 0 .47 43 0 .021 5.0
floats-esbmc-regression/round_true-unreach-call.i 0 4.2 300 41 - - - - 0 .63 42 0 .021 4.9
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 4.0 240 37 - - - - 2 5.5  260 0 3.7   200  
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 0 4.0 260 39 - - - - 0 .41 43 0 .024 4.8
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 0 4.2 270 41 - - - - 0 .55 44 0 .019 4.9
floats-esbmc-regression/trunc_true-unreach-call.i 0 3.9 250 40 - - - - 0 .56 44 0 .023 4.8
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 0 5.4 300 45 0 .70 45 0 .023 5.0 0 .69 51 0 .0035 .30 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 0 5.3 300 44 0 .53 44 0 .019 5.0 0 .67 50 0 .0011 .26 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 0 3.0 200 33 0 .58 43 0 .023 5.0 0 .66 49 0 .0011 .26 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 0 2.9 200 28 0 .56 44 0 .023 4.9 0 .64 50 0 .0014 .28 - -
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i 0 8.2 470 64 0 .61 44 0 .039 4.9 0 .68 49 0 .0014 .29 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 12   680 89 0 .56 43 0 .020 4.9 0 .86 49 0 .0011 .26 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 0 8.4 410 77 0 .72 42 0 .018 4.9 0 .85 47 0 .0020 .26 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 8.4 470 73 0 .53 43 0 .023 4.9 0 .68 49 0 .0013 .28 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 7.4 370 68 0 .62 43 0 .019 4.9 0 .68 49 0 .0037 .30 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 7.2 370 57 0 .56 43 0 .021 5.0 0 .69 49 0 .0011 .26 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 8.4 460 71 - - - - 0 .55 44 0 .020 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 6.6 330 56 - - - - 0 .55 43 0 .018 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 13   710 97 - - - - 0 .39 43 0 .027 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 7.0 390 60 - - - - 0 .44 43 0 .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 8.3 460 69 - - - - 0 .54 43 0 .023 4.8
heap-manipulation/tree_true-unreach-call.i 0 7.7 390 65 - - - - 0 .54 43 0 .018 4.8
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 0 6.0 320 57 0 .58 44 0 .023 5.0 0 .87 47 0 .0012 .26 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 6.1 310 52 0 .69 45 0 .018 4.9 0 .83 47 0 .0011 .26 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 0 6.6 330 48 0 .39 41 0 .023 5.0 0 .82 47 0 .0035 .32 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 0 5.3 300 51 0 .54 44 0 .020 4.8 0 .85 47 0 .0010 .26 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 0 5.8 310 58 0 .64 43 0 .023 4.9 0 .68 49 0 .0026 .26 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 0 6.4 340 61 0 .57 43 0 .039 5.0 0 .85 47 0 .0011 .26 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 6.3 330 58 - - - - 0 .68 44 0 .021 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 6.5 320 58 - - - - 0 .54 43 0 .021 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 0 6.5 340 57 - - - - 0 .57 41 0 .019 5.0
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 6.7 320 52 - - - - 0 .57 41 0 .025 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 5.4 310 52 - - - - 0 .52 41 0 .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 5.7 320 50 - - - - 0 .47 43 0 .019 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 6.4 320 50 - - - - 0 .59 43 0 .021 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 5.0 300 48 1 4.0  260 -32 3.3   250   0 2.8  210 1 .61   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 5.5 320 51 1 4.4  270 -32 5.0   230   0 2.5  210 1 .69   18    - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 1 5.1 290 51 1 2.2  260 1 3.1   230   0 2.6  180 1 .55   18    - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 0 4.2 320 44 0 .58 43 0 .023 4.8 0 .84 47 0 .0036 .28 - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 5.1 300 51 1 4.0  250 -32 3.8   260   0 2.6  180 1 .60   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 5.2 320 52 1 3.2  260 -32 4.7   260   0 2.7  190 1 .56   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 5.3 310 45 1 3.3  260 -32 4.9   230   0 2.0  200 1 .56   18    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 0 6.3 310 59 0 .52 44 0 .019 4.9 0 .65 50 0 .0038 .28 - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 0 5.4 300 50 0 .65 42 0 .036 4.9 0 .66 49 0 .0011 .26 - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 0 39   700 370 0 .57 42 0 .023 4.8 0 .66 49 0 .0036 .29 - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 5.1 310 42 1 3.2  260 -32 5.0   260   0 2.8  210 1 .60   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 4.7 280 49 1 3.0  260 -32 3.3   270   0 2.6  190 1 .60   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 3.9 260 35 - - - - 2 3.0  250 2 7.6   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 4.1 250 39 - - - - 2 3.3  250 2 7.1   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 4.0 240 36 - - - - 2 3.2  250 2 5.9   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 3.6 240 33 - - - - 2 3.2  250 2 5.6   250  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 0 5.8 300 51 - - - - 0 .55 41 0 .019 4.9
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 3.7 230 32 - - - - 2 2.9  250 2 4.4   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 3.8 260 37 - - - - 2 3.7  250 2 6.5   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 4.4 270 35 - - - - 2 3.6  250 2 6.2   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 4.0 240 37 - - - - 2 3.9  250 2 5.0   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 3.9 240 39 - - - - 2 3.6  250 2 5.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 4.0 240 40 - - - - 2 3.2  250 2 9.6   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 3.7 240 31 - - - - 2 2.5  250 2 9.8   410  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 3.9 250 36 - - - - 2 2.9  250 2 7.4   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 4.0 240 37 - - - - 2 4.0  250 2 8.3   280  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 4.1 260 41 - - - - 2 3.1  250 2 5.7   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 3.9 260 40 - - - - 2 3.0  250 2 5.2   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 0 7.0 350 62 - - - - 0 .64 41 0 .018 4.9
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 0 6.0 330 55 - - - - 0 .63 42 0 .020 4.8
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 3.9 240 36 - - - - 2 3.7  260 2 10     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 4.2 260 40 - - - - 2 3.5  250 2 5.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 4.0 240 34 - - - - 2 2.9  250 2 5.7   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 4.3 250 39 - - - - 2 3.4  250 2 5.5   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 3.9 240 38 - - - - 2 3.9  250 2 5.4   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 4.0 240 39 - - - - 2 3.5  250 2 5.7   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 3.9 240 40 - - - - 2 3.7  250 2 6.4   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 5.4 310 44 - - - - 2 2.9  250 2 5.0   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 4.0 240 36 - - - - 2 3.0  250 2 5.2   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 3.9 240 33 - - - - 2 3.0  250 2 6.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 3.8 240 38 - - - - 2 4.0  250 2 5.5   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 4.0 240 34 - - - - 2 3.2  250 2 5.6   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 4.1 250 35 - - - - 2 3.2  240 2 5.5   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 4.2 290 35 - - - - 2 3.0  250 2 5.8   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 5.2 300 49 - - - - 2 2.9  250 2 6.8   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 3.9 230 36 - - - - 2 2.3  250 2 7.5   270  
ldv-regression/test02_false-unreach-call_true-termination.c 1 5.2 290 45 1 3.8  260 1 4.8   220   0 2.8  190 1 .56   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 5.1 310 53 1 2.3  260 -32 5.0   230   0 2.0  210 1 .60   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 0 4.7 290 45 0 .57 43 0 .018 4.8 0 .85 49 0 .0021 .26 - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 4.9 300 44 1 3.9  260 1 3.9   230   0 2.6  180 1 .55   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 0 5.5 320 50 0 .66 42 0 .021 4.8 0 .84 47 0 .0038 .26 - -
ldv-regression/test22_false-unreach-call.c 0 5.4 310 42 0 .57 43 0 .021 4.8 0 .88 48 0 .0032 .29 - -
ldv-regression/test23_false-unreach-call.c 0 5.6 320 48 0 .55 43 0 .017 4.8 0 .69 50 0 .0011 .28 - -
ldv-regression/test24_false-unreach-call.c 0 7.4 420 61 0 .67 41 0 .019 4.9 0 .81 47 0 .0035 .26 - -
ldv-regression/test25_false-unreach-call_true-termination.c 0 6.7 360 59 0 .57 43 0 .040 4.8 0 .64 50 0 .0018 .29 - -
ldv-regression/test26_false-unreach-call_true-termination.c 0 4.8 290 41 0 .55 41 0 .023 4.9 0 .66 49 0 .0013 .29 - -
ldv-regression/test27_false-unreach-call_true-termination.c 0 6.5 320 54 0 .56 44 0 .020 4.9 0 .64 49 0 .0011 .29 - -
ldv-regression/test28_false-unreach-call_true-termination.c 0 5.3 310 43 0 .59 43 0 .022 4.9 0 .82 47 0 .0036 .26 - -
ldv-regression/test29_false-unreach-call_true-termination.c 0 5.4 300 48 0 .56 43 0 .044 4.9 0 .68 49 0 .0011 .29 - -
ldv-regression/test30_false-unreach-call_true-termination.c 0 4.9 290 44 0 .62 43 0 .023 4.9 0 .86 48 0 .0011 .26 - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 3.8 230 36 - - - - 2 3.9  250 2 5.5   250  
ldv-regression/test03_true-unreach-call_true-termination.c 2 3.7 240 37 - - - - 2 3.1  250 2 6.7   270  
ldv-regression/test04_true-unreach-call_true-termination.c 2 3.7 240 33 - - - - 2 3.7  250 2 6.8   300  
ldv-regression/test05_true-unreach-call_true-termination.c 2 4.1 260 40 - - - - 2 3.9  250 2 11     480  
ldv-regression/test07_true-unreach-call_true-termination.c 2 4.1 270 43 - - - - 2 3.7  250 2 8.6   350  
ldv-regression/test09_true-unreach-call_true-termination.c 2 4.1 250 39 - - - - 2 3.5  250 2 8.6   340  
ldv-regression/test10_true-unreach-call_true-termination.c 0 5.1 290 44 - - - - 0 .49 43 0 .019 5.0
ldv-regression/test11_true-unreach-call_true-termination.c 2 4.0 250 36 - - - - 2 3.5  260 2 7.3   270  
ldv-regression/test13_true-unreach-call_true-termination.c 0 4.9 290 39 - - - - 0 .51 41 0 .024 5.0
ldv-regression/test14_true-unreach-call_true-termination.c 2 4.0 250 41 - - - - 2 3.2  250 2 8.2   280  
ldv-regression/test15_true-unreach-call_true-termination.c 2 4.0 250 36 - - - - 2 3.2  250 2 8.1   280  
ldv-regression/test16_true-unreach-call_true-termination.c 2 4.2 260 36 - - - - 2 3.1  250 2 8.8   300  
ldv-regression/test17_true-unreach-call_true-termination.c 2 3.9 240 36 - - - - 2 2.4  250 2 5.3   260  
ldv-regression/test18_true-unreach-call_true-termination.c 2 3.8 240 38 - - - - 2 3.2  250 2 8.7   300  
ldv-regression/test19_true-unreach-call_true-termination.c 2 4.0 240 35 - - - - 2 3.1  250 2 9.3   350  
ldv-regression/test20_true-unreach-call_true-termination.c 2 3.6 240 36 - - - - 2 3.1  250 2 5.8   260  
ldv-regression/test21_true-unreach-call_true-termination.c 2 4.4 290 41 - - - - 2 3.4  250 2 8.0   300  
ldv-regression/test22_true-unreach-call.c 2 4.3 290 38 - - - - 2 7.2  310 2 21     630  
ldv-regression/test23_true-unreach-call.c 2 4.7 300 38 - - - - 2 7.4  320 2 260     680  
ldv-regression/test24_true-unreach-call_true-termination.c 2 4.1 350 42 - - - - 2 5.3  280 2 9.4   410  
ldv-regression/test25_true-unreach-call.c 2 4.5 380 43 - - - - 2 20    470 2 30     530  
ldv-regression/test26_true-unreach-call_true-termination.c 2 4.0 250 41 - - - - 2 3.2  250 2 8.5   290  
ldv-regression/test27_true-unreach-call_true-termination.c 2 4.3 270 44 - - - - 2 33    500 2 160     820  
ldv-regression/test28_true-unreach-call_true-termination.c 0 5.5 310 53 - - - - 0 .42 43 0 .020 4.9
ldv-regression/test29_true-unreach-call_true-termination.c 0 5.6 330 57 - - - - 0 .62 41 0 .026 4.8
ldv-regression/test30_true-unreach-call_true-termination.c 0 5.5 310 49 - - - - 0 .46 44 0 .019 4.8
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 0 27   940 150 0 .57 41 0 .018 4.8 0 .66 50 0 .0017 .26 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 28   920 190 0 .42 41 0 .019 4.8 0 .67 49 0 .0036 .26 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 29   960 160 0 .59 44 0 .023 4.8 0 .85 47 0 .0014 .26 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 24   890 130 - - - - 2 6.4  280 2 13     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 24   920 140 - - - - 2 6.3  280 2 11     430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 25   920 150 - - - - 2 4.3  290 2 13     420  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 24   910 150 - - - - 2 6.1  280 2 14     440  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 23   920 140 - - - - 2 8.6  280 2 12     420  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 24   890 150 - - - - 2 6.4  280 2 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 25   920 150 - - - - 2 4.2  300 2 13     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 25   920 160 - - - - 2 6.4  290 2 13     420  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 24   910 150 - - - - 2 5.1  280 2 16     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 24   930 150 - - - - 2 6.9  280 2 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 0 6.9 360 54 0 .40 44 0 .018 4.8 0 .67 49 0 .0011 .29 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 0 6.6 320 60 0 .56 43 0 .020 4.8 0 .82 47 0 .0011 .29 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 0 6.7 370 60 0 .56 43 0 .018 5.0 0 .86 47 0 .0028 .34 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 0 6.9 390 57 0 .58 41 0 .046 5.0 0 .68 52 0 .0011 .26 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 6.9 330 57 0 .40 41 0 .021 4.8 0 .89 48 0 .0011 .26 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 7.1 390 59 0 .63 43 0 .018 4.9 0 .85 47 0 .0011 .26 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 6.8 350 58 0 .51 43 0 .017 4.8 0 .84 47 0 .0010 .26 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 0 7.5 400 64 0 .39 40 0 .018 4.8 0 .66 49 0 .0037 .29 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 0 6.7 350 58 0 .67 41 0 .022 4.8 0 .70 49 0 .0011 .26 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 6.6 330 55 0 .61 43 0 .019 5.0 0 .67 50 0 .0013 .30 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 0 7.3 380 64 0 .63 44 0 .020 4.9 0 .68 49 0 .0011 .26 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 0 6.1 320 54 0 .57 42 0 .040 4.8 0 .66 49 0 .0023 .26 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 0 6.7 350 52 0 .40 41 0 .033 4.8 0 .67 49 0 .0014 .28 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 0 7.0 380 63 0 .54 43 0 .018 4.9 0 .86 47 0 .0037 .26 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 6.0 310 55 0 .55 42 0 .020 5.0 0 .65 49 0 .0016 .26 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 0 6.1 330 48 0 .64 42 0 .022 4.8 0 .84 48 0 .0036 .30 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 6.7 330 57 0 .55 44 0 .018 5.0 0 .64 51 0 .0011 .26 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 0 6.6 330 56 0 .63 44 0 .020 4.9 0 .85 47 0 .0033 .26 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 0 6.1 320 52 0 .71 46 0 .019 4.8 0 .84 47 0 .0018 .26 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 6.3 330 45 - - - - 0 .53 42 0 .023 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 6.4 320 51 - - - - 0 .55 44 0 .019 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 7.1 340 59 - - - - 0 .71 42 0 .024 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 6.7 360 61 - - - - 0 .53 43 0 .047 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 6.4 330 59 - - - - 0 .47 44 0 .019 5.0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 7.0 380 64 - - - - 0 .66 41 0 .020 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 7.1 360 57 - - - - 0 .58 44 0 .024 5.0
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 6.5 320 60 - - - - 0 .58 44 0 .018 5.0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 7.4 400 63 - - - - 0 .59 44 0 .019 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 6.3 350 52 - - - - 0 .59 41 0 .021 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 6.3 330 59 - - - - 0 .60 44 0 .020 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 7.2 370 62 - - - - 0 .44 43 0 .019 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 6.3 320 59 - - - - 0 .57 43 0 .021 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 6.9 350 56 - - - - 0 .57 43 0 .024 5.0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 7.1 370 58 - - - - 0 .59 41 0 .019 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 6.2 320 55 - - - - 0 .56 41 0 .024 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 6.8 340 61 - - - - 0 .53 43 0 .020 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 6.3 350 53 - - - - 0 .66 43 0 .024 4.8
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 6.7 360 54 - - - - 0 .52 43 0 .021 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 7.3 380 65 - - - - 0 .47 43 0 .021 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 6.4 430 56 - - - - 0 .62 43 0 .019 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 0 8.7 540 66 0 .55 42 0 .019 4.8 0 .87 48 0 .0036 .26 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 6.0 320 53 0 .57 43 0 .023 5.0 0 .65 49 0 .0012 .26 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 0 5.8 340 54 0 .56 43 0 .018 4.8 0 .65 49 0 .0030 .29 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 0 7.4 420 63 0 .41 42 0 .018 5.0 0 .85 47 0 .0011 .26 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 7.4 390 59 - - - - 0 .55 45 0 .020 5.0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 0 7.6 410 73 0 .62 43 0 .018 4.8 0 .82 47 0 .0036 .29 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 7.3 380 65 - - - - 0 .65 42 0 .021 4.9
list-ext2-properties/simple_search_value_false-unreach-call.i 0 6.2 310 57 0 .64 44 0 .021 4.8 0 .66 49 0 .0011 .26 - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 6.6 320 58 - - - - 0 .56 43 0 .020 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 0 6.4 350 59 0 .61 44 0 .018 4.8 0 .84 47 0 .0037 .26 - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 0 8.8 520 83 0 .70 41 0 .035 4.8 0 .66 49 0 .0013 .29 - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 0 9.5 520 84 0 .63 43 0 .019 4.9 0 .83 47 0 .0020 .26 - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 9.2 520 68 0 .58 44 0 .020 4.8 0 .68 49 0 .0037 .26 - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 0 8.8 520 73 0 .56 43 0 .018 4.8 0 .64 49 0 .0011 .28 - -
ldv-sets/test_add_true-unreach-call_true-termination.i 0 6.6 350 53 - - - - 0 .50 46 0 .017 4.8
ldv-sets/test_mutex_true-unreach-call.i 0 9.3 530 71 - - - - 0 .55 45 0 .022 4.8
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 8.5 500 67 - - - - 0 .54 41 0 .019 4.8
loops/array_false-unreach-call_true-termination.i 1 5.4 310 53 1 4.1  260 -32 5.7   260   0 1.9  180 1 .57   18    - -
loops/bubble_sort_false-unreach-call.i 0 8.7 460 82 0 .59 45 0 .019 5.0 0 .83 47 0 .0030 .29 - -
loops/count_up_down_false-unreach-call_true-termination.i 1 5.1 310 46 1 3.8  250 1 3.1   250   0 2.0  210 1 .60   18    - -
loops/eureka_01_false-unreach-call_true-termination.i 0 58   760 660 0 .70 45 0 .018 4.9 0 .65 49 0 .0038 .26 - -
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 5.5 330 52 1 3.2  260 1 7.3   270   0 2.8  210 -32 .61   18    - -
loops/insertion_sort_false-unreach-call_true-termination.i 0 7.1 340 68 0 .73 45 0 .018 4.8 0 .66 49 0 .0036 .29 - -
loops/invert_string_false-unreach-call_true-termination.i 0 6.3 320 55 0 .68 41 0 .018 4.9 0 .86 48 0 .0021 .29 - -
loops/linear_search_false-unreach-call.i 0 25   720 260 -32 4.8  280 0 95     7000   0 3.3  210 -32 .62   19    - -
loops/ludcmp_false-unreach-call.i 0 5.6 330 45 0 .61 41 0 .039 4.9 0 .64 49 0 .0011 .26 - -
loops/matrix_false-unreach-call_true-termination.i 0 900   1400 8800 0 .63 43 0 .018 4.9 0 .85 48 0 .0016 .26 - -
loops/n.c24_false-unreach-call.i 0 4.3 300 39 0 .41 41 0 .018 4.9 0 .67 49 0 .0037 .30 - -
loops/nec11_false-unreach-call_false-termination.i 1 5.3 310 44 1 4.0  260 -32 6.0   230   0 1.9  210 1 .60   18    - -
loops/nec20_false-unreach-call_true-termination.i 1 5.5 300 45 1 3.4  260 1 3.8   260   0 1.9  180 1 .57   18    - -
loops/s3_false-unreach-call.i 0 9.7 530 77 0 .65 41 0 .018 4.9 0 .84 47 0 .0010 .29 - -
loops/string_false-unreach-call_true-termination.i 0 13   590 120 0 .57 43 0 .019 4.9 0 .65 50 0 .0010 .26 - -
loops/sum01_bug02_false-unreach-call_true-termination.i 1 8.2 340 63 1 4.8  270 1 11     520   0 2.8  210 -32 .60   18    - -
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 6.7 330 54 1 3.9  270 1 6.4   410   0 2.8  210 -32 .57   18    - -
loops/sum01_false-unreach-call_true-termination.i 1 10   470 85 1 6.0  270 1 9.0   500   0 2.9  210 -32 .57   18    - -
loops/sum03_false-unreach-call_true-termination.i 1 10   420 92 -32 3.5  250 0 97     490   0 2.7  180 1 .56   18    - -
loops/sum04_false-unreach-call_true-termination.i 1 4.9 290 50 1 3.6  260 -32 5.2   250   0 2.8  210 1 .60   18    - -
loops/sum_array_false-unreach-call.i 1 6.4 330 59 0 92    2000 1 6.0   260   0 2.7  210 -32 .57   18    - -
loops/terminator_01_false-unreach-call_true-termination.i 1 5.0 300 46 1 3.0  260 -32 5.2   220   0 1.9  180 1 .57   18    - -
loops/terminator_02_false-unreach-call_true-termination.i 1 5.8 320 52 1 4.0  260 -32 3.2   230   0 2.0  210 1 .57   18    - -
loops/terminator_03_false-unreach-call_true-termination.i 1 5.6 310 49 1 2.2  260 1 5.1   260   0 1.9  180 1 .56   18    - -
loops/trex01_false-unreach-call_true-termination.i 1 6.4 330 56 -32 3.8  270 1 5.4   260   0 1.9  180 -32 .58   18    - -
loops/trex02_false-unreach-call_true-termination.i 1 22   770 200 1 3.1  260 1 5.2   250   0 2.0  190 -32 .58   18    - -
loops/trex03_false-unreach-call_true-termination.i 1 6.0 340 53 1 4.2  260 1 3.6   260   0 2.1  210 1 .62   18    - -
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 0 4.6 290 43 0 .57 43 0 .019 4.8 0 .68 49 0 .0011 .26 - -
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 0 4.5 300 44 0 .40 41 0 .018 4.8 0 .67 49 0 .0010 .29 - -
loops/vogal_false-unreach-call.i 1 18   670 170 1 5.0  300 -32 3.9   260   0 2.1  210 -32 .58   18    - -
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 1 5.0 300 51 1 2.2  260 -32 4.5   260   0 2.0  190 1 .61   18    - -
loops/array_true-unreach-call_true-termination.i 2 3.8 250 33 - - - - 2 4.0  270 2 7.2   280  
loops/bubble_sort_true-unreach-call_true-termination.i 0 4.6 300 41 - - - - 0 .55 44 0 .024 4.8
loops/count_up_down_true-unreach-call_true-termination.i 2 4.0 250 41 - - - - 0 900    5000 2 16     330  
loops/eureka_01_true-unreach-call.i 0 29   710 300 - - - - 0 .56 44 0 .024 4.8
loops/eureka_05_true-unreach-call_true-termination.i 2 4.7 300 41 - - - - 0 900    6100 2 53     800  
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 2 3.9 260 41 - - - - 2 4.8  270 2 5.3   260  
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 2 4.1 250 35 - - - - 2 4.1  270 2 6.4   260  
loops/insertion_sort_true-unreach-call_true-termination.i 0 6.4 330 57 - - - - 0 .72 43 0 .022 4.9
loops/invert_string_true-unreach-call_true-termination.i 2 4.0 250 42 - - - - 2 24    520 2 180     770  
loops/linear_sea.ch_true-unreach-call.i 0 280   720 3500 - - - - 0 .63 41 0 .022 4.8
loops/lu.cmp_true-unreach-call.i 1 6.8 390 63 - - - - 0 900    5400 0 960     3800  
loops/matrix_true-unreach-call_true-termination.i 2 4.2 250 39 - - - - 2 4.4  270 2 10     380  
loops/n.c11_true-unreach-call_false-termination.i 2 25   720 260 - - - - 0 900    7000 2 10     360  
loops/n.c40_true-unreach-call_true-termination.i 2 7.4 330 62 - - - - 2 2.9  270 2 7.4   350  
loops/nec40_true-unreach-call_true-termination.i 2 8.2 340 65 - - - - 2 4.2  270 2 7.5   330  
loops/string_true-unreach-call_true-termination.i 2 5.2 310 50 - - - - 2 6.4  280 2 11     380  
loops/sum01_true-unreach-call_true-termination.i 2 4.1 290 35 - - - - 0 510    7000 2 9.9   380  
loops/sum03_true-unreach-call_false-termination.i 2 4.2 260 41 - - - - 2 4.0  270 2 6.0   260  
loops/sum04_true-unreach-call_true-termination.i 2 3.8 240 34 - - - - 2 4.2  270 2 9.8   440  
loops/sum_array_true-unreach-call.i 0 21   680 190 - - - - 0 .62 45 0 .019 4.9
loops/terminator_02_true-unreach-call_true-termination.i 2 32   740 330 - - - - 2 4.1  270 2 6.5   260  
loops/terminator_03_true-unreach-call_true-termination.i 2 4.0 250 40 - - - - 2 3.9  270 2 7.2   260  
loops/trex01_true-unreach-call_true-termination.i 2 9.8 400 91 - - - - 2 30    1100 2 7.1   260  
loops/trex02_true-unreach-call_true-termination.i 2 4.2 270 41 - - - - 2 3.1  260 2 5.6   250  
loops/trex03_true-unreach-call_true-termination.i 0 900   1300 9800 - - - - 0 .54 43 0 .019 4.8
loops/trex04_true-unreach-call_false-termination.i 2 4.3 290 43 - - - - 2 4.9  270 2 5.7   260  
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 0 5.1 310 38 - - - - 0 .39 43 0 .020 5.0
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 0 4.5 300 43 - - - - 0 .48 43 0 .025 4.8
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 2 4.8 310 41 - - - - 2 5.2  280 2 4.1   260  
loops/vogal_true-unreach-call.i 0 23   680 220 - - - - 0 .63 43 0 .021 4.9
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 2 4.1 240 36 - - - - 2 3.7  260 2 5.0   250  
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 2 3.9 240 33 - - - - 2 3.4  270 2 5.9   260  
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 2 4.0 250 33 - - - - 2 3.2  270 2 5.1   260  
loop-acceleration/array_false-unreach-call1_true-termination.i 0 140   720 1400 0 .57 42 0 .018 4.8 0 .85 47 0 .0011 .26 - -
loop-acceleration/array_false-unreach-call2_true-termination.i 1 5.1 290 43 0 97    1200 -32 4.7   250   0 1.9  210 1 .60   18    - -
loop-acceleration/array_false-unreach-call3_true-termination.i 0 49   700 560 0 .70 46 0 .023 4.9 0 .65 49 0 .0034 .26 - -
loop-acceleration/const_false-unreach-call1.i 0 220   700 2500 0 .66 42 0 .020 4.9 0 .70 50 0 .0011 .26 - -
loop-acceleration/diamond_false-unreach-call1.i 0 20   690 200 0 .52 43 0 .019 5.0 0 .69 49 0 .0037 .30 - -
loop-acceleration/functions_false-unreach-call1_true-termination.i 1 5.1 300 40 0 92    1900 -32 5.1   260   0 2.0  180 1 .97   18    - -
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 4.8 300 46 1 3.1  250 1 5.5   250   0 2.7  180 1 .60   18    - -
loop-acceleration/nested_false-unreach-call1.i 1 4.6 280 40 0 92    1900 -32 6.4   260   0 2.0  180 1 3.4    18    - -
loop-acceleration/phases_false-unreach-call1.i 0 280   760 3400 0 .61 43 0 .022 4.8 0 .83 47 0 .0041 .26 - -
loop-acceleration/phases_false-unreach-call2_false-termination.i 1 5.9 330 54 1 3.4  260 1 4.6   260   0 2.0  180 -32 .60   18    - -
loop-acceleration/simple_false-unreach-call1.i 1 5.3 400 49 0 91    1800 -32 3.4   260   0 2.0  190 1 .80   18    - -
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 4.9 300 44 1 3.0  260 1 5.7   250   0 2.8  190 1 .77   18    - -
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 5.1 290 49 1 3.8  260 1 3.3   250   0 1.9  180 1 .56   18    - -
loop-acceleration/simple_false-unreach-call4.i 1 4.8 280 41 0 92    1700 -32 3.9   260   0 2.6  180 1 .77   18    - -
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 1 5.1 300 44 1 3.1  260 -32 5.3   250   0 2.6  180 1 .58   18    - -
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 1 5.0 310 45 1 4.1  260 -32 3.3   250   0 2.0  180 1 .60   18    - -
loop-acceleration/array_true-unreach-call1_true-termination.i 2 21   690 180 - - - - 2 3.1  270 2 9.3   280  
loop-acceleration/array_true-unreach-call2_true-termination.i 1 3.8 240 35 - - - - 0 900    2700 0 960     3300  
loop-acceleration/array_true-unreach-call3_true-termination.i 2 4.3 260 34 - - - - 2 4.3  270 2 6.1   320  
loop-acceleration/array_true-unreach-call4_true-termination.i 0 48   700 610 - - - - 0 .65 42 0 .019 4.9
loop-acceleration/const_true-unreach-call1.i 2 4.3 260 43 - - - - 2 4.6  270 2 7.7   270  
loop-acceleration/diamond_true-unreach-call1_true-termination.i 0 20   710 180 - - - - 0 .55 43 0 .020 4.8
loop-acceleration/diamond_true-unreach-call2.i 0 26   750 270 - - - - 0 .61 41 0 .019 4.8
loop-acceleration/functions_true-unreach-call1_true-termination.i 1 3.6 240 34 - - - - 0 530    7000 0 960     680  
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 4.2 250 38 - - - - 2 770    6200 2 6.4   270  
loop-acceleration/nested_true-unreach-call1.i 2 3.9 240 39 - - - - 2 5.4  270 2 13     360  
loop-acceleration/overflow_true-unreach-call1.i 1 3.6 240 37 - - - - 0 640    7000 0 960     620  
loop-acceleration/phases_true-unreach-call1.i 0 280   760 3200 - - - - 0 .60 44 0 .022 4.8
loop-acceleration/phases_true-unreach-call2_false-termination.i 0 280   1100 2400 - - - - 0 .56 44 0 .022 4.8
loop-acceleration/simple_true-unreach-call1.i 1 4.0 240 36 - - - - 0 450    7000 0 960     570  
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 3.8 250 37 - - - - 2 4.3  260 2 6.7   270  
loop-acceleration/simple_true-unreach-call3_true-termination.i 1 4.1 250 36 - - - - 0 800    7000 0 960     570  
loop-acceleration/simple_true-unreach-call4.i 2 3.9 240 32 - - - - 2 3.3  270 2 6.8   260  
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 2 3.6 240 36 - - - - 2 5.6  280 2 59     440  
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 2 3.8 240 34 - - - - 2 4.3  260 2 6.9   270  
loop-crafted/simple_array_index_value_false-unreach-call1_false-termination.i 1 5.4 310 45 1 4.7  280 1 3.2   240   0 2.8  210 -32 .61   18    - -
loop-crafted/simple_array_index_value_true-unreach-call1_true-termination.i 0 28   680 240 - - - - 0 .56 43 0 .021 5.0
loop-crafted/simple_array_index_value_true-unreach-call2_true-termination.i 0 43   720 520 - - - - 0 .52 43 0 .019 4.9
loop-crafted/simple_array_index_value_true-unreach-call3_true-termination.i 0 45   710 430 - - - - 0 .56 42 0 .019 5.0
loop-crafted/simple_array_index_value_true-unreach-call4_true-termination.i 2 40   750 460 - - - - 0 900    1700 2 62     450  
loop-crafted/simple_vardep_true-unreach-call1_true-termination.i 2 4.3 260 37 - - - - 2 2.6  260 2 5.7   260  
loop-crafted/simple_vardep_true-unreach-call2_true-termination.i 2 4.1 260 40 - - - - 2 4.2  270 2 5.8   260  
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 6.0 330 51 1 3.4  260 -32 4.6   260   0 1.9  180 -32 .58   18    - -
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 2 38   740 370 - - - - 0 900    2600 2 8.6   330  
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 2 4.4 260 41 - - - - 0 670    7000 2 12     360  
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 63   720 720 - - - - 0 .55 41 0 .019 4.9
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 39   740 420 - - - - 0 .67 44 0 .022 5.0
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 75   720 1000 - - - - 0 .68 41 0 .019 4.8
loop-invgen/down_true-unreach-call_true-termination.i 1 28   750 320 - - - - 0 340    7000 0 960     4600  
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 1 28   710 320 - - - - 0 520    7000 0 960     4600  
loop-invgen/half_2_true-unreach-call_true-termination.i 1 30   740 300 - - - - 0 790    7000 0 960     4800  
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 110   840 1300 - - - - 0 .69 41 0 .019 4.9
loop-invgen/id_build_true-unreach-call_true-termination.i 2 38   750 420 - - - - 2 4.3  280 2 7.7   270  
loop-invgen/large_const_true-unreach-call_true-termination.i 2 39   760 480 - - - - 2 5.0  280 2 12     360  
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 900   1500 9600 - - - - 0 .54 44 0 .020 4.9
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900   1400 8800 - - - - 0 .55 42 0 .021 4.8
loop-invgen/nested9_true-unreach-call_true-termination.i 0 900   1500 10000 - - - - 0 .57 41 0 .018 4.9
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 2 30   750 300 - - - - 0 670    7000 2 17     550  
loop-invgen/seq_true-unreach-call_true-termination.i 1 35   730 430 - - - - 0 720    7000 0 960     1900  
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 250   750 2800 - - - - 0 .57 43 0 .026 4.8
loop-invgen/up_true-unreach-call_true-termination.i 1 29   740 290 - - - - 0 350    7000 0 960     4600  
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 0 400   740 4100 - - - - 0 .60 42 0 .021 4.9
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 2 52   790 570 - - - - 0 900    640 2 12     410  
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 23   700 190 - - - - 2 4.5  270 2 9.7   300  
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 2 6.1 320 56 - - - - 0 450    7000 2 8.8   310  
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 2 4.3 260 36 - - - - 2 4.3  270 2 6.5   260  
loop-lit/css2003_true-unreach-call_true-termination.c.i 2 31   750 340 - - - - 2 3.8  270 2 6.9   270  
loop-lit/ddlm2013_true-unreach-call.i 0 40   800 530 - - - - 0 .64 44 0 .024 4.9
loop-lit/gj2007_true-unreach-call_true-termination.c.i 2 3.6 240 31 - - - - 2 36    610 2 110     1300  
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 2 21   670 200 - - - - 0 900    2300 2 8.5   300  
loop-lit/gr2006_true-unreach-call_true-termination.c.i 0 300   740 3300 - - - - 0 .61 43 0 .020 4.8
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 2 54   850 540 - - - - 0 900    1300 2 6.6   260  
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 2 6.7 340 53 - - - - 0 460    7000 2 7.5   280  
loop-lit/jm2006_true-unreach-call_true-termination.c.i 2 4.0 250 41 - - - - 0 900    5000 2 8.0   280  
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 2 6.9 340 55 - - - - 0 900    4600 2 7.7   280  
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 6.0 330 51 - - - - 0 .62 42 0 .023 4.9
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 5.6 310 48 0 93    2100 1 3.7   260   0 2.0  210 1 .57   18    - -
loop-new/count_by_1_true-unreach-call_true-termination.i 2 3.8 250 41 - - - - 2 3.0  270 2 7.1   260  
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 4.1 250 43 - - - - 2 3.6  260 2 8.2   290  
loop-new/count_by_2_true-unreach-call_true-termination.i 1 4.0 250 36 - - - - 0 510    7000 0 960     4700  
loop-new/count_by_k_true-unreach-call_true-termination.i 0 270   710 3200 - - - - 0 .55 44 0 .020 4.9
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 480   770 5300 - - - - 0 .63 43 0 .018 4.8
loop-new/gauss_sum_true-unreach-call_true-termination.i 0 17   320 210 - - - - 0 .58 42 0 .020 5.0
loop-new/half_true-unreach-call_true-termination.i 0 26   720 290 - - - - 0 .58 41 0 .023 5.0
loop-new/nested_true-unreach-call_true-termination.i 2 6.7 350 67 - - - - 0 900    3500 2 38     820  
loop-industry-pattern/aiob_1_true-unreach-call.c 0 5.6 350 51 - - - - 0 .55 41 0 .018 4.9
loop-industry-pattern/aiob_2_true-unreach-call.c 0 5.2 340 52 - - - - 0 .45 44 0 .026 4.8
loop-industry-pattern/aiob_3_true-unreach-call.c 0 5.5 330 49 - - - - 0 .58 43 0 .019 4.9
loop-industry-pattern/aiob_4_true-unreach-call.c 0 4.1 270 41 - - - - 0 .52 41 0 .022 4.9
loop-industry-pattern/mod3_true-unreach-call.c 0 260   1100 2600 - - - - 0 .60 44 0 .019 4.9
loop-industry-pattern/nested_true-unreach-call.c 0 900   1200 8400 - - - - 0 .61 41 0 .019 4.8
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 7.4 510 60 - - - - 0 .54 42 0 .022 5.0
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 7.6 520 64 - - - - 0 .69 43 0 .024 4.8
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 7.7 510 59 - - - - 0 .47 43 0 .018 4.8
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 7.5 510 64 - - - - 0 .67 44 0 .019 5.0
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 7.5 560 56 - - - - 0 .55 43 0 .025 4.8
loops/heavy_true-unreach-call.c 1 6.6 790 60 - - - - 0 900    6700 0 120     7000  
loops/compact_false-unreach-call.c 0 110   690 1200 0 .59 44 0 .022 4.9 0 .65 49 0 .0036 .28 - -
loops/heavy_false-unreach-call.c 0 900   1400 6500 0 .59 44 0 .018 4.8 0 .84 47 0 .0038 .30 - -
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 0 4.1 260 42 0 .42 42 0 .023 4.9 0 .68 49 0 .0026 .30 - -
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 11   360 130 1 4.9  270 1 3.7   270   0 2.8  180 0 .61   18    - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 0 7.0 320 59 -32 3.4  260 -32 3.0   230   0 2.9  210 -32 .58   18    - -
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 5.7 330 49 1 3.7  260 1 5.4   250   0 2.7  180 1 .57   18    - -
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 0 3.9 250 33 0 .57 43 0 .021 4.8 0 .87 48 0 .0037 .26 - -
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 3.8 250 34 0 .53 43 0 .021 4.8 0 .85 47 0 .0039 .28 - -
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 0 4.1 240 36 0 .66 42 0 .018 5.0 0 .66 49 0 .0010 .27 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 3.7 250 36 - - - - 0 .56 43 0 .023 5.0
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 4.0 250 39 - - - - 0 .67 41 0 .018 5.0
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 3.9 320 40 - - - - 0 .55 44 0 .019 5.0
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 2 210   670 2300 - - - - 0 3.7  270 2 8.8   320  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 900   1600 10000 - - - - 0 .56 44 0 .020 5.0
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 260   740 2600 - - - - 0 .56 43 0 .021 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 3.9 250 35 - - - - 0 .68 45 0 .024 4.8
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 4.0 240 42 - - - - 0 .66 46 0 .019 4.9
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 3.8 250 36 - - - - 0 .54 42 0 .018 4.8
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 3.8 250 35 - - - - 0 .51 43 0 .019 4.8
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900   1500 9200 - - - - 0 .55 42 0 .020 4.9
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 4.8 300 44 - - - - 0 .59 43 0 .019 5.0
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 2 34   730 380 - - - - 0 3.3  250 2 11     350  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 210   740 2900 - - - - 0 .50 42 0 .019 4.9
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 3.9 270 32 - - - - 0 .57 44 0 .019 4.8
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 3.7 240 38 - - - - 0 .53 44 0 .021 4.8
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 3.7 240 35 - - - - 0 .56 44 0 .019 4.8
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 0 3.9 250 38 0 .41 41 0 .019 4.8 0 .65 49 0 .0011 .26 - -
recursive-simple/afterrec_false-unreach-call_true-termination.c 0 3.6 230 31 0 .55 43 0 .023 4.8 0 .66 49 0 .0011 .26 - -
recursive-simple/fibo_10_false-unreach-call_true-termination.c 0 4.1 340 35 0 .71 42 0 .019 5.0 0 .66 50 0 .0035 .28 - -
recursive-simple/fibo_15_false-unreach-call.c 0 3.9 250 31 0 .72 46 0 .021 4.8 0 .69 50 0 .0033 .29 - -
recursive-simple/fibo_20_false-unreach-call.c 0 3.9 250 33 0 .60 44 0 .020 4.8 0 .86 47 0 .0036 .29 - -
recursive-simple/fibo_25_false-unreach-call.c 0 3.7 250 31 0 .66 43 0 .018 4.9 0 .70 52 0 .0041 .26 - -
recursive-simple/fibo_2calls_10_false-unreach-call.c 0 4.2 270 37 0 .54 43 0 .023 4.9 0 .68 49 0 .0035 .31 - -
recursive-simple/fibo_2calls_15_false-unreach-call.c 0 4.2 270 35 0 .42 41 0 .019 4.9 0 .68 49 0 .0037 .26 - -
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 4.1 270 34 0 .56 44 0 .021 5.0 0 .70 50 0 .0011 .26 - -
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 4.1 270 36 0 .53 41 0 .019 4.9 0 .68 51 0 .0036 .26 - -
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 5.4 320 43 1 4.0  260 -32 3.3   230   0 2.8  210 1 .60   18    - -
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 0 4.0 270 41 0 .58 44 0 .018 4.8 0 .65 49 0 .0036 .26 - -
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 0 4.0 270 34 0 .57 44 0 .023 4.9 0 .86 47 0 .0012 .26 - -
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 0 4.3 270 39 0 .58 44 0 .018 4.9 0 .68 49 0 .0011 .26 - -
recursive-simple/fibo_2calls_8_false-unreach-call_true-termination.c 0 4.3 270 42 0 .67 45 0 .022 4.9 0 .85 48 0 .0011 .28 - -
recursive-simple/fibo_5_false-unreach-call_true-termination.c 0 3.8 250 35 0 .41 42 0 .018 4.8 0 .66 49 0 .0011 .28 - -
recursive-simple/fibo_7_false-unreach-call_true-termination.c 0 3.9 240 38 0 .63 44 0 .030 4.9 0 .88 49 0 .0036 .28 - -
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 4.2 260 39 0 .57 43 0 .018 4.8 0 .68 49 0 .0035 .28 - -
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 0 3.9 250 35 0 .60 44 0 .019 4.9 0 .66 50 0 .0011 .26 - -
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c 0 3.8 260 37 0 .61 43 0 .022 4.8 0 .84 47 0 .0010 .26 - -
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 4.9 290 42 1 3.6  270 -32 4.1   220   0 2.0  190 1 .61   18    - -
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 4.7 290 39 1 2.8  270 -32 2.9   220   0 1.8  180 1 .57   18    - -
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 5.0 290 45 1 3.7  270 -32 3.1   220   0 2.6  180 1 .57   18    - -
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 5.0 290 43 1 3.9  270 -32 4.1   210   0 2.7  190 1 .57   18    - -
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 4.8 290 46 1 3.5  270 -32 5.0   210   0 2.6  180 1 .61   18    - -
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c 0 5.3 310 49 0 91    2500 -32 3.8   260   0 2.6  180 -32 .57   18    - -
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c 1 5.1 290 43 1 5.0  440 -32 3.4   260   0 2.7  180 -32 .58   18    - -
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c 1 5.1 290 47 1 2.5  270 -32 5.3   260   0 1.9  180 -32 .57   18    - -
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c 1 5.0 300 46 1 8.0  670 -32 3.9   260   0 1.9  180 -32 .57   18    - -
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c 1 5.0 280 50 1 4.5  290 -32 5.2   260   0 2.6  180 -32 .57   18    - -
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c 1 5.2 300 47 1 4.3  260 -32 5.0   260   0 1.9  180 -32 .60   18    - -
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 5.0 300 45 1 3.4  270 -32 5.1   220   0 2.6  180 1 .56   18    - -
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 5.0 300 46 1 2.7  270 -32 3.7   220   0 1.9  180 1 .60   18    - -
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 5.2 320 44 1 4.7  290 -32 4.6   220   0 1.9  180 1 .57   18    - -
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 5.2 300 44 1 4.3  270 -32 3.7   210   0 2.0  180 1 .60   18    - -
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 5.1 330 45 1 3.5  260 -32 3.6   230   0 2.8  180 1 .56   18    - -
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c 1 5.0 290 43 1 3.4  250 -32 3.0   230   0 2.1  180 1 .61   18    - -
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 2 4.1 260 37 - - - - 2 2.9  250 2 5.2   260  
recursive-simple/afterrec_true-unreach-call_true-termination.c 2 3.9 240 35 - - - - 2 3.2  260 2 5.2   260  
recursive-simple/fibo_10_true-unreach-call_true-termination.c 0 4.0 240 36 - - - - 0 .55 43 0 .019 4.8
recursive-simple/fibo_15_true-unreach-call.c 0 3.9 250 36 - - - - 0 .53 41 0 .023 4.9
recursive-simple/fibo_20_true-unreach-call.c 0 3.9 240 40 - - - - 0 .70 43 0 .021 5.0
recursive-simple/fibo_25_true-unreach-call.c 0 3.4 250 31 - - - - 0 .58 44 0 .019 4.9
recursive-simple/fibo_2calls_10_true-unreach-call.c 0 4.0 270 44 - - - - 0 .54 44 0 .019 4.9
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 4.0 260 42 - - - - 0 .70 42 0 .021 4.9
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 3.8 270 36 - - - - 0 .55 43 0 .019 4.8
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 4.1 270 39 - - - - 0 .58 44 0 .020 5.0
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 2 4.6 280 47 - - - - 2 3.8  250 2 9.3   370  
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 0 4.1 270 37 - - - - 0 .62 42 0 .019 4.8
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 0 4.2 280 36 - - - - 0 .57 44 0 .024 5.0
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 0 3.8 260 35 - - - - 0 .53 41 0 .019 4.8
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 0 3.9 270 36 - - - - 0 .59 42 0 .019 4.8
recursive-simple/fibo_5_true-unreach-call_true-termination.c 0 3.8 240 39 - - - - 0 .51 43 0 .018 4.8
recursive-simple/fibo_7_true-unreach-call_true-termination.c 0 3.9 240 32 - - - - 0 .53 43 0 .020 5.0
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 3.6 260 34 - - - - 0 .47 43 0 .024 4.8
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 4.3 260 35 - - - - 0 .48 45 0 .020 4.8
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 3.9 250 39 - - - - 0 .53 43 0 .020 4.9
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 0 4.0 250 37 - - - - 0 .56 43 0 .020 4.9
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c 0 4.0 250 38 - - - - 0 .60 43 0 .023 5.0
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c 0 3.8 240 36 - - - - 0 .57 41 0 .019 4.9
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c 0 3.8 240 36 - - - - 0 .65 41 0 .024 5.0
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 2 3.9 240 38 - - - - 0 3.2  250 2 16     510  
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 2 3.7 240 36 - - - - 0 3.4  250 2 19     640  
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 2 3.8 240 39 - - - - 0 4.0  250 2 27     750  
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 2 3.4 230 31 - - - - 0 3.2  250 2 37     810  
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 2 3.6 240 35 - - - - 0 2.4  250 2 11     430  
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 2 3.7 240 34 - - - - 0 4.0  240 2 21     550  
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 2 3.9 240 35 - - - - 0 2.9  250 2 29     680  
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 2 3.7 240 33 - - - - 0 3.2  250 2 34     760  
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 2 3.8 240 34 - - - - 0 2.8  250 2 48     910  
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 2 3.8 240 34 - - - - 0 3.2  250 2 9.5   360  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c 2 4.2 240 42 - - - - 0 3.1  250 2 11     320  
/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
total 923 541 30000   430000 310000 298 -153 2500 56000 298 -1923 990 33000 298 0 370 28000 298 -1094 75 1800 625 316 58000   330000 625 388 49000 210000
    correct results 315 543 2800   110000 27000 71 71 760 21000 29 29 250 8300 0 58 58 53 1100 166 332 6300   56000 194 388 6100 86000
        correct true 228 456 2300   83000 22000 0 0 0 0 166 332 6300   56000 194 388 6100 86000
        correct false 87 87 550   29000 5100 71 71 760 21000 29 29 250 8300 0 58 58 53 1100 0 0
    correct-unconfimed results 22 14 270   9800 2900 0 0 0 0 0 0
        correct-unconfirmed true 14 14 190   6600 2000 0 0 0 0 0 0
        correct-unconfirmed false 8 0 84   3200 840 0 0 0 0 0 0
    incorrect results 1 -16 6.2 330 57 7 -224 29 1900 61 -1952 250 15000 0 36 -1152 21 660 1 -16 4.9 280 0
        incorrect true 0 7 -224 29 1900 61 -1952 250 15000 0 36 -1152 21 660 0 0
        incorrect false 1 -16 6.2 330 57 0 0 0 0 1 -16 4.9 280 0
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]