Tool ULTIMATE Automizer 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-03 11:17:40 CET 2017-12-03 11:52:01 CET 2017-12-03 12:09:33 CET 2017-12-03 12:09:49 CET 2017-12-03 11:53:41 CET
Run set uautomizer.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.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/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_1117.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.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.1 240 32 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.8 260 40 false(no-overflow) 1 wit inspect 4.0  290 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 240 38 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.4   240   true -32 wit inspect .61   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.2 240 37 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 230 32 false(no-overflow) 1 wit inspect 4.1  260 false(no-overflow) 1 wit inspect 4.5   210   true -32 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.7 270 44 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.2 240 39 false(no-overflow) 1 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 4.4   240   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.5 270 38 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 4.9   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 250 36 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 4.6   240   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect 4.1 240 35 false(no-overflow) 1 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.6   210   true -32 wit inspect .65   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect 4.0 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect 4.6 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect 4.0 230 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   290  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect 4.1 240 35 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect 4.4 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 340 49 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .61   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 38 false(no-overflow) 1 wit inspect 4.2  280 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.6   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 230 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 6.0   320   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Binary_Search_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 5.0   250   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 280 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout 0 wit inspect 900   4400 14000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .048 5.0 error (invalid witness file) 0 wit inspect .0025 .34 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 5.0 290 40 false(no-overflow) 1 wit inspect 3.4  280 false(no-overflow) 1 wit inspect 4.9   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 270 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Gothenburg_v2_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 5.1   230   true -32 wit inspect .64   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.4  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .63   19    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 36 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 3.4   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 230 39 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 270 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect 6.3 340 47 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 44 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect 3.9 240 34 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 240 37 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 23   780 200 false(no-overflow) 1 wit inspect 22    950 false(no-overflow) 1 wit inspect 4.9   250   false(no-overflow) 1 wit inspect .63   19    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 230 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   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.2 240 38 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   220   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c timeout 0 wit inspect 900   3900 15000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .042 4.8 error (invalid witness file) 0 wit inspect .0028 .26 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.2   220   false(no-overflow) 1 wit inspect 1.4    18    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 330 45 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 36 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.3   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 36 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 33 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.4   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 250 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.4   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted/RecursiveNonterminating_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.6   230   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted/Rotation180_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 4.4   240   timeout 0 wit inspect 96      19    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 36 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.1 240 34 false(no-overflow) 1 wit inspect 3.1  250 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted/Singapore_v2_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   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Stockholm_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 .64   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 280 41 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect 13   660 120 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.4   270   true -32 wit inspect .64   19    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 280 43 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   250   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 6.0 320 40 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   240   true -32 wit inspect .59   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout 0 wit inspect 900   5300 14000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .039 4.8 error (invalid witness file) 0 wit inspect .0052 .26 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.3 360 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 30   940 320 - wit inspect - wit inspect - wit inspect true 2 wit inspect 40     840  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c true 2 wit inspect 4.6 280 36 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 300 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   260  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.2 300 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.0 300 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 17   720 150 - wit inspect - wit inspect - wit inspect true 2 wit inspect 21     640  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.1 230 38 - 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 300 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.6 290 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.5 310 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   250  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 4.7 290 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4900 13000 - 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   2000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 3.8 240 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.3 310 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     270  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 9.8 540 79 - 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 8.5 450 66 - 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 19   790 170 - wit inspect - wit inspect - wit inspect true 2 wit inspect 20     640  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 12   560 93 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     490  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 8.4 480 71 - 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 12   530 99 - 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 11   550 83 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     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 15     550  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect 4.1 240 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   210  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect 5.3 300 45 - 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 4.9 280 44 - 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 4.9 280 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.0 290 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   260  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 5.5 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 300 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.8 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   250  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.1 240 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   210  
termination-crafted/WhileTrue_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.3   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   5300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.7 300 43 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3   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 5.1 280 46 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/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   240   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 240 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.1   220   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect 5.9 300 49 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.6   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_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 5.0   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect 7.1 370 56 timeout 0 wit inspect 91    1100 false(no-overflow) 1 wit inspect 5.1   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout 0 wit inspect 900   5300 15000 error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0037 .32 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect 5.0 290 42 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout 0 wit inspect 900   5000 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .044 4.8 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout 0 wit inspect 900   8500 9900 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .0045 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 35 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 240 39 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.2   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 290 41 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.4   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.9 300 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 280 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.3   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.4 250 37 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 5.5   250   true -32 wit inspect .63   19    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 250 36 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect 5.8    18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.1   250   error (2) 0 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 40 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 36 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.9   250   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_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.3   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 41 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.4   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 35 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.7   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 280 37 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 5.6   270   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.2 240 32 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .64   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 230 34 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 4.9   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 3.9 230 31 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.3   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 39 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.4   260   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 39 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 32 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 4.6   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.1 250 41 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.06_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 5.2   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 36 false(no-overflow) 1 wit inspect 3.4  280 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 34 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.4   220   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 290 43 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 6.0   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 4.7 300 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.0   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect 6.2 330 45 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.2   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 34 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   220   timeout 0 wit inspect 96      19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 34 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_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.8   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 37 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-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect 4.4 270 36 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   260   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 230 33 false(no-overflow) 1 wit inspect 3.1  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.0 240 33 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 31 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.2   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 250 33 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 4.5   220   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 37 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   240   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_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 5.0   240   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect 6.5 340 48 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-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_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 5.0   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_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.9   230   true -32 wit inspect .64   19    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect 4.6 280 35 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.2   270   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 38 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.2   230   true -32 wit inspect .63   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.3  260 false(no-overflow) 1 wit inspect 4.7   220   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 38 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 4.3   230   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_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.8   230   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 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-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_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   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.9 290 39 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 33 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 5.0   230   true -32 wit inspect .58   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 37 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.4   250   true -32 wit inspect 2.6    18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 38 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect 2.0    18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 280 42 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 300 56 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-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 32 false(no-overflow) 1 wit inspect 3.2  250 false(no-overflow) 1 wit inspect 5.0   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 290 43 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.6   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.1 240 32 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.6   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 37 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 5.7 310 53 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 6.3   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.1 290 42 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.9   320   true -32 wit inspect .60   19    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_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 5.1   250   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 35 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.1   250   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 240 37 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.5   260   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 39 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   260   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 240 33 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 240 34 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.1   220   true -32 wit inspect .60   18    - 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.4  270 false(no-overflow) 1 wit inspect 4.7   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.0 240 32 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.3   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect 4.0 250 36 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/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 36 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 4.8   220   true -32 wit inspect .63   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 37 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.5   240   true -32 wit inspect 3.4    18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect 4.8 290 37 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/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 5.1 290 40 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect 5.3 280 45 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 4.7   250   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect 5.2 300 48 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 39 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.2   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect 4.5 280 40 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.2   250   true -32 wit inspect .63   19    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect 8.0 370 61 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.7   270   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/gcd1_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.2   230   true -32 wit inspect .62   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect 5.0 290 48 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.9   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 37 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.8   250   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5100 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.6 280 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 5.6 290 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect 15   640 130 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     510  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4700 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 160   4700 1900 - wit inspect - wit inspect - wit inspect true 2 wit inspect 42     2500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect 5.9 300 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 7.0 330 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect 5.9 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 6.6 320 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 8.4 380 65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2   290  
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c true 2 wit inspect 8.0 450 70 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   260  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 7.8 420 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   340  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 6.0 310 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2500 12000 - 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 8.0 440 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4   420  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.8 290 42 - 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   5400 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900   8100 8900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 160   4900 1800 - wit inspect - wit inspect - wit inspect true 2 wit inspect 43     2400  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect 4.3 230 33 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   220  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 4.8 280 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 4.8 290 49 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3   280  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_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.6   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 44 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 5.4 300 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 5.5 300 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
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   270  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect 110   3500 1400 - wit inspect - wit inspect - wit inspect true 2 wit inspect 140     3300  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_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.0   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 8.0 450 69 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8   440  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 4.6 280 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c true 2 wit inspect 6.1 310 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 4.8 280 43 - 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   5300 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 270 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   250  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 5.0 300 40 - 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   1200 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 wit inspect 9.0 510 67 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4   360  
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c true 2 wit inspect 17   700 160 - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     530  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 5.4 300 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 38 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.8 280 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 5.5 290 50 - 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.5 280 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   250  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 6.0 300 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_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.1   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect 4.5 290 37 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   250  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect 5.4 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   330  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 5.5 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 5.8 300 46 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8   260  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c true 2 wit inspect 4.8 280 39 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   320  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 350   5700 4500 - wit inspect - wit inspect - wit inspect true 2 wit inspect 350     5200  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect 5.1 280 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   270  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect 5.2 280 45 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   270  
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect 5.2 280 42 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect 5.2 290 41 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 8.1 420 71 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   420  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect 5.1 290 40 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect 4.3 250 37 false(no-overflow) 1 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 5.0   250   true -32 wit inspect .64   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.2 250 35 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.0   260   error (2) 0 wit inspect .63   19    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900   1100 6600 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .031 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect 4.1 240 38 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 5.3   260   false(no-overflow) 1 wit inspect .63   19    - wit inspect
termination-numeric/Et2_true_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 5.1   250   true -32 wit inspect .62   18    - wit inspect
termination-numeric/Et3_true_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 5.4   260   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.5 250 38 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.2   260   true -32 wit inspect .64   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect 8.1 450 74 timeout 0 wit inspect 91    530 false(no-overflow) 1 wit inspect 11     400   true -32 wit inspect .60   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 0 wit inspect 900   740 6400 error (invalid witness file) 0 wit inspect .53 46 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0044 .29 - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 9900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 2 wit inspect 10   540 86 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     480  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4700 11000 - 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 5.6 290 43 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c timeout 0 wit inspect 900   490 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/TwoWay_true-termination_true-no-overflow.c true 2 wit inspect 12   530 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     500  
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 wit inspect 5.7 300 50 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   270  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 44   1200 460 - wit inspect - wit inspect - wit inspect true 2 wit inspect 57     1100  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect 59   1500 640 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5600 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5600 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 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 351 28000 230000 370000 158 148 690 41000 158 150 750 36000 158 -4018 590 2800 122 200 2300 47000
    correct results 250 350 2200 93000 21000 148 148 510 39000 150 150 750 36000 14 14 17 260 100 200 1300 44000
        correct true 100 200 1500 53000 16000 0 0 0 100 200 1300 44000
        correct false 150 150 700 40000 6000 148 148 510 39000 150 150 750 36000 14 14 17 260 0
    correct-unconfimed results 1 1 59 1500 640 0 0 0 0
        correct-unconfirmed true 1 1 59 1500 640 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 0 126 -4032 90 2300 0
        incorrect true 0 0 0 126 -4032 90 2300 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 351 148 150 -4018 200
Run set uautomizer.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.NoOverflows-BitVectors