Tool 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* [apollon004; apollon025; apollon077; apollon078; apollon080] [apollon077; apollon078; apollon157] [apollon038; apollon077; apollon078; apollon164] [apollon025; apollon052; apollon077; apollon078]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 10:49:29 CET 2017-12-01 12:01:34 CET 2017-12-01 12:20:33 CET 2017-12-01 12:23:03 CET 2017-12-01 12:03:46 CET
Run set cpa-seq.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1049.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/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2017-12-01_1049.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2017-12-01_1049.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 3.4 300 29 false(no-overflow) 1 wit inspect 2.6  260 false(no-overflow) 1 wit inspect 3.1   230   true -32 wit inspect .62   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.5 280 32 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .73   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.6 280 32 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.1   240   true -32 wit inspect .62   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.4 280 27 false(no-overflow) 1 wit inspect 2.6  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .61   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.4 280 34 false(no-overflow) 1 wit inspect 4.8  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .63   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.5 280 31 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .79   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.4 280 29 false(no-overflow) 1 wit inspect 5.1  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .81   19    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.7 280 32 true -32 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.3   250   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.4 270 31 true -32 wit inspect 4.8  290 false(no-overflow) 1 wit inspect 4.8   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect 3.5 280 31 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 3.6   250   true -32 wit inspect .61   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect 3.1 270 30 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5   250  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect 3.1 280 28 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   220  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect 3.0 280 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   220  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 2.3  270 false(no-overflow) 1 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c timeout 0 wit inspect 900   3800 11000 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .82   18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .84   18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 27 false(no-overflow) 1 wit inspect 2.9  270 false(no-overflow) 1 wit inspect 3.8   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 290 25 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.4   250   true -32 wit inspect .82   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 5.2   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900   2600 13000 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0019 .30 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 280 28 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 24 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.7   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 24 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.3   250   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.1   260   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.0   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.5   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 270 24 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 3.5   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.9   240   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.2   250   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.0   270   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 24 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.3   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect 3.0 280 27 false(no-overflow) 1 wit inspect 2.5  280 false(no-overflow) 1 wit inspect 3.7   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 190   1300 1500 false(no-overflow) 1 wit inspect 22    980 false(no-overflow) 1 wit inspect 4.4   260   false(no-overflow) 1 wit inspect .65   19    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 23 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 21 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900   2200 12000 error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .042 4.9 error (invalid witness file) 0 wit inspect .0035 .33 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.6   240   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.1   220   false(no-overflow) 1 wit inspect 1.3    18    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 26 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.4   250   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 26 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.7   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.4   260   true -32 wit inspect .75   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 1 wit inspect 3.5 300 30 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 4.3   260   error (2) 0 wit inspect .59   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 21 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 260 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.8   220   timeout 0 wit inspect 96      19    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 4.0   230   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 23 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .58   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 260 23 false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 3.4   220   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.2   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.4   270   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 3.1 280 28 false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 4.7   270   false(no-overflow) 1 wit inspect .84   19    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 28 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 3.9   240   true -32 wit inspect .64   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.3   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900   13000 10000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 31     830  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2   270  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   6200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 21 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   220  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   2600 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   260  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   260  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 2.9 290 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c true 1 wit inspect 2.7 270 25 - 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   6300 9900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 2.5 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   200  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   270  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     500  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 3.9 290 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0   460  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.0 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     640  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 5.0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.3 280 30 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     440  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1400 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5100 9900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 5.0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect 2.6 270 22 - 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 2.7 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3   270  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   280  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   260  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 2.6 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   270  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 260 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   250  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 290 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.7 270 22 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   13000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.6   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 26 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.7   250   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   260   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 21 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.1   280   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 26 false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 3.5   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 26 false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 5.2   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900   13000 11000 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 2.5  260 false(no-overflow) 1 wit inspect 4.4   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.2   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900   6200 10000 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 910   620 13000 error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0035 .28 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 280 27 false(no-overflow) 1 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 3.3   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 2.7 280 24 false(no-overflow) 1 wit inspect 2.8  260 false(no-overflow) 1 wit inspect 3.4   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.8   260   true -32 wit inspect .76   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.6   270   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.9   270   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 2.7 270 23 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.2   240   false(no-overflow) 1 wit inspect .82   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 22 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.9   270   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   240   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.0   240   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 24 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .61   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.7  260 false(no-overflow) 1 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 280 22 false(no-overflow) 1 wit inspect 2.3  280 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 290 28 false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .75   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 280 26 false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 4.1   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 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.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.7   270   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 2.6 280 23 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.2   220   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 290 29 false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 3.1   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.2   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 260 22 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.3   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 21 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.7   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 25 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.4   240   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.5   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.0   240   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 22 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 260 23 false(no-overflow) 1 wit inspect 2.9  260 false(no-overflow) 1 wit inspect 4.0   250   false(no-overflow) 1 wit inspect .83   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 260 25 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.2   220   error (2) 0 wit inspect .75   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 3.4   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 260 22 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.0   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 23 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.9   220   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.3   240   error (2) 0 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 24 false(no-overflow) 1 wit inspect 2.6  260 false(no-overflow) 1 wit inspect 3.6   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.9   230   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 2.7 270 25 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.7   250   false(no-overflow) 1 wit inspect .84   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 260 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 310 29 false(no-overflow) 1 wit inspect 2.7  270 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.3   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.6   230   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 22 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 3.4   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 2.7 260 25 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.6   260   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 21 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 4.0   230   false(no-overflow) 1 wit inspect 4.2    18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 26 false(no-overflow) 1 wit inspect 2.5  260 false(no-overflow) 1 wit inspect 5.5   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 23 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.9   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 24 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.4   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 290 26 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 4.4   260   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .60   19    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 4.0   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 26 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 280 24 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 3.0 280 26 false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 4.8   280   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 3.2 280 27 false(no-overflow) 1 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 3.4   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c timeout 0 wit inspect 900   2500 8200 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 3.1 310 28 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 3.4   250   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 260 23 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.2   240   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 2.6 270 26 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.3   270   true -32 wit inspect .71   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 26 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 3.8   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 22 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 290 24 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 26 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 26 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 27 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 3.5   240   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 270 25 false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 3.5   220   false(no-overflow) 1 wit inspect .83   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 2.9 270 25 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 3.3   250   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 24 false(no-overflow) 1 wit inspect 4.5  260 false(no-overflow) 1 wit inspect 3.4   260   error (2) 0 wit inspect .77   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 25 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.1   240   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.9   250   error (2) 0 wit inspect .59   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .82   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 280 24 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 3.7   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect 3.7 330 34 false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 5.4   270   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 20 false(no-overflow) 1 wit inspect 2.3  260 false(no-overflow) 1 wit inspect 4.9   250   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 22 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.5   270   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect 2.8 270 26 false(no-overflow) 1 wit inspect 2.6  270 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c out of memory 0 wit inspect 850   15000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 2.7 260 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 100   1100 860 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6200 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   540 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 59   480 780 - wit inspect - wit inspect - wit inspect true 2 wit inspect 31     2400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect 2.9 280 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 3.9 280 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 2.8 260 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   310  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     430  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     400  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   8000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c out of memory 0 wit inspect 890   15000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4000 9100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 910   610 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 59   460 710 - wit inspect - wit inspect - wit inspect true 2 wit inspect 51     2000  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 2.9 300 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   250  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 3.0 290 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   250  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 2.8 290 27 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   290  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 wit inspect 2.6 280 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   290  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c timeout 0 wit inspect 900   7100 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   560 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 2.6 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   270  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4000 9700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   250  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   280  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900   6800 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect 2.5 270 20 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   260  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   510 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     370  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 10000 - 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 2.6 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   270  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8   260  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 2.6 260 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7   250  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 110   1000 790 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 2.5 270 21 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 2.6 270 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect 2.6 260 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8   250  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4900 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 4.1 290 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   260  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   270  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 2 wit inspect 2.6 270 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout 0 wit inspect 900   8100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect 3.4 310 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   270  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect 3.4 310 29 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect 2.8 280 25 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   270  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect 3.3 310 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   260  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect 3.3 310 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted-lit/genady_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect 2.8 290 23 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   260  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect 3.1 310 28 false(no-overflow) 1 wit inspect 2.5  260 false(no-overflow) 1 wit inspect 3.8   260   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 24 false(no-overflow) 1 wit inspect 2.8  260 false(no-overflow) 1 wit inspect 5.4   260   error (2) 0 wit inspect .61   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900   2000 8300 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 21 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 5.5   250   error (2) 0 wit inspect .63   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 260 27 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.7   250   error (2) 0 wit inspect .61   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.6 270 21 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.1   240   error (2) 0 wit inspect .74   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect 2.7 270 23 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.6   240   error (2) 0 wit inspect .60   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c timeout 0 wit inspect 900   1600 11000 error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 0 wit inspect 900   1600 7500 error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6500 10000 - 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   4300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c true 1 wit inspect 5.3 310 57 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect 3.0 280 24 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   260  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1900 9300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2900 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 0 wit inspect 900   740 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 wit inspect 3.5 310 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   280  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 15   460 160 - wit inspect - wit inspect - wit inspect true 2 wit inspect 46     1100  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4400 9800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5700 11000 - 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   7800 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
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 313 45000   320000 540000 158 81 510   40000 158 147 580 35000 158 -822 200 2700 122 164 2500 38000
    correct results 229 311 1200   66000 10000 145 145 490   39000 147 147 580 35000 106 106 75 1900 82 164 600 28000
        correct true 82 164 560   25000 5300 0 0 0 82 164 600 28000
        correct false 147 147 600   41000 5100 145 145 490   39000 147 147 580 35000 106 106 75 1900 0
    correct-unconfimed results 2 2 8.0 580 82 0 0 0 0
        correct-unconfirmed true 2 2 8.0 580 82 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 2 -64 8.7 550 0 29 -928 19 530 0
        incorrect true 0 2 -64 8.7 550 0 29 -928 19 530 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 313 81 147 -822 164
Run set cpa-seq.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.NoOverflows-BitVectors