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]
Date of execution 2017-12-02 18:23:42 CET 2017-12-02 20:05:51 CET 2017-12-02 20:31:31 CET 2017-12-02 20:34:26 CET 2017-12-02 20:11:47 CET
Run set esbmc-kind.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1823.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-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1823.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1823.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 .11  28 .83 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.7   220   true -32 wit inspect .68   19    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect .092 28 .97 false(no-overflow) 1 wit inspect 2.8  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .68   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect .079 28 1.1  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.0   240   true -32 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect .11  28 .82 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.1   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect .081 28 1.0  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.3   220   true -32 wit inspect .69   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .083 28 .90 false(no-overflow) 1 wit inspect 4.8  260 false(no-overflow) 1 wit inspect 5.3   240   false(no-overflow) 1 wit inspect .68   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .11  28 .76 false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 5.4   240   false(no-overflow) 1 wit inspect .72   18    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .10  28 .97 false(no-overflow) 1 wit inspect 4.8  260 false(no-overflow) 1 wit inspect 5.3   240   false(no-overflow) 1 wit inspect .80   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .12  28 .58 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 4.4   240   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect .082 28 .83 false(no-overflow) 1 wit inspect 4.1  270 false(no-overflow) 1 wit inspect 5.5   240   true -32 wit inspect .81   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect .081 26 .77 - 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 .089 27 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   250  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect .080 27 .76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect .088 26 .72 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect .075 26 .84 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.6  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 5.2   220   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect .41  28 4.0  false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.7  timeout 0 wit inspect 91    990 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.4  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 2.2  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.1   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 3.2  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect .35  28 3.3  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .65   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.5  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 6.6   260   true -32 wit inspect .78   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900     390 11000    error (invalid witness file) 0 wit inspect .40 45 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.3  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 4.9   240   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/Copenhagen_disj_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 7.1   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect .42  28 3.4  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.2   250   false(no-overflow) 1 wit inspect .68   19    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .37  28 4.0  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.8  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   220   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect .41  28 3.9  false(no-overflow) 1 wit inspect 2.3  270 false(no-overflow) 1 wit inspect 5.7   260   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 3.3  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_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 5.5   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.4  false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 5.8   260   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.9  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.2  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.8   260   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.1  false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 4.5   210   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 1.7  false(no-overflow) 1 wit inspect 4.8  290 false(no-overflow) 1 wit inspect 5.6   250   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.2  timeout 0 wit inspect 92    920 true -32 wit inspect 7.7   260   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.2  false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.1  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   220   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900     390 12000    error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.5  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.6  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.7  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.3  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.2   220   true -32 wit inspect .66   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.1  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.2   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.8  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/RecursiveMultiplication_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 5.7   260   error (2) 0 wit inspect .80   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect .11  28 1.5  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.8   240   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 2.2  false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 4.5   210   error (2) 0 wit inspect .67   18    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.9  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.9  false(no-overflow) 1 wit inspect 4.9  260 false(no-overflow) 1 wit inspect 5.7   240   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.9  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.3   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 .21  28 1.9  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect .32  28 2.5  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.4  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .28  28 1.8  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 7.2   260   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .57  28 5.7  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 8.0   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .34  28 3.3  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .33  28 2.9  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900     880 11000    error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .074 26 .79 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12  26 .57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 42     770  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 2 wit inspect .072 26 .78 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   250  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .089 26 .78 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .10  26 .85 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .089 26 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   270  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .096 26 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1300 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect .033 15 .31 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     450 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     400 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .075 26 .77 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   270  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .082 26 .86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c true 1 wit inspect .11  26 .96 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
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 .020 4.9
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .082 26 .66 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   210  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     150 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     9000 9500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 720     15000 7600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 670     15000 7800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     4800 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 770     15000 6700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 680     15000 6600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     12000 7200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     12000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect .079 26 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .072 26 .89 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   260  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .10  26 .62 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .076 26 .86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   250  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12  26 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5   260  
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 .020 5.0
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12  26 .86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .11  26 .72 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   250  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .093 26 .73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .10  26 .68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .11  26 .66 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     890 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect .41  29 4.6  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect .56  30 6.8  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 5.1   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 3.2  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.9   250   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 .35  28 2.8  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 6.9   260   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect .38  28 3.7  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 6.7   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect .38  28 2.9  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.6   250   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect .36  28 3.8  false(no-overflow) 1 wit inspect 4.8  260 false(no-overflow) 1 wit inspect 5.3   260   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900     890 11000    error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.8 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 .36  28 3.8  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 6.0   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.1  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.6   250   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900     1000 9700    error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 900     120 9600    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.5  false(no-overflow) 1 wit inspect 4.1  270 false(no-overflow) 1 wit inspect 6.0   240   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.3  false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 6.2   260   true -32 wit inspect .78   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect .35  28 3.7  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.8   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect .45  28 3.7  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.5  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect .69  32 6.7  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect .31  28 2.9  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 3.4  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 6.2   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .33  28 2.9  false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.9   260   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect .47  29 4.2  false(no-overflow) 1 wit inspect 4.3  270 true -32 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect .42  28 4.3  false(no-overflow) 1 wit inspect 2.7  280 true -32 wit inspect 5.4   250   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.4  false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect .13  28 1.2  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.9   230   true -32 wit inspect .79   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.3  false(no-overflow) 1 wit inspect 2.3  260 true -32 wit inspect 5.8   210   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.1  false(no-overflow) 1 wit inspect 4.3  270 true -32 wit inspect 4.6   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.2  false(no-overflow) 1 wit inspect 4.0  270 true -32 wit inspect 5.5   210   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 1.9  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 3.1  false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 6.7   270   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect .30  28 2.8  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.9  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.3  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .75   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.5  false(no-overflow) 1 wit inspect 3.8  270 true -32 wit inspect 5.5   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.6  false(no-overflow) 1 wit inspect 3.6  290 false(no-overflow) 1 wit inspect 4.9   240   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 2.2  false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 3.1  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 7.3   260   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.1  false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 6.3   260   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect .37  29 4.5  false(no-overflow) 1 wit inspect 4.7  260 true -32 wit inspect 5.3   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect .31  28 2.7  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.5  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 4.3   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.0  false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.1   240   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.9  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.4   220   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 1.7  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.6   270   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 2.1  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.8   230   error (2) 0 wit inspect .67   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.6  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.4   240   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 3.0  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.8   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 1.7  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.6  false(no-overflow) 1 wit inspect 4.1  260 true -32 wit inspect 5.2   230   true -32 wit inspect .74   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect .34  28 3.2  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect .37  28 4.9  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect .35  28 3.0  false(no-overflow) 1 wit inspect 2.9  290 false(no-overflow) 1 wit inspect 5.1   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 .27  28 2.4  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.1  false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.8   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.2  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 2.6  false(no-overflow) 1 wit inspect 4.2  260 true -32 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.0  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 5.7   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.4  false(no-overflow) 1 wit inspect 3.8  260 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect .32  28 3.1  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 4.9   240   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 2.5  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 6.1   240   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 .41  28 3.3  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .30  28 3.1  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .49  28 4.5  false(no-overflow) 1 wit inspect 4.7  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.6  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.2   240   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_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 5.1   250   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  28 1.7  false(no-overflow) 1 wit inspect 4.5  270 true -32 wit inspect 4.5   230   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.5  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 1.8  false(no-overflow) 1 wit inspect 4.2  260 true -32 wit inspect 5.2   210   error (2) 0 wit inspect .60   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .18  28 2.1  false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 6.1   230   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.3  false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 3.4   230   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .12  28 1.7  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 7.6   270   false(no-overflow) 1 wit inspect .70   19    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.2  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .82   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.5  timeout 0 wit inspect 91    780 false(no-overflow) 1 wit inspect 6.1   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.8  false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect .19  28 2.4  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.8   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.9  false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.7   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .23  28 3.1  false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 2.9  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.8  false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 5.5   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 1.7  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .21  28 1.7  false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.2   220   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .25  28 2.2  false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .83   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .43  28 3.6  false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 5.1   250   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.5  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .30  28 2.9  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 6.1   250   error (2) 0 wit inspect .72   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .34  28 3.0  false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 5.1   250   error (2) 0 wit inspect .64   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .34  28 2.9  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.5   250   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .32  29 3.0  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .15  28 1.4  false(no-overflow) 1 wit inspect 4.5  270 false(no-overflow) 1 wit inspect 6.2   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect .37  29 4.5  true -32 wit inspect 5.5  320 false(no-overflow) 1 wit inspect 6.9   270   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect .26  28 3.7  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   250   error (2) 0 wit inspect .71   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect .14  28 1.3  false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 5.5   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect .29  28 3.5  false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     590 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect .12  26 .65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .074 26 .91 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect .23  27 2.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-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 .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect .25  26 3.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 49     2400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect .077 26 .86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect .12  26 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect .14  26 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect .12  26 .78 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect .091 26 .71 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 0 wit inspect 900     120 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 0 wit inspect 900     99 10000    - 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     99 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .16  26 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   270  
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 .025 4.8
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 900     670 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900     120 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect .28  26 3.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 45     2300  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect .077 26 .80 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   200  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   260  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect .11  26 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   250  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect .098 26 .90 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect .092 26 .96 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect .18  26 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 wit inspect .11  26 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6   270  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .46  26 6.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 160     3600  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     240 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect .079 26 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     990 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect .087 26 .93 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   250  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 0 wit inspect 900     940 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect .078 26 .88 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   250  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900     760 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect .10  26 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .11  26 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   280  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     230 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 0 wit inspect 690     15000 7100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 0 wit inspect 890     15000 7600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect .29  26 3.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   250  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .12  26 .70 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .59 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   250  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .075 26 .86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .12  26 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect .083 26 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect .096 26 .98 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect .085 26 .75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .11  26 .65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   280  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect .14  26 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   270  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 2 wit inspect .10  26 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 6.1   33 77    - wit inspect - wit inspect - wit inspect true 2 wit inspect 390     5300  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect .19  27 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect .14  27 1.9  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect .15  27 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect .16  27 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2   260  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect .16  27 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 0 wit inspect 900     11000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect .12  27 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   260  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect .20  28 1.5  false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 6.9   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect .17  28 1.8  false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 5.8   250   error (2) 0 wit inspect .64   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 5.5   64 71    timeout 0 wit inspect 92    870 true -32 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect .24  28 2.0  false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 7.2   270   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect .27  28 2.7  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.8   250   true -32 wit inspect .60   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect .22  28 2.1  false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.7   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect .44  28 3.5  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 6.9   260   true -32 wit inspect .68   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect .43  29 4.7  timeout 0 wit inspect 91    520 true -32 wit inspect 8.3   300   false(no-overflow) 1 wit inspect .83   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 23     57 310    timeout 0 wit inspect 91    800 out of memory 0 wit inspect 79     7000   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 0 wit inspect 620     15000 6600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     11000 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 0 wit inspect 900     900 9800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 1 wit inspect 110     170 1200    - 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     3700 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1600 8300    - 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.8  - wit inspect - wit inspect - wit inspect true 2 wit inspect 62     1200  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect 2.0   27 27    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2500  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .050 4.9
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1000 9000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 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 297 47000 210000 550000 158 113 1100   44000 158 -509 910 43000 158 -386 200 2800 122 142 4000 40000
    correct results 223 294 81 6200 910 145 145 540   38000 131 131 720 31000 126 126 85 2300 71 142 1200 32000
        correct true 71 142 15 1900 160 0 0 0 71 142 1200 32000
        correct false 152 152 66 4300 750 145 145 540   38000 131 131 720 31000 126 126 85 2300 0
    correct-unconfimed results 3 3 110 220 1300 0 0 0 0
        correct-unconfirmed true 3 3 110 220 1300 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 1 -32 5.5 320 20 -640 110 4600 16 -512 11 290 0
        incorrect true 0 1 -32 5.5 320 20 -640 110 4600 16 -512 11 290 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 297 113 -509 -386 142
Run set esbmc-kind.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.NoOverflows-BitVectors