Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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*
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: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-02 06:23:16 CET 2017-12-02 08:10:39 CET 2017-12-02 08:34:53 CET 2017-12-02 08:39:22 CET 2017-12-02 08:15:43 CET
Run set esbmc-incr.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0623.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/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0623.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0623.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 false(no-overflow) 1 wit inspect .12  28 .72 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 6.0   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect .082 28 .93 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.9   250   true -32 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect .082 28 .98 false(no-overflow) 1 wit inspect 5.2  260 false(no-overflow) 1 wit inspect 5.6   240   true -32 wit inspect .71   19    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect .097 28 .70 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect .12  28 .81 false(no-overflow) 1 wit inspect 4.9  270 false(no-overflow) 1 wit inspect 5.0   220   true -32 wit inspect .71   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .092 28 1.1  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.7   250   false(no-overflow) 1 wit inspect .83   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .11  28 .77 false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 6.2   240   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .11  28 .77 false(no-overflow) 1 wit inspect 4.8  270 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .71   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .083 28 .88 false(no-overflow) 1 wit inspect 4.9  260 false(no-overflow) 1 wit inspect 5.6   220   false(no-overflow) 1 wit inspect .82   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect .080 28 1.0  false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 6.3   240   true -32 wit inspect .67   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect .072 26 .92 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect .088 27 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   280  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect .072 26 .96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect .079 26 .90 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect .073 26 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 2.1  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect .36  28 2.9  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.4   250   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.6  timeout 0 wit inspect 91    1200 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.9  false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.8  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.0  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.7   230   false(no-overflow) 1 wit inspect .79   19    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.1  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.8  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.5   270   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900     390 10000    error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.4  false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.4   220   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 1.9  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.5   260   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect .32  28 2.6  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .32  28 3.1  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.3   260   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.7  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.1  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .32  28 2.4  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 6.4   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.7  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 1.6  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.3  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.9   240   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.5  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.6   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.4  false(no-overflow) 1 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 5.7   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.1  false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.9   220   true -32 wit inspect .65   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.2  timeout 0 wit inspect 91    950 true -32 wit inspect 8.0   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.3  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .85   18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.8  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.7   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900     400 12000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.1  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.6  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.2  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.3  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.9  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.0   260   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.2  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 6.3   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.7  false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 5.5   250   error (2) 0 wit inspect .79   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.6  false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 6.2   240   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.2  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.1   220   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 2.5  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 2.0  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.0  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.9  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.2  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 6.5   240   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.6  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.8   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.5  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.0   260   false(no-overflow) 1 wit inspect 5.8    18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .55  28 4.4  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 8.5   270   false(no-overflow) 1 wit inspect .84   18    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.3  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.5  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900     890 11000    error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .087 26 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1600 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout 0 wit inspect 900     1500 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     130 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12  26 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1300 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect .056 15 .25 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     440 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     400 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     760 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     630 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 750     15000 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 0 wit inspect 900     5900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     11000 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     150 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     6400 7300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1000 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     12000 6500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     12000 6200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     4900 6300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     4900 6800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     4800 5200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     6100 6000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 890     15000 7700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 0 wit inspect 900     2100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     170 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     380 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     400 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     220 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 0 wit inspect 900     720 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     410 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     740 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .069 26 .84 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 290     15000 4400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .61  26 8.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     900 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.3  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.1   240   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 3.0  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.3   260   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.8  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.6   260   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.9  false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 1.8  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.6   260   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.2  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.7   240   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.8  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 4.9   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900     890 12000    error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.4  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 6.4   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.4  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.2   270   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900     1100 11000    error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 900     120 12000    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.3  false(no-overflow) 1 wit inspect 4.5  270 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.5  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.3   270   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.4  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 2.2  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.8   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.2  false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 6.6   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect .42  29 4.2  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.6  false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 6.4   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.7  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.5   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .30  28 2.6  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect .37  28 4.0  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.9   260   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect .31  28 3.4  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.8   240   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.2  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect .11  28 1.3  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .69   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.5  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.9   250   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect .11  28 1.5  false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.2  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 4.8   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.5  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 6.2   260   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.7  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.8  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 2.1  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.6  false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.8   220   false(no-overflow) 1 wit inspect .78   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 2.1  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 5.8   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.5  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.5  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 2.1  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 6.0   220   false(no-overflow) 1 wit inspect .64   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.5  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.2   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 3.2  false(no-overflow) 1 wit inspect 2.5  260 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.4  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.7  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.5  false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 5.9   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.8  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.4   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.5  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.6   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.6  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.2   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.9  false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .62   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.7  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.7  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.8   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.9  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.1   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.1  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 1.6  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.1  false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 1.9  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.1   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 1.9  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.8   260   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 2.2  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.0  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.4  false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 5.6   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.2  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect .31  28 2.8  true -32 wit inspect 3.8  250 false(no-overflow) 1 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.1  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 2.2  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.3   250   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 2.7  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 2.3  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.0  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.3   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.9  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.5  false(no-overflow) 1 wit inspect 4.7  280 true -32 wit inspect 5.9   230   timeout 0 wit inspect 96      19    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.9  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.5  false(no-overflow) 1 wit inspect 2.3  260 true -32 wit inspect 5.2   220   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.6  false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 1.9  false(no-overflow) 1 wit inspect 4.5  270 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.3  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 7.9   270   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.6  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 6.2   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.6  timeout 0 wit inspect 91    650 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.6  false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.5  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.8  false(no-overflow) 1 wit inspect 3.1  250 false(no-overflow) 1 wit inspect 4.8   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.7  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.6   220   false(no-overflow) 1 wit inspect .82   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.9  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.7  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.5  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.8  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 6.6   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.9  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.2   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.5  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 2.6  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.5  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 6.0   260   error (2) 0 wit inspect .66   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.4  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.2   250   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.1  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 6.0   230   error (2) 0 wit inspect .80   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.3  false(no-overflow) 1 wit inspect 3.8  250 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.3  false(no-overflow) 1 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 6.3   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect .34  29 2.8  true -32 wit inspect 5.8  310 false(no-overflow) 1 wit inspect 6.5   280   true -32 wit inspect .74   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.2  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.9   260   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.3  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 6.1   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.9  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.6   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     620 9300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 0 wit inspect 900     600 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .62  26 7.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 0 wit inspect 900     870 9800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900     130 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect .18  26 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 48     2300  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     240 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     250 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     280 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 0 wit inspect 900     120 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 0 wit inspect 900     110 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     110 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     340 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     350 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 900     670 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .63  26 7.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900     130 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect .16  26 2.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 48     2500  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout 0 wit inspect 900     220 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     520 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     460 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 0 wit inspect 900     680 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 0 wit inspect 900     140 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     180 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 0 wit inspect 900     160 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .41  26 4.8  - wit inspect - wit inspect - wit inspect true 2 wit inspect 170     3600  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     230 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     990 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     490 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 0 wit inspect 900     950 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900     800 9500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     200 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     250 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 0 wit inspect 590     15000 7100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 0 wit inspect 510     15000 5600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     180 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 0 wit inspect 900     560 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .20  26 2.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     320 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     740 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     350 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 0 wit inspect 900     300 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 wit inspect 900     3600 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     670 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     420 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout 0 wit inspect 900     400 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 5.7   32 72    - wit inspect - wit inspect - wit inspect true 2 wit inspect 370     5200  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 0 wit inspect 900     5700 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1400 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2900 9000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 5.0
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1800 8300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .062 5.0
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 8100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1800 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 5.0
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.6  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 6.3   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.8  false(no-overflow) 1 wit inspect 5.7  280 false(no-overflow) 1 wit inspect 5.9   260   error (2) 0 wit inspect .79   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 8.0   80 110    timeout 0 wit inspect 91    910 true -32 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 2.0  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 8.1   270   true -32 wit inspect .77   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.2  false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 5.9   240   true -32 wit inspect .70   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.9  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 6.1   250   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect .39  28 3.6  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 8.4   260   true -32 wit inspect .72   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect .30  28 2.8  timeout 0 wit inspect 91    520 true -32 wit inspect 8.9   310   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 16     51 180    timeout 0 wit inspect 92    790 out of memory 0 wit inspect 80     7000   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 0 wit inspect 460     15000 4900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     8800 6500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 1 wit inspect 84     160 1000    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     490  
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2900 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 8600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .22  26 2.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 59     1000  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect 1.9   28 24    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
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 188 96000   250000 1100000 158 80 1100   44000 158 -47 930 43000 158 -451 200 2800 122 34 2700 21000
    correct results 169 186 64   4800 700 144 144 540   38000 145 145 810 34000 125 125 89 2300 17 34 750 18000
        correct true 17 34 9.3 450 120 0 0 0 17 34 750 18000
        correct false 152 152 55   4300 580 144 144 540   38000 145 145 810 34000 125 125 89 2300 0
    correct-unconfimed results 2 2 86   190 1000 0 0 0 0
        correct-unconfirmed true 2 2 86   190 1000 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 2 -64 9.6 570 6 -192 39 1500 18 -576 12 330 0
        incorrect true 0 2 -64 9.6 570 6 -192 39 1500 18 -576 12 330 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 188 80 -47 -451 34
Run set esbmc-incr.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.NoOverflows-BitVectors