Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-03 04:09:48 CET 2017-12-03 05:12:06 CET 2017-12-03 05:44:30 CET 2017-12-03 05:48:14 CET 2017-12-03 05:20:50 CET
Run set symbiotic.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.NoOverflows-BitVectors
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-03_0409.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/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-03_0409.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-03_0409.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 .17  11 1.8  false(no-overflow) 1 wit inspect 4.0  260 false(no-overflow) 1 wit inspect 4.6   220   true -32 wit inspect .63   19    - wit inspect
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i false(no-overflow) 1 wit inspect .17  11 1.5  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 5.3   260   true -32 wit inspect .70   19    - wit inspect
signedintegeroverflow-regression/Division_false-no-overflow.c.i false(no-overflow) 1 wit inspect .16  11 1.7  false(no-overflow) 1 wit inspect 4.4  260 false(no-overflow) 1 wit inspect 4.7   240   true -32 wit inspect .63   18    - wit inspect
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i false(no-overflow) 1 wit inspect .16  11 1.7  false(no-overflow) 1 wit inspect 3.9  260 false(no-overflow) 1 wit inspect 4.2   220   true -32 wit inspect .62   19    - wit inspect
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i false(no-overflow) 1 wit inspect .17  11 1.5  false(no-overflow) 1 wit inspect 2.9  270 false(no-overflow) 1 wit inspect 5.0   220   true -32 wit inspect .78   18    - wit inspect
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .14  11 1.9  false(no-overflow) 1 wit inspect 4.7  270 false(no-overflow) 1 wit inspect 5.3   250   false(no-overflow) 1 wit inspect .78   18    - wit inspect
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .14  11 1.7  false(no-overflow) 1 wit inspect 4.4  270 false(no-overflow) 1 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .15  11 1.7  false(no-overflow) 1 wit inspect 4.6  260 false(no-overflow) 1 wit inspect 5.3   250   false(no-overflow) 1 wit inspect .77   18    - wit inspect
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i false(no-overflow) 1 wit inspect .14  11 1.8  false(no-overflow) 1 wit inspect 4.8  270 false(no-overflow) 1 wit inspect 6.9   240   false(no-overflow) 1 wit inspect .66   18    - wit inspect
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i false(no-overflow) 1 wit inspect .17  11 1.7  false(no-overflow) 1 wit inspect 4.6  270 false(no-overflow) 1 wit inspect 7.0   240   true -32 wit inspect .79   18    - wit inspect
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow_true-termination.c.i true 2 wit inspect .15  11 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow_true-termination.c.i true 2 wit inspect .16  11 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   260  
signedintegeroverflow-regression/Multiplication_true-no-overflow_true-termination.c.i true 2 wit inspect .15  11 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   210  
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow_true-termination.c.i true 2 wit inspect .15  11 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8   210  
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow_true-termination.c.i true 2 wit inspect .15  11 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
termination-crafted/2Nested_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.9  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 4.5   210   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/4NestedWith3Variables_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.6  false(no-overflow) 1 wit inspect 2.3  270 true -32 wit inspect 4.8   220   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted/Ackermann_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.9  timeout 0 wit inspect 91    1000 true -32 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted/Bangalore_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.1   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Bangalore_v3_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.7  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.4   210   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted/Benghazi_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .73   18    - wit inspect
termination-crafted/Binary_Search_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 7.2   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Cairo_nondet_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.4   220   true -32 wit inspect .61   18    - wit inspect
termination-crafted/Cairo_step2_false-no-overflow.c timeout (timeout) 0 wit inspect 900     170 13000    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect
termination-crafted/Collatz_unknown-termination_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.0  false(no-overflow) 1 wit inspect 3.4  270 true -32 wit inspect 5.4   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Copenhagen_disj_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.6  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.9   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Gothenburg_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.7  false(no-overflow) 1 wit inspect 4.1  260 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/Gothenburg_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.6  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Hanoi_2vars_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.1  260 true -32 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted/Hanoi_3vars_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.5   210   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Hanoi_plus_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.7  280 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.8   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Mysore_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 6.5   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/NestedRecursion_1a_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.8  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted/NestedRecursion_2a_false-no-overflow.c false(no-overflow) 1 wit inspect .15  12 2.1  false(no-overflow) 1 wit inspect 3.2  250 true -32 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/NonTermination1_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.5  270 true -32 wit inspect 5.2   220   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted/NonTermination2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 2.6  270 true -32 wit inspect 4.5   210   true -32 wit inspect .65   18    - wit inspect
termination-crafted/NonTermination4_false-no-overflow.c false(no-overflow) 1 wit inspect .16  11 2.0  timeout 0 wit inspect 91    940 true -32 wit inspect 4.8   260   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/NonTerminationSimple2_false-no-overflow.c false(no-overflow) 1 wit inspect .15  11 1.7  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.2   220   false(no-overflow) 1 wit inspect .91   18    - wit inspect
termination-crafted/NonTerminationSimple3_false-no-overflow.c false(no-overflow) 1 wit inspect .15  12 1.7  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 5.4   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/NonTerminationSimple4_false-no-overflow.c error (1) 0 wit inspect .099 11 1.2  error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
termination-crafted/NonTerminationSimple5_false-no-overflow.c false(no-overflow) 1 wit inspect .17  11 1.7  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 5.8   290   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/NonTerminationSimple6_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.9  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .75   19    - wit inspect
termination-crafted/NonTerminationSimple8_false-no-overflow.c false(no-overflow) 1 wit inspect .18  11 1.7  false(no-overflow) 1 wit inspect 3.5  270 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/NonTerminationSimple9_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 6.7   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Pure2Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.4  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.2   210   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Pure3Phase_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.6  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .77   18    - wit inspect
termination-crafted/RecursiveMultiplication_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.9  false(no-overflow) 1 wit inspect 4.0  270 true -32 wit inspect 5.5   230   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted/RecursiveNonterminating_false-no-overflow.c false(no-overflow) 1 wit inspect .16  14 1.8  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 5.7   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted/Rotation180_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 2.7  260 true -32 wit inspect 3.0   220   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted/Singapore_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.6   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 .19  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.3   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted/Singapore_v1_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 5.5   220   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted/Singapore_v2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted/Stockholm_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 5.7   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted/Thun_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect 5.7    18    - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.9  false(no-overflow) 1 wit inspect 3.1  270 true -32 wit inspect 4.9   240   false(no-overflow) 1 wit inspect 1.2    18    - wit inspect
termination-crafted/aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.3  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 4.5   230   true -32 wit inspect .65   18    - wit inspect
termination-crafted/aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 2.4  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 5.2   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted/easy2_false-no-overflow.c timeout (timeout) 0 wit inspect 900     210 13000    error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .13  11 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   230  
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     250 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout (timeout) 0 wit inspect 900     70 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     180 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     52 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     55 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .20  12 2.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   260  
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     100 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (1) 0 wit inspect .080 11 .63 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.8
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     270 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     170 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     230 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     15 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 300     2900 2500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3800 7900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.9
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .13  11 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   210  
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     76 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     72 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .040 4.9
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     100 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     92 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     130 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     360 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     290 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     400 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     980 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     270 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c true 2 wit inspect .13  11 1.6  - 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 true 2 wit inspect .16  11 1.6  - 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 timeout (timeout) 0 wit inspect 900     4000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .027 4.8
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     250 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     170 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout (timeout) 0 wit inspect 900     250 12000    - 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 timeout (timeout) 0 wit inspect 900     330 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     210 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .14  11 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c true 2 wit inspect .13  11 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   210  
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .15  11 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1   260  
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (timeout) 0 wit inspect 900     180 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.9  false(no-overflow) 1 wit inspect 2.3  260 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .90   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.9  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.8  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 4.3   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .22  12 2.4  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.3   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c false(no-overflow) 1 wit inspect .21  12 2.0  false(no-overflow) 1 wit inspect 3.9  260 true -32 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 5.6   300   false(no-overflow) 1 wit inspect .90   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c false(no-overflow) 1 wit inspect .25  12 2.7  false(no-overflow) 1 wit inspect 3.7  270 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_false-no-overflow.c timeout (timeout) 0 wit inspect 900     200 10000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.7  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.1   210   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_false-no-overflow.c timeout (timeout) 0 wit inspect 900     1900 9800    error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_false-no-overflow.c timeout (timeout) 0 wit inspect 900     4000 8700    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.9  false(no-overflow) 1 wit inspect 2.4  270 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.1   210   true -32 wit inspect .60   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 2.0  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 5.6   220   false(no-overflow) 1 wit inspect .69   18    - wit inspect
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.9  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 5.0   220   false(no-overflow) 1 wit inspect .72   18    - wit inspect
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.9  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 6.0   290   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.3  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c false(no-overflow) 1 wit inspect .21  12 2.1  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 5.9   230   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.8  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 4.8   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 2.3  false(no-overflow) 1 wit inspect 3.3  270 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c false(no-overflow) 1 wit inspect .21  12 2.0  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .70   18    - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.9  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.7  false(no-overflow) 1 wit inspect 3.7  270 true -32 wit inspect 5.4   210   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.2  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 4.8   220   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.0  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.2   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.9  false(no-overflow) 1 wit inspect 3.7  270 true -32 wit inspect 4.3   210   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 2.0  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 6.4   220   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.8  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.8   210   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.0  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.3   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.4   210   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.6  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.9  false(no-overflow) 1 wit inspect 2.4  270 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .71   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.7  false(no-overflow) 1 wit inspect 3.7  270 true -32 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.8  270 true -32 wit inspect 4.0   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 2.3  260 true -32 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.9  false(no-overflow) 1 wit inspect 3.1  260 true -32 wit inspect 4.7   230   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 .16  12 1.9  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.6  false(no-overflow) 1 wit inspect 3.4  270 true -32 wit inspect 4.9   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.2  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.8  false(no-overflow) 1 wit inspect 3.5  270 true -32 wit inspect 4.9   220   true -32 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.5   220   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 6.0   210   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c false(no-overflow) 1 wit inspect .15  12 1.7  false(no-overflow) 1 wit inspect 3.3  250 true -32 wit inspect 6.4   210   error (2) 0 wit inspect .66   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.7  false(no-overflow) 1 wit inspect 3.8  260 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 2.8  270 true -32 wit inspect 5.2   210   false(no-overflow) 1 wit inspect .74   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 2.1  false(no-overflow) 1 wit inspect 4.0  260 true -32 wit inspect 4.4   230   true -32 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 7.0   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.3   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.4   230   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 .17  12 2.3  false(no-overflow) 1 wit inspect 3.3  270 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .64   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.0  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 1.8  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 5.7   300   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c false(no-overflow) 1 wit inspect .17  12 1.9  false(no-overflow) 1 wit inspect 3.2  270 true -32 wit inspect 5.8   290   true -32 wit inspect .61   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c false(no-overflow) 1 wit inspect .21  12 2.0  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 6.4   300   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.3   220   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 .16  12 2.2  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 2.3  260 true -32 wit inspect 4.7   210   false(no-overflow) 1 wit inspect .60   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 3.6  260 true -32 wit inspect 4.4   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 2.4  260 true -32 wit inspect 4.2   220   false(no-overflow) 1 wit inspect .58   18    - wit inspect
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.4  false(no-overflow) 1 wit inspect 3.8  260 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 4.3  270 true -32 wit inspect 5.0   230   timeout 0 wit inspect 96      18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c unknown 0 wit inspect 2.4   4300 25    error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.6  false(no-overflow) 1 wit inspect 3.3  270 true -32 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.7  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .68   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 7.0   230   false(no-overflow) 1 wit inspect .63   19    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 2.7  270 true -32 wit inspect 5.0   220   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  timeout 0 wit inspect 91    970 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.6  false(no-overflow) 1 wit inspect 3.1  270 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .67   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.8  false(no-overflow) 1 wit inspect 2.9  270 true -32 wit inspect 4.6   220   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.8  false(no-overflow) 1 wit inspect 2.8  260 true -32 wit inspect 4.0   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.3  260 true -32 wit inspect 4.3   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 .16  12 1.9  false(no-overflow) 1 wit inspect 2.4  270 true -32 wit inspect 4.4   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 2.0  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 4.4   220   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.7  false(no-overflow) 1 wit inspect 2.9  270 true -32 wit inspect 4.2   220   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.0  false(no-overflow) 1 wit inspect 3.8  260 true -32 wit inspect 6.8   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.8  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 4.2   210   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 .19  12 1.9  false(no-overflow) 1 wit inspect 2.4  270 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .59   18    - wit inspect
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.9  false(no-overflow) 1 wit inspect 3.6  270 true -32 wit inspect 4.5   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 2.1  false(no-overflow) 1 wit inspect 2.4  260 true -32 wit inspect 4.8   230   error (2) 0 wit inspect .60   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c false(no-overflow) 1 wit inspect .21  12 2.0  false(no-overflow) 1 wit inspect 3.5  260 true -32 wit inspect 4.5   210   error (2) 0 wit inspect .63   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 2.0  false(no-overflow) 1 wit inspect 3.9  260 true -32 wit inspect 4.6   220   error (2) 0 wit inspect .62   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.9  false(no-overflow) 1 wit inspect 3.2  260 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.1  false(no-overflow) 1 wit inspect 3.7  270 true -32 wit inspect 6.7   210   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/cstrncmp_false-no-overflow.c false(no-overflow) 1 wit inspect .24  13 2.6  false(no-overflow) 1 wit inspect 4.4  310 true -32 wit inspect 5.9   260   true -32 wit inspect .59   18    - wit inspect
termination-crafted-lit/gcd1_false-no-overflow.c false(no-overflow) 1 wit inspect .20  12 2.2  false(no-overflow) 1 wit inspect 3.1  250 true -32 wit inspect 4.7   230   error (2) 0 wit inspect .64   18    - wit inspect
termination-crafted-lit/joey_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 3.7  260 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .63   18    - wit inspect
termination-crafted-lit/min_rf_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.4  260 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     4000 9000    - 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 timeout (timeout) 0 wit inspect 900     360 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .15  11 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   270  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     210 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     350 8700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     1900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .045 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     4300 11000    - 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 timeout (timeout) 0 wit inspect 900     3200 8000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     200 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     1800 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     31 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     320 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     68 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     210 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     66 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     65 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     430 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     170 11000    - 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 timeout (timeout) 0 wit inspect 900     130 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .14  11 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1   260  
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     4200 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3100 7200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .037 4.8
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c true 2 wit inspect .13  11 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     230 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     210 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3900 11000    - 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 timeout (timeout) 0 wit inspect 900     3400 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3800 8000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     23 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     81 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     51 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .17  11 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 160     3500  
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3900 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 12000    - 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 timeout (timeout) 0 wit inspect 900     120 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .043 4.9
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     250 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     75 12000    - 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 timeout (timeout) 0 wit inspect 900     67 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     230 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     210 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     45 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     240 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     160 12000    - 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 timeout (timeout) 0 wit inspect 900     44 11000    - 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 timeout (timeout) 0 wit inspect 900     40 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .15  11 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   250  
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 11000    - 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 timeout (timeout) 0 wit inspect 900     240 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     680 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3900 8100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c true 2 wit inspect .16  12 2.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   260  
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     190 11000    - 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 timeout (timeout) 0 wit inspect 900     210 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3700 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     15000 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/aviad_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     330 8500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c unknown 0 wit inspect .22  13 2.3  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c unknown 0 wit inspect .22  13 2.6  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 0 wit inspect .18  12 2.1  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c unknown 0 wit inspect .22  13 2.0  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c unknown 0 wit inspect .22  13 2.4  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect .19  12 2.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     420  
termination-crafted-lit/strchr_true-no-overflow_true-termination.c unknown 0 wit inspect .19  12 2.2  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/Addition01_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 2.0  false(no-overflow) 1 wit inspect 3.5  270 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-numeric/Avg_true_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.7  false(no-overflow) 1 wit inspect 3.3  260 false(no-overflow) 1 wit inspect 7.5   230   error (2) 0 wit inspect .62   18    - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect .24  12 3.1  timeout 0 wit inspect 92    1100 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
termination-numeric/Et1_true_false-no-overflow.c false(no-overflow) 1 wit inspect .18  12 1.7  false(no-overflow) 1 wit inspect 3.0  260 false(no-overflow) 1 wit inspect 5.6   230   false(no-overflow) 1 wit inspect .75   18    - wit inspect
termination-numeric/Et2_true_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.8  false(no-overflow) 1 wit inspect 3.1  280 false(no-overflow) 1 wit inspect 4.9   230   true -32 wit inspect .60   18    - wit inspect
termination-numeric/Et3_true_false-no-overflow.c false(no-overflow) 1 wit inspect .16  12 1.9  false(no-overflow) 1 wit inspect 3.1  260 false(no-overflow) 1 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .66   18    - wit inspect
termination-numeric/Et4_true_false-no-overflow.c false(no-overflow) 1 wit inspect .19  12 1.7  false(no-overflow) 1 wit inspect 3.4  260 false(no-overflow) 1 wit inspect 5.3   230   true -32 wit inspect .61   18    - wit inspect
termination-numeric/MultCommutative_false-no-overflow.c false(no-overflow) 1 wit inspect .27  12 2.8  timeout 0 wit inspect 91    660 true -32 wit inspect 5.1   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c false(no-overflow) 1 wit inspect 12     39 160    timeout 0 wit inspect 91    940 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .65   18    - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     2000 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     300 14000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     250 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     230 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 1 wit inspect 20     170 290    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     490  
termination-numeric/Parts_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     3200 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .032 4.8
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     350 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     49 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .31  12 4.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 68     1000  
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 1 wit inspect .65  16 7.7  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     500 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     480 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (timeout) 0 wit inspect 900     1800 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 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 195 87000   110000 1100000 158 145 1000 44000 158 -4337 750 34000 158 -485 200 2800 122 42 2300 13000
    correct results 172 193 42   2100 490 145 145 490 38000 15 15 81 3500 123 123 85 2300 21 42 330 9200
        correct true 21 42 3.3 230 36 0 0 0 21 42 330 9200
        correct false 151 151 39   1800 450 145 145 490 38000 15 15 81 3500 123 123 85 2300 0
    correct-unconfimed results 2 2 21   180 300 0 0 0 0
        correct-unconfirmed true 2 2 21   180 300 0 0 0 0
        correct-unconfirmed false 0 0 0 0 0
    incorrect results 0 0 136 -4352 670 31000 19 -608 12 350 0
        incorrect true 0 0 136 -4352 670 31000 19 -608 12 350 0
        incorrect false 0 0 0 0 0
score (280 tasks, max score: 402) 195 145 -4337 -485 42
Run set symbiotic.sv-comp18.NoOverflows-BitVectors cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.NoOverflows-BitVectors uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.NoOverflows-BitVectors