Tool ULTIMATE Kojak 0.1.23-3204b741 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-03 11:17:40 CET 2017-12-03 11:52:51 CET 2017-12-03 12:03:01 CET 2017-12-03 12:03:17 CET 2017-12-03 11:54:19 CET
Run set ukojak.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_1117.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/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_1117.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 4.3 240 36 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .61   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.4 260 38 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.4   250   true -32 wit inspect .62   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.4 250 35 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.8   240   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.2 250 37 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.1   210   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 240 35 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.5 270 35 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .67   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.2 250 38 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.0   220   false(no-overflow) 1 wit inspect .67   19    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.4 250 34 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.6   250   false(no-overflow) 1 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.2 240 37 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.6 240 42 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .67   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect 4.0 240 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect 4.4 260 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   320  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect 3.9 240 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect 4.0 230 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect 4.0 240 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.3   320   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   240   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 38 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 35 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.4   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 260 38 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 290 40 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900   5200 12000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect 3.1    18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 33 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.5   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 41 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect 6.9 370 51 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 39 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .65   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 38 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 38 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 350   4900 4900 false(no-overflow) 1 wit inspect 22    950 false(no-overflow) 1 wit inspect 4.8   260   false(no-overflow) 1 wit inspect .61   19    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 34 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.2   220   false(no-overflow) 1 wit inspect 3.9    18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 35 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.9   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900   5200 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .050 4.8 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 36 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.4   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 4.1 250 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.1   240   true -32 wit inspect .64   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 39 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 38 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .62   19    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 32 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 4.6   230   error (2) 0 wit inspect .64   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.3   250   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 38 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 34 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 41 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 33 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 41 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.6   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 12   540 120 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.5   270   true -32 wit inspect .64   19    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 36 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.2   250   error (2) 0 wit inspect .61   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 39 false(no-overflow) 1 wit inspect 3.0  250 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900   7000 13000 error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.6 260 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5200 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 2 wit inspect 4.5 260 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   260  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.0 470 63 - 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 7.0 460 58 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 6.2 420 59 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.3 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   270  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5700 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.0 240 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.9 270 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.1 270 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.8 420 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 5.8 310 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   270  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5300 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 0 wit inspect 900   6200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 3.9 230 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   220  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5300 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.6 400 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3   270  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 18   670 170 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     500  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1200 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1200 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1500 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1600 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900   2000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect 4.0 240 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 6.4 380 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.3 390 55 - 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 6.1 380 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.0 340 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 5.8 320 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.5 380 62 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.1 260 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   250  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.8 240 31 - 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 3.8 230 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   220  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 310 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   7100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 260 36 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 260 42 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 42 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect 6.2 380 59 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 5.4   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 250 44 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   240   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect 5.9 340 51 timeout 0 wit inspect 91    1200 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900   7000 10000 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect 5.9 320 52 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 37 false(no-overflow) 1 wit inspect 2.9  250 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900   6000 12000 error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 900   6700 12000 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.1   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 36 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect 5.5 310 48 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 270 39 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 250 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.9   270   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 250 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.7   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.4   260   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 260 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 260 34 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .60   19    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 260 42 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .65   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 34 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 35 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 39 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.9   220   true -32 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 40 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .59   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 41 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 35 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 35 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 34 false(no-overflow) 1 wit inspect 4.1  270 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .58   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 34 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 290 42 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.7   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 5.7 330 45 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .63   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.5  250 false(no-overflow) 1 wit inspect 4.8   240   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 38 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.5   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 37 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   220   false(no-overflow) 1 wit inspect 4.4    18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 33 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 39 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   240   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 260 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 3.3   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 260 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .61   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 4.9   220   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   240   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.3  250 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .62   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 260 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 5.6 300 48 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 34 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 6.5   320   true -32 wit inspect 1.3    18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.5   230   true -32 wit inspect 3.6    18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 270 42 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 9.9 480 81 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 40 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 260 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.9   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 36 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 38 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 5.7 320 46 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 6.7   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 5.5 320 43 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 36 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 31 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 340 46 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 5.4 270 43 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.0   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 6.2 350 51 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .59   19    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 340 52 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 340 44 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   240   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect 6.4 350 54 false(no-overflow) 1 wit inspect 3.7  310 false(no-overflow) 1 wit inspect 7.8   330   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 37 false(no-overflow) 1 wit inspect 3.1  250 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 300 48 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 6.8 470 61 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 5.6 310 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   7100 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 7.6 490 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect 120   2300 1700 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6600 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect 7.5 470 69 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   290  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 16   700 160 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect 8.5 530 83 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 7.2 440 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 7.6 480 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 14   630 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0   310  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 2 wit inspect 13   590 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8   430  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 19   690 190 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   410  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 14   580 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   280  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6100 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 wit inspect 93   2000 1000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7   440  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 5.6 310 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   7100 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .053 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6700 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect 4.1 230 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 5.1 280 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 5.8 320 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 6.5 380 57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   250  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 8.5 470 78 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 7.5 470 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 6.8 460 57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 6.0 310 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 wit inspect 6.7 450 57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3   280  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c timeout 0 wit inspect 900   6300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 5.7 310 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 100   2300 1300 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1   430  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 5.1 280 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   250  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 2 wit inspect 13   570 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 5.3 290 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect 4.7 260 39 - 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 6.2 380 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .030 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 wit inspect 9.3 520 86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6   360  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5600 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 11   520 100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 6.8 470 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.9 270 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 7.0 470 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 4.6 260 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 7.0 480 64 - 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 6.0 340 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect 4.4 260 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   270  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect 6.6 420 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   250  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 6.9 430 57 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 7.8 470 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 2 wit inspect 4.8 260 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   270  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect 5.4 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect 5.7 310 54 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   270  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect 5.5 300 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   270  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect 5.5 310 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect 5.6 300 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 36   1000 410 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0   420  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect 5.7 320 48 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   270  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 260 37 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .62   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 260 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.1   250   error (2) 0 wit inspect .63   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900   2300 8700 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .032 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .61   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.1  250 false(no-overflow) 1 wit inspect 5.0   260   true -32 wit inspect .63   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .60   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect 11   600 120 timeout 0 wit inspect 91    510 false(no-overflow) 1 wit inspect 13     400   true -32 wit inspect .63   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 0 wit inspect 900   2100 10000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0035 .31 - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1700 11000 - 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   5000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 5.0
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1500 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect 7.6 490 65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1900 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2500 9500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 5.0
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 wit inspect 8.4 470 73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 170   4700 2200 - wit inspect - wit inspect - wit inspect true 2 wit inspect 520     980  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4600 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .038 4.8
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5700 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 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 318 44000 310000 580000 158 148 700 41000 158 150 740 36000 158 -4116 590 2800 122 168 1000 24000
    correct results 234 318 2100 87000 22000 148 148 510 39000 150 150 740 36000 12 12 15 220 84 168 1000 24000
        correct true 84 168 1100 42000 11000 0 0 0 84 168 1000 24000
        correct false 150 150 1000 45000 11000 148 148 510 39000 150 150 740 36000 12 12 15 220 0
    incorrect results 0 0 0 129 -4128 86 2400 0
        incorrect true 0 0 0 129 -4128 86 2400 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 318 148 150 -4116 168
Run set ukojak.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.NoOverflows-BitVectors