Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 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* [apollon013; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon089; apollon164] [apollon077; apollon078; apollon089; apollon134] [apollon022; apollon077; apollon078]
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]
Date of execution 2017-12-01 10:20:37 CET 2017-12-01 11:18:40 CET 2017-12-01 11:36:11 CET 2017-12-01 11:38:17 CET 2017-12-01 11:21:10 CET
Run set 2ls.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_1020.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/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2017-12-01_1020.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 1 .13  24 .86 1 3.8  260 1 2.9   220   -32 .78   18    -
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 1 .14  24 .95 1 4.2  260 1 5.6   260   -32 .61   18    -
signedintegeroverflow-regression/Division_false-no-overflow.c.i 1 .10  24 1.0  1 4.1  260 1 5.8   240   -32 .70   18    -
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 1 .14  24 .85 1 2.8  260 1 4.7   220   -32 .60   18    -
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 1 .10  24 .89 1 4.6  290 1 5.5   220   -32 .77   18    -
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 1 .12  24 .93 1 2.8  260 1 4.9   240   1 .72   18    -
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 1 .10  24 1.3  1 4.0  260 1 4.3   220   1 .79   18    -
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 1 .13  24 .81 -32 4.0  280 1 3.3   250   1 .77   18    -
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 1 .13  24 .92 -32 2.6  260 1 4.7   220   1 .62   18    -
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 1 .14  24 .77 1 2.8  270 1 4.9   240   -32 .61   19    -
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i 2 .12  24 .80 - - - 2 3.0   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i 2 .13  24 .80 - - - 2 3.5   260  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i 2 .11  24 .79 - - - 2 2.8   220  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i 2 .11  24 .91 - - - 2 3.0   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i 2 .11  24 .78 - - - 2 2.8   220  
termination-crafted/2Nested_false-no-overflow.c 1 .11  22 .77 1 2.4  270 1 5.2   220   1 .62   18    -
termination-crafted/4NestedWith3Variables_false-no-overflow.c 1 .15  24 .98 1 3.9  300 1 3.5   230   1 .63   18    -
termination-crafted/Ackermann_false-no-overflow.c 0 .098 22 .71 0 .42 44 0 .020 5.0 0 .0015 .26 -
termination-crafted/Bangalore_false-no-overflow.c 1 .14  22 .92 1 4.0  260 1 5.2   220   1 .73   18    -
termination-crafted/Bangalore_v3_false-no-overflow.c 1 .11  22 .95 1 2.3  260 1 4.5   220   1 .69   18    -
termination-crafted/Benghazi_nondet_false-no-overflow.c 1 .13  23 .87 1 2.4  260 1 4.8   230   1 .60   18    -
termination-crafted/Binary_Search_false-no-overflow.c 0 .10  22 .65 0 .41 43 0 .020 4.9 0 .0016 .26 -
termination-crafted/Cairo_nondet_false-no-overflow.c 1 .13  23 .98 1 2.3  260 -32 4.8   220   -32 .77   18    -
termination-crafted/Cairo_step2_false-no-overflow.c 0 900     1300 11000    0 .41 41 0 .047 4.8 0 .0011 .30 -
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 1 .11  23 .98 1 2.4  270 1 5.9   260   1 .69   18    -
termination-crafted/Copenhagen_disj_false-no-overflow.c 1 .13  23 .75 1 3.3  260 1 4.7   250   1 .77   18    -
termination-crafted/Gothenburg_false-no-overflow.c 1 .13  25 1.2  1 3.7  270 1 5.2   250   1 .68   18    -
termination-crafted/Gothenburg_v2_false-no-overflow.c 1 .13  25 .97 1 2.6  270 1 7.3   260   1 .75   18    -
termination-crafted/Hanoi_2vars_false-no-overflow.c 1 .12  22 1.0  1 2.3  270 1 4.3   220   1 .60   18    -
termination-crafted/Hanoi_3vars_false-no-overflow.c 1 .11  23 .80 1 2.4  260 1 5.3   230   1 .71   18    -
termination-crafted/Hanoi_plus_false-no-overflow.c 1 .13  23 .86 1 2.5  260 1 5.4   230   1 .72   18    -
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 1 .12  22 .86 1 2.2  260 1 4.2   260   1 .70   18    -
termination-crafted/Mysore_false-no-overflow.c 1 .12  23 .81 1 3.5  260 1 3.9   260   1 .67   18    -
termination-crafted/NestedRecursion_1a_false-no-overflow.c 0 .12  22 .68 0 .53 43 0 .019 4.8 0 .0014 .27 -
termination-crafted/NestedRecursion_2a_false-no-overflow.c 0 .12  22 .75 0 .52 43 0 .022 4.8 0 .0016 .26 -
termination-crafted/NonTermination1_false-no-overflow.c 1 .12  23 .87 1 3.4  270 1 4.0   220   1 .76   18    -
termination-crafted/NonTermination2_false-no-overflow.c 1 .14  23 .86 1 3.5  270 1 3.2   220   -32 .58   18    -
termination-crafted/NonTermination4_false-no-overflow.c 1 .53  41 5.7  1 34    970 0 78     7000   1 .75   18    -
termination-crafted/NonTerminationSimple2_false-no-overflow.c 1 .14  22 .77 1 3.2  260 1 4.3   220   1 .66   18    -
termination-crafted/NonTerminationSimple3_false-no-overflow.c 1 .099 23 1.0  1 3.5  260 1 4.5   210   1 .76   18    -
termination-crafted/NonTerminationSimple4_false-no-overflow.c 0 900     1200 13000    0 .53 43 0 .032 4.8 0 .0014 .26 -
termination-crafted/NonTerminationSimple5_false-no-overflow.c 1 .13  22 .82 1 2.3  260 1 6.2   260   1 .68   18    -
termination-crafted/NonTerminationSimple6_false-no-overflow.c 1 .14  22 .91 1 2.3  260 1 5.1   220   1 .70   19    -
termination-crafted/NonTerminationSimple8_false-no-overflow.c 1 .13  22 1.1  1 3.3  260 1 4.9   230   1 .69   18    -
termination-crafted/NonTerminationSimple9_false-no-overflow.c 1 .14  22 .80 1 3.4  260 1 4.4   220   -32 .65   18    -
termination-crafted/Pure2Phase_false-no-overflow.c 1 .13  22 .87 1 2.3  260 1 5.2   250   1 .58   18    -
termination-crafted/Pure3Phase_false-no-overflow.c 1 .14  23 .85 1 2.4  260 1 4.6   230   1 .63   18    -
termination-crafted/RecursiveMultiplication_false-no-overflow.c 0 .10  22 .65 0 .42 44 0 .042 4.9 0 .0029 .26 -
termination-crafted/RecursiveNonterminating_false-no-overflow.c 0 .12  22 .71 0 .55 43 0 .023 4.8 0 .0015 .26 -
termination-crafted/Rotation180_false-no-overflow.c 1 .11  24 .68 1 2.2  260 1 4.3   220   0 .69   18    -
termination-crafted/Singapore_false-no-overflow.c 1 .12  23 .81 1 3.4  260 1 5.6   230   1 .75   18    -
termination-crafted/Singapore_plus_false-no-overflow.c 1 .11  23 1.0  1 2.2  260 1 4.8   230   1 .58   18    -
termination-crafted/Singapore_v1_false-no-overflow.c 1 .12  23 1.0  1 3.3  260 1 5.8   230   1 .70   18    -
termination-crafted/Singapore_v2_false-no-overflow.c 1 .12  23 .83 1 3.5  270 1 4.9   230   1 .60   18    -
termination-crafted/Stockholm_false-no-overflow.c 1 .12  23 .89 1 3.4  260 1 4.4   220   1 .59   18    -
termination-crafted/Thun_false-no-overflow.c 1 .13  23 .76 1 3.2  260 1 3.1   210   1 .71   18    -
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 1 .12  23 1.1  1 3.4  260 1 7.1   260   1 .60   18    -
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 1 .12  24 1.1  1 2.6  270 1 8.2   290   1 .97   18    -
termination-crafted/aaron2_false-no-overflow.c 1 .14  25 .85 1 2.5  270 1 4.6   260   -32 .60   18    -
termination-crafted/aaron3_false-no-overflow.c 1 .14  23 .76 1 2.4  270 1 5.2   260   -32 .72   18    -
termination-crafted/easy2_false-no-overflow.c 0 900     1700 12000    0 .40 41 0 .023 4.9 0 .0015 .26 -
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 2 .19  24 1.4  - - - 2 3.1   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 2 5.9   200 66    - - - 2 36     820  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 2 3.0   100 31    - - - 2 3.4   260  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.3   170 37    - - - 2 4.8   280  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 2 .10  22 .73 - - - 2 4.6   280  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 2 .087 23 .86 - - - 2 5.8   260  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 2 .17  24 1.2  - - - 2 4.4   280  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     310 8400    - - - 0 .018 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 2 .12  22 .68 - - - 2 4.3   210  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1300 12000    - - - 0 .018 4.8
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1400 13000    - - - 0 .018 4.9
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 2 .11  23 .87 - - - 2 4.5   260  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 2 .11  23 .83 - - - 2 3.8   260  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 1 6.3   280 63    - - - 0 960     4800  
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 0 .16  24 1.7  - - - 0 .018 4.9
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 2 .13  22 .69 - - - 2 2.8   210  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1500 10000    - - - 0 .018 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 0 .10  22 .64 - - - 0 .042 4.8
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     750 7700    - - - 0 .018 4.8
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 0 .12  22 .69 - - - 0 .031 4.9
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 .12  22 .66 - - - 0 .020 4.9
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 .12  22 .64 - - - 0 .018 4.9
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 0 .11  22 .67 - - - 0 .020 4.9
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 0 .10  22 .84 - - - 0 .018 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 0 .086 22 .64 - - - 0 .018 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 0 .097 22 .64 - - - 0 .018 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 2 .11  23 .80 - - - 2 2.8   210  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 2 .12  22 .84 - - - 2 4.5   260  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 2 .11  25 .81 - - - 2 3.8   260  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 2 .11  23 .83 - - - 2 3.8   270  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 2 .14  23 .75 - - - 2 3.7   260  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 2 .15  23 1.7  - - - 2 4.4   260  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 2 .11  23 .72 - - - 2 5.8   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 2 .10  22 .74 - - - 2 3.5   260  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2 .10  22 .84 - - - 2 2.8   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 2 .10  22 .72 - - - 2 2.8   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 2 .11  22 .92 - - - 2 3.9   270  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1700 9900    - - - 0 .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 1 .15  23 .84 1 3.5  260 1 5.6   250   1 .71   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 1 .13  26 1.1  1 3.2  260 1 4.4   260   1 .62   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 1 .11  23 .93 1 2.4  260 1 5.4   260   -32 .58   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 1 .14  23 .88 1 3.4  260 1 6.6   250   -32 .58   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 1 .13  23 .98 1 2.4  260 1 6.8   260   1 .77   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 1 .14  25 .96 1 3.3  260 1 6.4   230   1 .71   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 1 .13  23 1.1  1 3.7  260 1 7.4   270   1 .75   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c 0 900     1700 12000    0 .40 43 0 .023 4.8 0 .0015 .26 -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 1 .14  23 .90 1 2.4  260 1 5.2   260   1 .71   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 1 .12  22 .87 1 3.0  260 1 4.7   250   1 .74   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c 0 900     3000 5800    0 .43 42 0 .029 4.8 0 .0017 .29 -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c 0 900     1000 9500    0 .40 43 0 .018 4.8 0 .0014 .34 -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 1 .14  23 .84 1 3.4  270 1 4.6   230   1 .72   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 1 .14  25 .85 1 2.4  260 1 5.4   280   1 .74   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 1 .13  22 .80 1 3.2  260 1 6.1   260   1 .77   18    -
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 1 .14  23 .83 1 3.4  260 1 4.6   260   1 .63   18    -
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 1 .13  23 .86 1 2.3  260 1 4.3   270   1 .70   18    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 1 .15  29 1.5  1 3.6  260 1 5.3   230   1 .72   18    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 1 .11  23 .82 1 2.5  260 1 4.4   260   1 .71   18    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 1 .11  23 1.0  1 3.4  260 1 5.4   260   -32 .72   18    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 1 .13  23 .82 1 2.6  270 1 5.9   260   -32 .60   19    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 1 .14  23 .94 1 2.6  270 1 6.2   270   1 .59   18    -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 1 .13  24 .81 1 2.3  260 1 5.5   240   1 .61   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 1 .11  23 .95 1 2.5  270 1 3.5   260   1 .77   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 1 .12  23 .86 1 2.6  290 1 4.6   230   -32 .62   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 1 .10  23 1.1  1 4.0  260 1 6.7   260   1 .59   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 1 .10  23 .75 1 2.5  270 1 3.2   230   1 .66   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 1 .14  23 .88 1 3.4  270 1 3.1   230   1 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 1 .13  22 .81 1 2.3  260 1 4.4   220   1 .70   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 1 .14  23 .83 1 2.3  260 1 3.6   260   1 .71   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 1 .14  23 .82 1 3.4  270 1 4.2   240   1 .59   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 1 .10  23 1.1  1 2.3  260 1 4.7   220   1 .68   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 1 .11  23 .84 1 2.3  260 1 4.2   210   1 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 1 .15  24 1.1  1 3.5  260 1 4.6   230   1 .67   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 1 .13  23 .98 1 2.6  280 1 4.6   220   1 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 1 .14  23 .85 1 3.3  270 1 4.5   210   1 .76   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 1 .14  23 .88 1 2.5  270 1 6.3   260   1 .61   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 1 .10  23 .87 1 2.3  260 1 5.9   250   1 .70   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 1 .15  24 .77 1 3.5  260 1 4.7   230   1 .65   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 1 .14  23 .83 1 2.4  270 1 3.5   220   1 .70   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 1 .12  23 .89 1 2.4  260 1 4.7   230   1 .60   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 1 .14  23 .88 1 3.5  270 1 5.8   230   1 .58   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 1 .13  22 .89 1 2.3  270 1 5.0   220   1 .61   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 1 .11  23 .81 1 3.1  260 1 3.2   250   1 .77   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 1 .13  22 .84 1 2.4  260 1 4.7   220   1 .77   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 1 .11  23 .97 1 2.4  280 1 3.3   230   1 .60   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 1 .13  23 .84 0 91    320 1 5.5   270   1 .77   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 1 .11  23 1.0  1 2.3  270 1 5.7   220   -32 .71   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 1 .12  22 .92 1 2.3  260 1 4.8   230   -32 .67   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 1 .12  23 .73 1 2.3  260 1 4.9   240   1 .77   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 1 .12  22 .80 1 2.5  260 1 3.5   230   1 .59   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 1 .12  23 .99 1 3.7  280 1 4.9   230   1 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 1 .12  23 .89 1 3.6  280 1 5.0   230   1 .59   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 1 .12  23 1.1  1 2.3  260 1 5.9   250   1 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 1 .11  23 1.1  1 2.3  260 1 3.3   240   -32 .60   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 1 .12  23 .84 -32 3.3  260 1 5.5   230   1 .69   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 1 .12  23 .82 1 3.7  270 1 4.6   230   -32 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 1 .13  23 .91 1 3.8  260 1 5.9   270   -32 .72   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 1 .13  23 1.1  -32 2.3  270 1 4.9   250   1 .61   18    -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 1 .11  22 .84 1 3.3  260 1 3.5   230   -32 .74   18    -
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 1 .13  23 .80 1 3.3  260 1 6.4   260   1 .69   18    -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 1 .12  23 .80 1 2.3  260 1 4.8   230   1 .72   18    -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 1 .11  23 .99 1 3.4  260 -32 6.4   230   1 .58   18    -
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 1 .10  23 1.0  1 2.3  260 1 5.9   240   1 .73   18    -
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 1 .11  23 .95 1 2.4  260 1 5.3   260   1 .63   18    -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 1 .13  23 1.2  -32 5.1  280 1 6.9   260   0 96      18    -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 1 .14  23 .82 1 3.3  260 1 4.7   230   1 .58   18    -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 1 .13  22 .90 1 2.4  260 1 5.6   260   0 .59   18    -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 1 .14  23 .96 1 3.3  260 1 6.1   230   1 .59   18    -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 1 .14  23 1.0  1 2.3  260 1 4.7   230   1 .72   18    -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 0 .098 22 .66 0 .42 44 0 .019 4.8 0 .0015 .26 -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 0 .10  22 .62 0 .42 41 0 .018 5.0 0 .0017 .29 -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 0 .11  22 .86 0 .55 43 0 .024 4.8 0 .0014 .34 -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 0 .11  22 .59 0 .57 44 0 .022 4.9 0 .0014 .32 -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 1 .12  22 .94 1 2.3  260 1 4.5   220   0 .75   18    -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 1 .11  23 .91 1 2.2  260 1 5.0   250   1 .76   18    -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 1 .11  23 .72 1 3.3  260 1 5.0   220   1 .71   18    -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 1 .11  22 .94 1 4.1  260 1 4.5   220   1 .77   18    -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 1 .10  23 1.3  1 3.9  280 1 5.8   220   1 .76   18    -
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 1 .13  22 .74 1 2.3  260 1 5.1   220   1 .67   18    -
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 1 .14  23 .82 1 2.4  260 1 5.2   260   0 .60   18    -
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 1 .14  23 .88 1 2.5  260 1 3.2   230   1 .58   18    -
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 1 .12  23 .81 1 3.4  260 1 4.7   230   1 .75   18    -
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 1 .13  23 .90 1 3.6  260 1 6.0   260   1 .77   18    -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 1 .12  23 .90 1 3.5  260 1 6.2   260   0 .60   18    -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 1 .14  22 .76 1 3.3  260 1 6.5   260   0 .58   18    -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 1 .12  24 1.1  1 2.4  260 1 7.0   260   0 .74   18    -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 1 .13  23 .90 1 3.1  260 1 5.4   230   1 .72   18    -
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 1 .11  23 1.2  1 3.3  270 1 6.1   250   1 .62   18    -
termination-crafted-lit/cstrncmp_false-no-overflow.c 0 .16  23 1.4  0 .43 44 0 .019 4.9 0 .0032 .29 -
termination-crafted-lit/gcd1_false-no-overflow.c 1 .15  23 .86 1 2.3  260 1 4.8   230   0 .72   18    -
termination-crafted-lit/joey_false-no-overflow.c 0 .091 22 .78 0 .40 41 0 .020 4.9 0 .0016 .26 -
termination-crafted-lit/min_rf_false-no-overflow.c 1 .10  23 .90 1 3.4  260 1 5.9   260   1 .71   18    -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 0 900     900 7600    - - - 0 .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 2 .11  22 .87 - - - 2 4.5   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2 .13  23 .81 - - - 2 4.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 0 900     1700 9800    - - - 0 .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 2 20     610 180    - - - 2 6.8   290  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 0 900     2500 5800    - - - 0 .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 0 900     990 10000    - - - 0 .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 2 .79  40 9.2  - - - 2 30     2400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 2 .14  23 .72 - - - 2 4.6   280  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 2 .11  23 .69 - - - 2 7.7   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 2 .13  23 .78 - - - 2 4.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 2 .11  23 .80 - - - 2 3.8   250  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 2 .12  22 .76 - - - 2 5.6   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 2 .22  25 1.9  - - - 2 5.5   290  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 0 900     2100 12000    - - - 0 .018 4.9
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 0 900     480 7000    - - - 0 .018 5.0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 0 900     510 6800    - - - 0 .020 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 2 .097 25 .88 - - - 2 4.9   280  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 0 900     1200 7000    - - - 0 .018 5.0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 0 900     1200 9700    - - - 0 .018 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2 .11  22 .75 - - - 2 5.3   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 0 900     1700 9400    - - - 0 .018 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 0 900     970 10000    - - - 0 .040 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 2 .75  39 10    - - - 2 31     2300  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 2 .10  22 .76 - - - 2 4.0   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 2 .11  22 .60 - - - 2 3.6   260  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 2 .11  22 .67 - - - 2 4.1   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 2 .11  22 .80 - - - 2 3.6   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 2 .11  23 .80 - - - 2 3.9   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 2 .094 23 .87 - - - 2 4.3   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 2 .10  22 .70 - - - 2 4.3   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 2 .11  22 .68 - - - 2 4.4   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 2 .10  22 .94 - - - 2 7.2   270  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 2 6.7   110 77    - - - 2 120     3300  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 0 900     2700 9500    - - - 0 .018 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 2 .10  22 .79 - - - 2 3.7   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 0 900     1300 9200    - - - 0 .018 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 2 .11  22 .71 - - - 2 3.5   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 2 .15  24 1.2  - - - 2 5.7   280  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 2 .089 23 .90 - - - 2 3.6   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 0 900     2400 11000    - - - 0 .018 4.9
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 2 .13  22 .69 - - - 2 3.4   260  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 2 .13  23 .74 - - - 2 4.0   270  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 0 900     1000 7100    - - - 0 .018 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 0 .12  22 .67 - - - 0 .018 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 0 .12  22 .65 - - - 0 .018 5.0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 2 .090 23 .81 - - - 2 4.5   270  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 2 .10  25 .82 - - - 2 3.8   260  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2 .11  22 .78 - - - 2 3.7   270  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 2 18     610 170    - - - 2 7.4   280  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 2 .12  22 .69 - - - 2 4.8   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 2 .12  22 .78 - - - 2 5.0   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 2 .11  22 .94 - - - 2 3.7   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 2 .10  22 .76 - - - 2 3.5   260  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 2 .10  23 .78 - - - 2 6.2   260  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 2 .13  23 .75 - - - 2 4.3   280  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 2 .12  23 .82 - - - 2 6.8   270  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 2 .11  22 .88 - - - 2 5.4   260  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 2 3.6   94 42    - - - 2 350     5100  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 0 .16  24 1.6  - - - 0 .017 4.9
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 0 .16  24 1.3  - - - 0 .020 4.9
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 0 .17  23 1.4  - - - 0 .044 4.9
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 0 .17  24 1.6  - - - 0 .019 4.9
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 0 .19  24 1.2  - - - 0 .018 4.9
termination-crafted-lit/genady_true-termination_true-no-overflow.c 2 .98  30 11    - - - 2 6.3   400  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 0 .20  24 1.4  - - - 0 .017 4.8
termination-numeric/Addition01_false-no-overflow.c 0 .099 22 .71 0 .53 43 0 .023 4.8 0 .0010 .26 -
termination-numeric/Avg_true_false-no-overflow.c 0 .12  22 .69 0 .41 44 0 .019 4.8 0 .0014 .34 -
termination-numeric/Binomial_true-termination_false-no-overflow.c 0 .10  22 .83 0 .51 43 0 .019 4.8 0 .0016 .26 -
termination-numeric/Et1_true_false-no-overflow.c 0 .12  22 .66 0 .54 43 0 .019 4.9 0 .0011 .31 -
termination-numeric/Et2_true_false-no-overflow.c 0 .099 22 .67 0 .40 45 0 .019 4.9 0 .0016 .28 -
termination-numeric/Et3_true_false-no-overflow.c 0 .12  22 .60 0 .54 43 0 .019 4.8 0 .0013 .29 -
termination-numeric/Et4_true_false-no-overflow.c 0 .12  22 .61 0 .40 41 0 .020 4.9 0 .0013 .31 -
termination-numeric/MultCommutative_false-no-overflow.c 0 .11  22 .77 0 .41 41 0 .020 5.0 0 .0014 .26 -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 0 .10  22 .69 0 .39 43 0 .022 4.9 0 .0015 .34 -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 0 .10  22 .67 - - - 0 .018 4.8
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 0 .097 22 .65 - - - 0 .018 4.9
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 0 .10  22 .80 - - - 0 .018 4.9
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 0 .098 22 .74 - - - 0 .018 4.9
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 0 .093 22 .68 - - - 0 .018 4.9
termination-numeric/Parts_true-termination_true-no-overflow.c 0 .12  22 .72 - - - 0 .017 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c 0 .12  22 .61 - - - 0 .018 5.0
termination-numeric/gcd01_true-termination_true-no-overflow.c 0 .098 22 .85 - - - 0 .018 4.8
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 2 .55  39 6.7  - - - 2 56     970  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 0 .099 22 .76 - - - 0 .018 4.9
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 0 .10  22 .71 - - - 0 .018 4.8
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 0 .12  22 .70 - - - 0 .018 4.8
termination-numeric/twisted_true-termination_true-no-overflow.c 0 900     24 9800    - - - 0 .018 4.9
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
total 280 274 25000   46000 270000 158 -35 520 37000 158 64 730 38000 158 -604 190 2400 122 142 1900 37000
    correct results 202 273 87   6400 820 125 125 400 34000 128 128 640 31000 100 100 69 1800 71 142 910 32000
        correct true 71 142 71   3400 700 0 0 0 71 142 910 32000
        correct false 131 131 17   3000 120 125 125 400 34000 128 128 640 31000 100 100 69 1800 0
    correct-unconfimed results 1 1 6.3 280 63 0 0 0 0
        correct-unconfirmed true 1 1 6.3 280 63 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 5 -160 17 1300 2 -64 11 440 22 -704 15 400 0
        incorrect true 0 5 -160 17 1300 2 -64 11 440 22 -704 15 400 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 274 -35 64 -604 142
Run set 2ls.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.NoOverflows-BitVectors