Tool ULTIMATE Taipan 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 08:43:49 CET 2017-12-03 08:58:51 CET 2017-12-03 09:15:45 CET 2017-12-03 09:17:25 CET 2017-12-03 09:00:18 CET
Run set utaipan.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-03_0843.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/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2017-12-03_0843.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2017-12-03_0843.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.1 240 34 false(no-overflow) 1 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 4.1   220   true -32 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.7 270 41 false(no-overflow) 1 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 240 34 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.7   240   true -32 wit inspect .64   19    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.3 240 37 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .60   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.0 240 35 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.3   220   true -32 wit inspect .62   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.4 270 39 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.7   250   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.0 240 35 false(no-overflow) 1 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.4 260 34 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 240 33 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.5   240   false(no-overflow) 1 wit inspect .62   19    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 250 38 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect 4.3 240 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect 4.7 280 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   250  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect 4.3 250 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect 4.2 240 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect 4.1 240 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.3   230   true -32 wit inspect .61   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.0  260 false(no-overflow) 1 wit inspect 5.3   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Ackermann_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 5.1   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Bangalore_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   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 250 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 290 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900   2400 13000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0024 .30 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 290 41 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.0   240   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   230   false(no-overflow) 1 wit inspect 4.2    18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 34 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.1   240   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 35 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 32 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 38 false(no-overflow) 1 wit inspect 3.4  250 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.4  250 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 38 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.4   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 37 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect 6.8 350 44 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 250   2200 2700 false(no-overflow) 1 wit inspect 22    950 false(no-overflow) 1 wit inspect 4.9   250   false(no-overflow) 1 wit inspect .65   19    - wit inspect
termination-crafted/NonTerminationSimple2_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.3   210   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 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.4   230   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900   2500 15000 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .0016 .31 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 290 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .64   19    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 230 36 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   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.0 250 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 280 37 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.3   270   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Pure3Phase_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 5.1   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/RecursiveMultiplication_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 5.3   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   230   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 33 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   220   timeout 0 wit inspect 96      19    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 240 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 32 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .60   19    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 38 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.2   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 35 false(no-overflow) 1 wit inspect 2.5  270 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 290 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 6.7   330   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 13   610 100 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.6   270   true -32 wit inspect .61   19    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 40 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900   5300 13000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0038 .32 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.5 260 36 - 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   1500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 2 wit inspect 4.8 280 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   320  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.8 330 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0   260  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.5 290 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 5.5 300 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.8 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 24   800 220 - wit inspect - wit inspect - wit inspect true 2 wit inspect 22     520  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.1 240 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   210  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.3 300 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.1 280 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   270  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.4 300 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 7.6 390 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   250  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.8
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.3 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   3900 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.4 310 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4   270  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.2 320 55 - 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 true 2 wit inspect 16   640 140 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     460  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 44   1100 390 - wit inspect - wit inspect - wit inspect true 2 wit inspect 20     630  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 23   670 180 - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     510  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 13   580 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 15   610 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     490  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 9.5 520 76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     480  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 14   610 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     560  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect 3.9 230 31 - 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 5.8 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   270  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.8 360 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.9 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.9 300 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 5.0 280 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.6 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.7 280 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5   260  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.0 240 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.2 240 31 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.8 290 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 1 wit inspect 7.4 350 60 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 290 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.5   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect 5.1 290 38 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .64   19    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 280 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .63   19    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect 6.3 290 47 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.7   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 290 42 timeout 0 wit inspect 91    1200 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900   5300 12000 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 40 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.1   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.7 290 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900   3000 15000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 900   3800 12000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .037 4.9 error (invalid witness file) 0 wit inspect .0043 .35 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 34 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 32 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 280 42 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 290 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.0   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 290 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   260   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 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 32 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect 5.2    18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 290 34 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   250   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_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 5.0   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 260 38 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_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 6.3   320   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 37 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .59   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 290 37 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 36 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .58   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 36 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 39 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/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 38 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_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.9   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 32 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 36 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 38 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.4   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.3 290 43 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 6.6   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 290 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   250   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.1 240 31 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 35 false(no-overflow) 1 wit inspect 3.3  260 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 31 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 32 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 34 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.3   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 6.3 340 55 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.8   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.2 250 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   230   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 4.3 240 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 32 false(no-overflow) 1 wit inspect 2.2  260 false(no-overflow) 1 wit inspect 5.7   320   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 340 45 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 37 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-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect 3.9 230 31 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 280 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 37 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.5   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 32 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   240   true -32 wit inspect .60   19    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 290 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_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 3.3   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 34 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 40 false(no-overflow) 1 wit inspect 3.3  250 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .76   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 5.0 290 43 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 5.8 290 48 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 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-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 38 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.7   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 5.3   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 34 false(no-overflow) 1 wit inspect 3.8  280 false(no-overflow) 1 wit inspect 4.5   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 290 46 false(no-overflow) 1 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 6.2   270   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 290 41 false(no-overflow) 1 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 32 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 240 37 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 32 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 40 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect 3.9 240 30 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 3.2   220   true -32 wit inspect .61   19    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 35 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 34 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 32 false(no-overflow) 1 wit inspect 2.4  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 35 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 280 36 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.9   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 300 41 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.3   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 280 40 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.9   240   true -32 wit inspect .62   19    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 290 39 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 6.5 340 56 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/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 270 37 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect 5.8 290 51 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 6.4   270   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/gcd1_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 5.0   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 300 44 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 34 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.8   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   3800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 8.6 400 75 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 5.0 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 1 wit inspect 7.0 370 57 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 8.1 380 61 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect 46   1400 450 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 1 wit inspect 10   490 76 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     6000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 51   1700 470 - wit inspect - wit inspect - wit inspect true 2 wit inspect 39     2000  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect 7.0 340 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 8.9 490 67 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect 6.9 320 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 5.0 290 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 6.6 320 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 6.5 330 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   290  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 1 wit inspect 10   520 84 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4800  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 2 wit inspect 10   500 92 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.9   440  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 7.6 360 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   290  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 6.4 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4   280  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4900 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .049 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 wit inspect 8.8 480 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8   440  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.6 290 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .041 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 50   1500 500 - wit inspect - wit inspect - wit inspect true 2 wit inspect 39     2100  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect 4.0 240 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   250  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 5.7 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 5.0 280 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 5.2 300 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 5.2 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 5.7 300 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 5.7 310 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 wit inspect 6.0 300 53 - 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 true 2 wit inspect 120   4000 1500 - wit inspect - wit inspect - wit inspect true 2 wit inspect 140     3600  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4800 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 8.6 470 76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   430  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 4.7 290 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   270  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 2 wit inspect 7.4 330 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 4.6 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900   5400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect 4.6 290 35 - 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 7.0 360 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   260  
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   990 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 wit inspect 11   540 99 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1   360  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c true 2 wit inspect 8.7 450 70 - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     540  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 5.6 320 48 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   280  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.5 280 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   270  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 6.2 300 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 4.8 280 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 6.4 300 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect 4.6 280 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   330  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect 5.9 300 48 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 5.9 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 6.9 310 58 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9   270  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 7.7 380 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 360     5400  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 47 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   270  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect 5.4 290 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect 5.3 280 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   270  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect 5.2 290 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   280  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 6.5 310 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3   430  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect 5.4 290 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 35 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .62   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 32 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   250   error (2) 0 wit inspect .63   19    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900   4800 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .041 4.9 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 33 false(no-overflow) 1 wit inspect 3.1  250 false(no-overflow) 1 wit inspect 5.5   270   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .64   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 33 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   250   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 41 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-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect 9.2 450 80 timeout 0 wit inspect 91    530 false(no-overflow) 1 wit inspect 11     390   true -32 wit inspect .62   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c true -32 wit inspect 60   690 750 error (1) 0 wit inspect .64 48 timeout 0 wit inspect 97     590   error (1) 0 wit inspect .10   9.0  - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 5700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .042 4.8
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 2 wit inspect 7.3 370 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c true 1 wit inspect 58   1600 420 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4900  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .044 4.8
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 6200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 0 wit inspect 33   700 390 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 42 - 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 70   1300 690 - wit inspect - wit inspect - wit inspect true 2 wit inspect 57     1100  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2500 11000 - 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   5500 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.9
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 280 319 25000 190000 320000 158 148 700 41000 158 150 840 37000 158 -4148 590 2800 122 196 6100 67000
    correct results 248 346 1900 83000 17000 148 148 520 39000 150 150 740 36000 12 12 19 220 98 196 1300 42000
        correct true 98 196 990 42000 8900 0 0 0 98 196 1300 42000
        correct false 150 150 920 41000 8200 148 148 520 39000 150 150 740 36000 12 12 19 220 0
    correct-unconfimed results 5 5 93 3300 700 0 0 0 0
        correct-unconfirmed true 5 5 93 3300 700 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 1 -32 60 690 750 0 0 130 -4160 85 2400 0
        incorrect true 1 -32 60 690 750 0 0 130 -4160 85 2400 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 319 148 150 -4148 196
Run set utaipan.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.NoOverflows-BitVectors