Tool CBMC 5.8 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* [apollon058; apollon077; apollon078; apollon114] [apollon077; apollon078; apollon135; apollon137; apollon144] apollon* [apollon039; apollon060; apollon077; apollon078]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 11:16:27 CET 2017-12-01 12:31:21 CET 2017-12-01 12:51:49 CET 2017-12-01 12:54:09 CET 2017-12-01 12:35:01 CET
Run set cbmc.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_1116.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/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_1116.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_1116.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 .25 34 2.5 false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 3.0   220   true -32 wit inspect .63   18    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect .26 34 2.5 true -32 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.5   260   true -32 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect .27 34 2.1 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.3   240   true -32 wit inspect .79   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect .25 34 2.5 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .81   18    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect .25 34 2.4 false(no-overflow) 1 wit inspect 4.3  270 false(no-overflow) 1 wit inspect 3.1   210   true -32 wit inspect .77   19    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .26 34 2.1 true -32 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.2   250   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .24 34 2.3 false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 3.4   250   false(no-overflow) 1 wit inspect .65   19    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .24 34 2.0 true -32 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 5.9   250   false(no-overflow) 1 wit inspect .83   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .26 34 2.2 true -32 wit inspect 3.8  260 false(no-overflow) 1 wit inspect 4.5   250   false(no-overflow) 1 wit inspect .72   19    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect .27 34 2.2 true -32 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   240   true -32 wit inspect .83   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect .44 34 5.1 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect .47 34 4.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5   260  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect .44 34 4.1 - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect .47 34 4.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect .46 34 4.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.0 true -32 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 5.7   210   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect .28 36 2.6 true -32 wit inspect 4.8  340 false(no-overflow) 1 wit inspect 6.0   250   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.5 timeout 0 wit inspect 91    700 false(no-overflow) 1 wit inspect 3.4   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.8 false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 3.2   220   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.3 false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 true -32 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 4.9   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect .28 34 2.6 false(no-overflow) 1 wit inspect 18    450 false(no-overflow) 1 wit inspect 5.2   270   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.1 true -32 wit inspect 3.6  270 true -32 wit inspect 2.9   220   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c error (42) 0 wit inspect 870    5100 5000   error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.3 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 4.1   260   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 true -32 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 5.4   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect .26 35 2.0 true -32 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .29 33 2.4 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 4.5   270   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 true -32 wit inspect 3.5  260 true -32 wit inspect 5.2   210   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.2 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.3 true -32 wit inspect 3.0  270 false(no-overflow) 1 wit inspect 5.8   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.4   270   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.3 true -32 wit inspect 3.9  270 false(no-overflow) 1 wit inspect 6.3   260   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.6 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 6.0   250   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.1 false(no-overflow) 1 wit inspect 3.8  280 false(no-overflow) 1 wit inspect 3.8   270   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 true -32 wit inspect 3.5  310 true -32 wit inspect 5.3   210   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.2 true -32 wit inspect 4.6  300 false(no-overflow) 1 wit inspect 3.5   270   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect 1.8  35 20   true -32 wit inspect 26    2200 out of memory 0 wit inspect 59     7000   false(no-overflow) 1 wit inspect .69   19    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.5 true -32 wit inspect 3.4  260 true -32 wit inspect 5.1   210   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 3.1   210   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (42) 0 wit inspect 880    5100 4300   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.5   260   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 1.9 true -32 wit inspect 3.5  260 true -32 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.0 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.5   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.4 false(no-overflow) 1 wit inspect 3.0  270 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 3.9   220   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .25 35 2.4 true -32 wit inspect 4.0  270 false(no-overflow) 1 wit inspect 3.5   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c witness invalid (false(no-overflow)) 0 wit inspect .25 33 2.2 timeout 0 wit inspect 91    3000 true -32 wit inspect 3.5   230   error (invalid witness file) 0 wit inspect .66   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.1 true -32 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 3.0   210   error (2) 0 wit inspect .66   18    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 true -32 wit inspect 3.2  260 true -32 wit inspect 4.4   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .28 35 2.1 true -32 wit inspect 2.7  260 true -32 wit inspect 5.7   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.3 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 true -32 wit inspect 2.6  260 true -32 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.0 false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 true -32 wit inspect 3.7  280 false(no-overflow) 1 wit inspect 5.5   220   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 true -32 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.2   280   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.5 true -32 wit inspect 3.4  260 true -32 wit inspect 4.9   240   false(no-overflow) 1 wit inspect .67   19    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .24 35 2.5 true -32 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 5.1   250   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.2 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c error (42) 0 wit inspect 870    2200 3100   error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.2  34 28   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    3000 3200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c error (42) 0 wit inspect 870    3900 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    3800 3000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .034 4.9
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    5300 4700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    5500 5800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .45 33 3.8 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    2200 3200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    8400 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    4600 5900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    4500 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    3200 4900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    3900 3500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c error (134) 0 wit inspect 50    14000 600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c error (134) 0 wit inspect 58    14000 730   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 210    15000 2800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    1200 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    2000 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    3200 4100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    310 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    290 2400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    710 3800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    480 3200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    700 3600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    810 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    4100 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c error (42) 0 wit inspect 870    2700 5600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    5300 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    2200 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    2100 6800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    830 9100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c error (42) 0 wit inspect 870    4500 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    1300 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    5100 4100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .050 4.9
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .39 33 5.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 1 wit inspect .41 33 4.3 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 2.8   200  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.2  61 55   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   270  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c error (42) 0 wit inspect 870    2400 4200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 1.9 true -32 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 6.5   260   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect .28 36 2.6 true -32 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 6.9   260   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 true -32 wit inspect 4.2  260 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.5 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.6   240   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect .29 33 2.6 true -32 wit inspect 5.3  270 false(no-overflow) 1 wit inspect 8.5   280   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.3 false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.7 true -32 wit inspect 5.2  270 false(no-overflow) 1 wit inspect 3.6   260   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c error (42) 0 wit inspect 870    2400 3400   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .045 4.9 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 1.5 true -32 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.2   260   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 1.9 false(no-overflow) 1 wit inspect 2.8  260 false(no-overflow) 1 wit inspect 5.0   260   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c error (42) 0 wit inspect 870    1500 5000   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c error (42) 0 wit inspect 870    590 9400   error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.0 false(no-overflow) 1 wit inspect 2.8  270 false(no-overflow) 1 wit inspect 4.4   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.2 true -32 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 true -32 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 3.7   270   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.3 true -32 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.7   260   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.6 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.4   260   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect .35 38 2.6 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 6.0   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect .28 35 2.4 true -32 wit inspect 7.1  290 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 true -32 wit inspect 4.1  270 false(no-overflow) 1 wit inspect 3.5   250   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.2 false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 3.4   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.2 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 6.1   260   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.3 true -32 wit inspect 3.5  250 false(no-overflow) 1 wit inspect 4.8   250   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 1.9 false(no-overflow) 1 wit inspect 3.2  270 true -32 wit inspect 3.0   210   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.7 false(no-overflow) 1 wit inspect 3.1  270 false(no-overflow) 1 wit inspect 3.3   230   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.8 false(no-overflow) 1 wit inspect 3.0  270 false(no-overflow) 1 wit inspect 3.7   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 1.8 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.1 false(no-overflow) 1 wit inspect 3.5  270 false(no-overflow) 1 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 1.9 true -32 wit inspect 3.5  260 true -32 wit inspect 5.7   220   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.3 true -32 wit inspect 2.9  270 true -32 wit inspect 3.2   220   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.2 true -32 wit inspect 3.0  280 false(no-overflow) 1 wit inspect 3.0   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.2 true -32 wit inspect 76    320 true -32 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 true -32 wit inspect 3.2  260 true -32 wit inspect 3.2   210   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect .27 34 2.2 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.2 true -32 wit inspect 4.3  320 true -32 wit inspect 3.0   220   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.2 false(no-overflow) 1 wit inspect 3.0  270 true -32 wit inspect 4.0   210   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 7.5   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.4 true -32 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 6.7   250   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect .27 34 2.9 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.0 true -32 wit inspect 3.8  270 false(no-overflow) 1 wit inspect 3.5   250   false(no-overflow) 1 wit inspect .86   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.0 false(no-overflow) 1 wit inspect 2.8  260 false(no-overflow) 1 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.4   220   true -32 wit inspect .76   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 1.8 false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.4   210   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.7   260   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.5 false(no-overflow) 1 wit inspect 2.7  260 true -32 wit inspect 5.0   220   error (2) 0 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.8 true -32 wit inspect 4.5  370 false(no-overflow) 1 wit inspect 6.0   250   false(no-overflow) 1 wit inspect .81   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.9 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.1 false(no-overflow) 1 wit inspect 2.8  260 true -32 wit inspect 3.0   210   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.7 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.2   230   true -32 wit inspect .73   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.3 true -32 wit inspect 3.7  270 false(no-overflow) 1 wit inspect 3.3   250   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 1.9 true -32 wit inspect 4.2  270 false(no-overflow) 1 wit inspect 4.7   240   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 true -32 wit inspect 4.0  280 false(no-overflow) 1 wit inspect 3.5   240   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 false(no-overflow) 1 wit inspect 2.9  270 true -32 wit inspect 3.1   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.4 true -32 wit inspect 3.1  280 false(no-overflow) 1 wit inspect 3.6   250   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.3 true -32 wit inspect 3.8  260 true -32 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.2 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect .24 35 2.3 false(no-overflow) 1 wit inspect 3.4  270 false(no-overflow) 1 wit inspect 3.2   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 1.9 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 5.7   230   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 true -32 wit inspect 3.7  280 false(no-overflow) 1 wit inspect 3.3   240   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 false(no-overflow) 1 wit inspect 2.9  260 true -32 wit inspect 3.1   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.2 true -32 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 7.0   260   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 false(no-overflow) 1 wit inspect 3.0  270 true -32 wit inspect 3.2   230   false(no-overflow) 1 wit inspect .79   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.1 true -32 wit inspect 3.8  260 true -32 wit inspect 5.3   220   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.1 false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.2   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.1 true -32 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 3.5   260   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.0 true -32 wit inspect 4.5  260 true -32 wit inspect 3.4   240   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .29 33 2.0 true -32 wit inspect 3.1  250 true -32 wit inspect 5.5   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.6 false(no-overflow) 1 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 6.4   270   error (2) 0 wit inspect .65   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.4 false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 3.1   230   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 false(no-overflow) 1 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.3 timeout 0 wit inspect 91    510 false(no-overflow) 1 wit inspect 10     470   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.6 false(no-overflow) 1 wit inspect 6.0  290 false(no-overflow) 1 wit inspect 4.9   270   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect .29 33 2.4 timeout 0 wit inspect 91    1000 false(no-overflow) 1 wit inspect 4.6   250   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.1 false(no-overflow) 1 wit inspect 3.2  270 false(no-overflow) 1 wit inspect 3.5   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.3 false(no-overflow) 1 wit inspect 3.0  270 true -32 wit inspect 5.2   210   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.5 true -32 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 6.3   270   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .24 33 2.6 true -32 wit inspect 3.9  260 true -32 wit inspect 3.0   210   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 true -32 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.1 true -32 wit inspect 3.9  300 false(no-overflow) 1 wit inspect 3.1   230   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.0 true -32 wit inspect 3.8  270 true -32 wit inspect 3.1   210   false(no-overflow) 1 wit inspect .76   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .25 35 2.0 true -32 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 5.6   260   error (2) 0 wit inspect .69   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.1 false(no-overflow) 1 wit inspect 3.1  270 false(no-overflow) 1 wit inspect 3.3   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 1.9 true -32 wit inspect 3.5  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.7 true -32 wit inspect 3.6  270 false(no-overflow) 1 wit inspect 5.6   260   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.2 timeout 0 wit inspect 91    1700 false(no-overflow) 1 wit inspect 6.5   260   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.2 true -32 wit inspect 9.2  300 false(no-overflow) 1 wit inspect 4.0   270   false(no-overflow) 1 wit inspect .78   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .23 33 2.4 true -32 wit inspect 11    420 false(no-overflow) 1 wit inspect 4.0   270   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .26 33 2.0 false(no-overflow) 1 wit inspect 3.7  260 false(no-overflow) 1 wit inspect 3.3   230   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.6 false(no-overflow) 1 wit inspect 3.5  270 true -32 wit inspect 3.1   210   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect .44 34 4.6 true -32 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.8   260   true -32 wit inspect .67   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect .25 35 2.3 false(no-overflow) 1 wit inspect 3.2  260 false(no-overflow) 1 wit inspect 6.0   240   error (2) 0 wit inspect .62   19    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect .30 34 3.1 false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 4.6   270   false(no-overflow) 1 wit inspect .80   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect .27 35 2.1 true -32 wit inspect 5.0  280 false(no-overflow) 1 wit inspect 6.8   270   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    590 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1800 6000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.3  61 44   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2300 3900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1700 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1500 4800   - 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 error (42) 0 wit inspect 870    610 8700   - 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 1.4  34 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 34     2500  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1400 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 8500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1300 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2700 7200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5500 5100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1100 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1400 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c error (42) 0 wit inspect 870    360 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    360 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2400 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.8
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    7000 3600   - 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 error (42) 0 wit inspect 870    3100 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.3  62 47   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   270  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2300 3900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    610 10000   - 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 1.4  35 18   - wit inspect - wit inspect - wit inspect true 2 wit inspect 43     2300  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c error (42) 0 wit inspect 880    8400 3900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1100 7600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 5600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 7100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1600 7700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2000 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    520 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1100 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1300 7200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect 2.7  35 32   - wit inspect - wit inspect - wit inspect true 2 wit inspect 140     3500  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1600 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1000 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    3100 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c error (42) 0 wit inspect 880    4500 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    3400 4500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    770 4900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c error (42) 0 wit inspect 870    3000 7900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1300 7400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1700 6300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    640 8300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    7400 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (134) 0 wit inspect 490    15000 5000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    980 5900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1800 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 2.5  37 27   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6   260  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1700 4300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    4400 3300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2400 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1300 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c error (42) 0 wit inspect 870    2800 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    13000 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    780 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2600 7900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c error (42) 0 wit inspect 870    2900 5600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 8.1  180 93   - wit inspect - wit inspect - wit inspect true 2 wit inspect 380     5300  
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    8400 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 3900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    7500 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 3400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    1200 4400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 9.4  160 110   - wit inspect - wit inspect - wit inspect true 2 wit inspect 60     540  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (6) 0 wit inspect 730    8500 3800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 2.4 true -32 wit inspect 5.3  290 false(no-overflow) 1 wit inspect 3.9   270   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect .27 35 2.2 false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 3.5   260   error (2) 0 wit inspect .66   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c witness invalid (false(no-overflow)) 0 wit inspect 23    250 280   timeout 0 wit inspect 91    3100 true -32 wit inspect 7.1   730   error (invalid witness file) 0 wit inspect .60   22    - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect .27 33 1.8 true -32 wit inspect 4.3  260 false(no-overflow) 1 wit inspect 7.1   340   true -32 wit inspect .71   19    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect .28 33 2.3 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.4   250   error (2) 0 wit inspect .61   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect .25 33 2.1 false(no-overflow) 1 wit inspect 3.6  260 false(no-overflow) 1 wit inspect 3.9   280   error (2) 0 wit inspect .66   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect .27 34 2.5 false(no-overflow) 1 wit inspect 3.3  270 false(no-overflow) 1 wit inspect 3.6   260   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c witness invalid (false(no-overflow)) 0 wit inspect .30 34 2.5 timeout 0 wit inspect 98    3400 true -32 wit inspect 6.3   240   error (invalid witness file) 0 wit inspect .55   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 2.0  78 25   timeout 0 wit inspect 92    1900 false(no-overflow) 1 wit inspect 10     500   false(no-overflow) 1 wit inspect .65   19    - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    330 2600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2800 6600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    260 3000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c out of memory 0 wit inspect 730    15000 5200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 1 wit inspect 5.0  91 55   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     510  
termination-numeric/Parts_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    840 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    2500 4600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/gcd01_true-termination_true-no-overflow.c error (42) 0 wit inspect 880    5000 4800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 2.7  38 29   - wit inspect - wit inspect - wit inspect true 2 wit inspect 61     1000  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect 2.6  36 25   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5800 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (42) 0 wit inspect 870    5800 4600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .046 4.8
termination-numeric/twisted_true-termination_true-no-overflow.c error (134) 0 wit inspect 170    13000 1900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 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 188 90000   370000 560000 158 -2397 1400 57000 158 -1169 730 44000 158 -255 110   2800 122 36 2700 22000
    correct results 167 185 88   6000 900 67 67 240 18000 111 111 510 28000 129 129 90   2400 18 36 770 18000
        correct true 18 36 46   980 530 0 0 0 18 36 770 18000
        correct false 149 149 42   5000 380 67 67 240 18000 111 111 510 28000 129 129 90   2400 0
    correct-unconfimed results 3 3 8.1 160 84 0 0 0 0
        correct-unconfirmed true 3 3 8.1 160 84 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 77 -2464 390 23000 40 -1280 170 9300 12 -384 8.6 220 0
        incorrect true 0 77 -2464 390 23000 40 -1280 170 9300 12 -384 8.6 220 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 188 -2397 -1169 -255 36
Run set cbmc.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.NoOverflows-BitVectors