Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 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* [apollon075; apollon077; apollon078] [apollon016; apollon038; apollon064; apollon078; apollon084; apollon107] [apollon016; apollon038; apollon078; apollon084; apollon107] 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-01 13:07:37 CET 2017-12-01 14:46:42 CET 2017-12-01 15:12:32 CET 2017-12-01 15:13:50 CET 2017-12-01 14:48:36 CET
Run set depthk.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1307.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/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_1307.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) 0 wit inspect 4.1  410 30   error (invalid witness file) 0 wit inspect 1.9  170 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .067  9.1  - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 0 wit inspect 3.8  420 33   error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .066  9.0  - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.2  420 27   error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .065  9.1  - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 0 wit inspect 3.9  420 39   error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .070  9.1  - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.2  420 29   error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.2   220   error (1) 0 wit inspect .067  9.1  - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.0  410 32   error (invalid witness file) 0 wit inspect 2.5  190 true -32 wit inspect 4.1   210   error (1) 0 wit inspect .088  9.0  - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 0 wit inspect 3.9  420 30   error (invalid witness file) 0 wit inspect 2.1  170 true -32 wit inspect 4.4   210   error (1) 0 wit inspect .066  9.1  - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.1  420 30   error (invalid witness file) 0 wit inspect 1.7  170 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .066  9.0  - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.0  420 31   error (invalid witness file) 0 wit inspect 1.9  170 true -32 wit inspect 4.4   210   error (1) 0 wit inspect .067  9.1  - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 0 wit inspect 4.0  420 32   error (invalid witness file) 0 wit inspect 1.6  170 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .065  9.0  - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i unknown 0 wit inspect 1.3  48 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8   220  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i unknown 0 wit inspect 1.6  49 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   250  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i unknown 0 wit inspect 1.7  48 21   - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i false(no-overflow) -16 wit inspect 480    420 5400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i unknown 0 wit inspect 480    110 6200   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 0 wit inspect .53 75 6.6 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 0 wit inspect .60 75 6.7 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 0 wit inspect .61 49 7.3 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .067  8.9  - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.0 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.1   210   error (1) 0 wit inspect .073  9.0  - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.9 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 0 wit inspect .40 48 5.0 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 0 wit inspect .85 75 12   error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.2   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c unknown 0 wit inspect 77    75 1000   error (invalid witness file) 0 wit inspect .49 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c unknown 0 wit inspect 21    75 260   error (invalid witness file) 0 wit inspect .49 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.7 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .066  9.1  - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 0 wit inspect .61 75 7.4 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.9   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 7.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 0 wit inspect .53 75 6.4 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.2   210   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.9 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.0 error (invalid witness file) 0 wit inspect 1.9  170 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 4.3 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .064  9.1  - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.6 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 0 wit inspect .57 49 6.5 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.9   230   error (1) 0 wit inspect .069  9.1  - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 0 wit inspect .52 48 5.6 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.2 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.1   210   error (1) 0 wit inspect .066  8.9  - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 4.3 error (invalid witness file) 0 wit inspect 1.4  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .073  9.0  - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 0 wit inspect 12    75 140   error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .070  9.0  - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 5.6 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c unknown 0 wit inspect 76    75 950   error (invalid witness file) 0 wit inspect .44 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.3   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.5 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 7.2 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 0 wit inspect .53 75 7.7 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.2   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.0 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.2   210   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 0 wit inspect .58 75 6.6 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 0 wit inspect .57 49 7.7 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 5.3   230   error (1) 0 wit inspect .067  8.9  - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 0 wit inspect .56 49 7.0 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 0 wit inspect .36 75 4.1 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.7 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.5 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .071  8.9  - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 8.1 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .069  8.9  - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 7.0 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .064  9.1  - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 7.5 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.2   210   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.2 error (invalid witness file) 0 wit inspect 2.2  160 true -32 wit inspect 4.2   210   error (1) 0 wit inspect .066  8.9  - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 6.9 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 0 wit inspect .62 77 7.9 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 5.1   230   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect .41 75 4.6 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.6 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted/easy2_false-no-overflow.c unknown 0 wit inspect 160    390 2300   error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2  76 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 60    100 790   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c unknown 0 wit inspect 1.3  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6   270  
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  100 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   270  
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 7.6  75 92   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 7.2  75 89   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.5  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 380    560 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.9
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2  75 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 68    75 850   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   270  
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.3  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   270  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.5  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   260  
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 38    100 500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c unknown 0 wit inspect 120    160 1500   - 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 unknown 0 wit inspect 1.2  75 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   220  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 900    120 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 510    15000 7100   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   280  
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     500  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 450    15000 6300   - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     480  
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 440    15000 6000   - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     650  
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 440    15000 5900   - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     520  
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 390    15000 4400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     440  
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 440    15000 6000   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     500  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 500    15000 5300   - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     470  
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 500    15000 7300   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     560  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.3  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8   270  
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   260  
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c unknown 0 wit inspect 72    75 1000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.3  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   260  
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   270  
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2  48 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.4  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 120    240 1600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 0 wit inspect .58 100 6.9 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 0 wit inspect .60 130 6.5 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.9   220   error (1) 0 wit inspect .068  8.9  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.7 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 0 wit inspect .63 100 6.9 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 5.1   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 4.8 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 0 wit inspect .58 130 6.7 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .069  8.9  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c unknown 0 wit inspect 160    390 2100   error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.5 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .076  9.1  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.0 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .065  9.1  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c unknown 0 wit inspect 900    710 6100   error (invalid witness file) 0 wit inspect .49 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .33 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c unknown 0 wit inspect 900    140 12000   error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .029 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.5 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.6 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.8 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .070  9.0  - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 4.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 0 wit inspect .61 76 7.1 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 0 wit inspect 480    130 6900   error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.7 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .087  8.9  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 0 wit inspect .41 75 4.5 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 2.9   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.8 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.9   240   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 0 wit inspect .44 76 4.8 error (invalid witness file) 0 wit inspect 2.3  160 true -32 wit inspect 5.1   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 0 wit inspect .42 76 4.6 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.4 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.1   210   error (1) 0 wit inspect .064  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 5.1 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .069  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.4 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.6   210   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .065  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 5.0 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .065  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 7.4 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.8 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.2   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.6 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.3 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 7.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.5 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 4.7 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.1   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.1 error (invalid witness file) 0 wit inspect 2.2  160 true -32 wit inspect 4.1   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 5.7 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 5.0   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.2 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.4 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.3 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.9   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.9 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 5.5 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.4   210   error (1) 0 wit inspect .066  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 4.0 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 0 wit inspect .36 75 4.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 6.8 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 0 wit inspect .36 75 4.3 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 7.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.7   210   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 4.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.8 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 5.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   220   error (1) 0 wit inspect .081  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 4.3 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 5.2 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 7.0 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 7.5 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .066  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.6 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.7   240   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.6 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 3.0   210   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 5.3 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 0 wit inspect .38 75 3.9 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .070  9.0  - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.6 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 0 wit inspect .39 75 4.8 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.8 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .064  9.0  - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 0 wit inspect .56 100 6.6 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.6 error (invalid witness file) 0 wit inspect 1.6  170 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .068  8.9  - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 7.6 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 0 wit inspect .65 79 8.1 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.7   220   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 7.2 error (invalid witness file) 0 wit inspect 1.4  160 true -32 wit inspect 4.9   220   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 0 wit inspect .58 75 6.4 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.2   220   error (1) 0 wit inspect .065  9.1  - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 6.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   220   error (1) 0 wit inspect .067  8.9  - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 0 wit inspect .57 75 6.8 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .067  9.1  - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 0 wit inspect .56 49 6.5 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 0 wit inspect .56 49 7.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.4   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 0 wit inspect .57 49 6.3 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .070  9.0  - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 0 wit inspect .56 51 7.4 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.1 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .068  8.9  - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 5.9 error (invalid witness file) 0 wit inspect 1.5  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 7.0 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.3   210   error (1) 0 wit inspect .071  9.1  - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 6.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   210   error (1) 0 wit inspect .066  9.1  - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 0 wit inspect .36 75 4.5 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 0 wit inspect .54 75 7.2 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.8   220   error (1) 0 wit inspect .071  8.9  - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 0 wit inspect .53 75 6.5 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 8.4 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 5.0   220   error (1) 0 wit inspect .068  8.9  - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 0 wit inspect .56 76 6.5 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 0 wit inspect .56 75 7.7 error (invalid witness file) 0 wit inspect 1.7  160 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.3 error (invalid witness file) 0 wit inspect 1.6  170 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .069  9.0  - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 0 wit inspect .37 75 4.7 error (invalid witness file) 0 wit inspect 2.2  160 true -32 wit inspect 4.6   220   error (1) 0 wit inspect .069  9.1  - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 0 wit inspect .40 75 4.6 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.3   220   error (1) 0 wit inspect .064  9.0  - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 0 wit inspect .41 75 4.7 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 0 wit inspect .55 75 7.2 error (invalid witness file) 0 wit inspect 2.0  160 true -32 wit inspect 4.4   210   error (1) 0 wit inspect .064  9.1  - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 0 wit inspect .68 76 8.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .067  9.0  - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 0 wit inspect .57 100 6.5 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .066  9.0  - wit inspect
termination-crafted-lit/joey_false-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 630    15000 8800   error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 0 wit inspect .42 75 4.8 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .064  9.1  - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 890    120 9800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c unknown 0 wit inspect 120    240 1700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c unknown 0 wit inspect 900    710 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c unknown 0 wit inspect 900    1200 8000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c unknown 0 wit inspect 890    130 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c unknown 0 wit inspect 7.3  76 89   - wit inspect - wit inspect - wit inspect true 2 wit inspect 32     2400  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8   320  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  100 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.8  100 25   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   310  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c unknown 0 wit inspect 890    110 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c unknown 0 wit inspect 200    270 2800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c unknown 0 wit inspect 43    75 540   - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 30    75 340   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   400  
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.9  100 24   - 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 unknown 0 wit inspect 900    5300 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c unknown 0 wit inspect 130    230 1800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c unknown 0 wit inspect 160    390 2000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c unknown 0 wit inspect 900    130 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c unknown 0 wit inspect 13    76 150   - wit inspect - wit inspect - wit inspect true 2 wit inspect 41     1700  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  75 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3  75 16   - 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 unknown 0 wit inspect 1.3  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c unknown 0 wit inspect 2.0  75 25   - 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 unknown 0 wit inspect 1.2  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   270  
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  75 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   270  
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c unknown 0 wit inspect 1.4  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 140     3600  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 900    160 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 270    190 3600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   260  
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c unknown 0 wit inspect 890    320 11000   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c unknown 0 wit inspect 140    100 1700   - 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 unknown 0 wit inspect 1.5  75 19   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   260  
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 500    110 6300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 890    130 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c unknown 0 wit inspect 580    15000 7300   - 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 unknown 0 wit inspect 450    15000 6000   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     570  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c unknown 0 wit inspect 2.1  75 25   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   260  
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   260  
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   260  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.8  100 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   260  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.7  100 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   270  
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   250  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   250  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  100 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4   250  
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  100 20   - 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 unknown 0 wit inspect 1.3  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   270  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c unknown 0 wit inspect 1.3  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted-lit/aviad_true-termination_true-no-overflow.c unknown 0 wit inspect 22    75 260   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900    590 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900    530 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900    560 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/genady_true-termination_true-no-overflow.c unknown 0 wit inspect 54    75 780   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/strchr_true-no-overflow_true-termination.c false(no-overflow) -16 wit inspect .54 75 5.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   230  
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 0 wit inspect .54 49 6.3 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 0 wit inspect .59 49 6.6 error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 5.1   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 0 wit inspect 27    140 330   error (invalid witness file) 0 wit inspect 2.6  170 true -32 wit inspect 5.1   240   error (1) 0 wit inspect .078  9.1  - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 0 wit inspect .45 49 5.3 error (invalid witness file) 0 wit inspect 2.1  160 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .065  9.0  - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 0 wit inspect .58 49 8.0 error (invalid witness file) 0 wit inspect 1.9  160 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 0 wit inspect .54 49 7.3 error (invalid witness file) 0 wit inspect 1.9  170 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .068  9.1  - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 0 wit inspect .49 49 5.3 error (invalid witness file) 0 wit inspect 1.6  160 true -32 wit inspect 5.0   220   error (1) 0 wit inspect .068  9.0  - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c unknown 0 wit inspect 480    15000 5900   error (1) 0 wit inspect .51 48 false(no-overflow) 1 wit inspect 11     430   error (1) 0 wit inspect .073  9.0  - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 0 wit inspect 1.7  140 21   error (invalid witness file) 0 wit inspect 1.8  160 true -32 wit inspect 11     630   error (1) 0 wit inspect .066  9.1  - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c unknown 0 wit inspect 460    15000 6400   - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 380     7000  
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.6  49 21   - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     490  
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c unknown 0 wit inspect 380    15000 4700   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3  49 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   260  
termination-numeric/LogRecursive_true-termination_true-no-overflow.c unknown 0 wit inspect 2.0  77 24   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     490  
termination-numeric/Parts_true-termination_true-no-overflow.c unknown 0 wit inspect 900    430 8100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 0 wit inspect 5.8  150 52   - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     510  
termination-numeric/gcd01_true-termination_true-no-overflow.c unknown 0 wit inspect 430    15000 5400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 57     1100  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c unknown 0 wit inspect 1.8  49 20   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2900  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c unknown 0 wit inspect 2.5  97 30   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5400  
termination-numeric/rec_counter3_true-termination_true-no-overflow.c unknown 0 wit inspect 2.4  99 28   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5300  
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900    6600 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 280 -32 28000 270000 350000 158 0 270 25000 158 -4767 690 34000 158 0 10 1400 122 170 6000 59000
    correct results 0 0 1 1 11 430 0 85 170 800 33000
        correct true 0 0 0 0 85 170 800 33000
        correct false 0 0 1 1 11 430 0 0
    correct-unconfimed results 149 0 630 15000 8500 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 149 0 630 15000 8500 0 0 0 0
    incorrect results 2 -32 480 500 5400 0 149 -4768 680 33000 0 0
        incorrect true 0 0 149 -4768 680 33000 0 0
        incorrect false 2 -32 480 500 5400 0 0 0 0
score (280 tasks, max score: 402) -32 0 -4767 0 170
Run set depthk.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.NoOverflows-BitVectors