Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 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-01 15:15:10 CET 2017-12-01 21:58:57 CET 2017-12-01 21:59:47 CET
Run set depthk.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/depthk.2017-12-01_1515.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
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .67 44 false(termination) 1 wit inspect 4.9   230  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c unknown 0 wit inspect 1.2 56 12 error (1) 0 wit inspect .58 45 false(termination) 1 wit inspect 5.0   250  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 15 error (1) 0 wit inspect .61 45 false(termination) 1 wit inspect 4.8   230  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c unknown 0 wit inspect 690   15000 10000 error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 6.0   280  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .44 47 unknown 0 wit inspect 62     510  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 12 error (1) 0 wit inspect .64 45 false(termination) 1 wit inspect 5.1   260  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 55 13 error (1) 0 wit inspect .57 47 false(termination) 1 wit inspect 6.4   260  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 720   15000 8100 error (1) 0 wit inspect .65 46 false(termination) 1 wit inspect 10     410  
termination-crafted/Mysore_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .61 45 unknown 0 wit inspect 41     660  
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 660   15000 8800 error (1) 0 wit inspect .65 47 false(termination) 1 wit inspect 7.5   270  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 730   15000 8400 error (1) 0 wit inspect .60 45 false(termination) 1 wit inspect 20     490  
termination-crafted/NonTermination3_false-termination_false-valid-deref.c unknown 0 wit inspect 1.2 57 14 error (1) 0 wit inspect .45 47 false(termination) 1 wit inspect 5.4   260  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .60 45 false(termination) 1 wit inspect 5.3   260  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 12 error (1) 0 wit inspect .66 45 false(termination) 1 wit inspect 5.1   230  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .64 45 false(termination) 1 wit inspect 5.2   260  
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .60 49 false(termination) 1 wit inspect 5.2   250  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .60 45 false(termination) 1 wit inspect 5.6   230  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 55 15 - wit inspect - wit inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 710   15000 9500 - wit inspect - wit inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 12 - wit inspect - wit inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 58 15 - wit inspect - wit inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 12 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 16 - wit inspect - wit inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 750   15000 9200 - wit inspect - wit inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 710   15000 8600 - wit inspect - wit inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 680   15000 9300 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 630   15000 7700 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 690   15000 8200 - wit inspect - wit inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory (false(no-overflow)) 0 wit inspect 730   15000 8900 - wit inspect - wit inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 710   15000 10000 - wit inspect - wit inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 11 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 17 - wit inspect - wit inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 15 - wit inspect - wit inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 55 14 - wit inspect - wit inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.3 56 13 - wit inspect - wit inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.3 56 17 - wit inspect - wit inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 4.8   250  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 error (1) 0 wit inspect .61 45 false(termination) 1 wit inspect 5.6   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c unknown 0 wit inspect 99   64 1400 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 5.0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 error (1) 0 wit inspect .61 47 false(termination) 1 wit inspect 4.7   230  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 15 error (1) 0 wit inspect .74 45 false(termination) 1 wit inspect 9.3   370  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.7 56 20 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 57 14 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c unknown 0 wit inspect 8.1 240 97 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 56 14 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 57 16 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 16 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 18 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 14 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 57 13 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c unknown 0 wit inspect 1.2 57 15 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 57 16 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 10 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 58 16 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c unknown 0 wit inspect 770   15000 8800 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 620   15000 7400 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 58 15 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 12 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 14 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 18 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 17 - wit inspect - wit inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c unknown 0 wit inspect 2.0 56 23 - wit inspect - wit inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 16 - wit inspect - wit inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c unknown 0 wit inspect 2.0 57 23 - wit inspect - wit inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c unknown 0 wit inspect 2.0 57 24 - wit inspect - wit inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c unknown 0 wit inspect 1.4 56 15 - wit inspect - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 730   15000 9000 - wit inspect - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c unknown 0 wit inspect 14   340 170 - wit inspect - wit inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 56 15 - wit inspect - wit inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 610   15000 8000 - wit inspect - wit inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 12 - wit inspect - wit inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-numeric/Parts_true-termination_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 670   15000 9200 - wit inspect - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c unknown 0 wit inspect 1.3 57 16 - wit inspect - wit inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 - wit inspect - wit inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c unknown 0 wit inspect 570   15000 6300 - wit inspect - wit inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 14 - wit inspect - wit inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 17 - wit inspect - wit inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 57 16 - wit inspect - wit inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 56 15 - wit inspect - wit inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (false(no-overflow)) 0 wit inspect 900   3800 8800 - wit inspect - wit inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.8 57 25 - wit inspect - wit inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.7 56 16 - wit inspect - wit inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 16 - wit inspect - wit inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 56 19 - wit inspect - wit inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 57 16 - wit inspect - wit inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 56 17 - wit inspect - wit inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 - wit inspect - wit inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 57 16 - wit inspect - wit inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 56 15 - wit inspect - wit inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 57 18 - wit inspect - wit inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 14 - wit inspect - wit inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 17 - wit inspect - wit inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 58 14 - wit inspect - wit inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 15 - wit inspect - wit inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 - wit inspect - wit inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 57 14 - wit inspect - wit inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 57 15 - wit inspect - wit inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 - wit inspect - wit inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 - wit inspect - wit inspect
termination-restricted-15/a.10_true-termination.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 58 14 - wit inspect - wit inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 - wit inspect - wit inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 15 - wit inspect - wit inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 12 - wit inspect - wit inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 - wit inspect - wit inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c unknown 0 wit inspect 1.3 56 15 - wit inspect - wit inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 15 - wit inspect - wit inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 14 - wit inspect - wit inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 56 16 - wit inspect - wit inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5 57 17 - wit inspect - wit inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 16 - wit inspect - wit inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 58 17 - wit inspect - wit inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c unknown 0 wit inspect 1.6 56 17 - wit inspect - wit inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 17 - wit inspect - wit inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 16 - wit inspect - wit inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 14 - wit inspect - wit inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 - wit inspect - wit inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 17 - wit inspect - wit inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4 56 18 - wit inspect - wit inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 - wit inspect - wit inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 16 - wit inspect - wit inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 15 - wit inspect - wit inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 - wit inspect - wit inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 15 - wit inspect - wit inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 - wit inspect - wit inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 error (1) 0 wit inspect .61 45 false(termination) 1 wit inspect 7.0   270  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 5.2   240  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 error (1) 0 wit inspect .46 47 false(termination) 1 wit inspect 4.7   230  
termination-restricted-15/Ex02_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 12 error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 5.1   240  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 error (1) 0 wit inspect .59 45 false(termination) 1 wit inspect 4.7   230  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .46 46 false(termination) 1 wit inspect 4.7   250  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 error (1) 0 wit inspect .61 45 false(termination) 1 wit inspect 6.4   260  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 error (1) 0 wit inspect .61 45 false(termination) 1 wit inspect 6.5   270  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .69 47 false(termination) 1 wit inspect 37     700  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 11     420  
termination-restricted-15/Flip_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 error (1) 0 wit inspect .46 47 false(termination) 1 wit inspect 6.3   260  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c unknown 0 wit inspect 1.4 57 16 error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 5.1   260  
termination-restricted-15/GCD_false-termination_true-no-overflow.c unknown 0 wit inspect 1.4 57 18 error (1) 0 wit inspect .62 47 false(termination) 1 wit inspect 5.4   260  
termination-restricted-15/Loop_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .70 45 false(termination) 1 wit inspect 5.2   250  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 8.8   360  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 13 error (1) 0 wit inspect .45 47 false(termination) 1 wit inspect 4.9   230  
termination-restricted-15/NO_01_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .59 45 false(termination) 1 wit inspect 6.3   260  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 14 error (1) 0 wit inspect .58 47 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 15 error (1) 0 wit inspect .66 45 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c unknown 0 wit inspect 1.3 56 14 error (1) 0 wit inspect .71 46 false(termination) 1 wit inspect 23     370  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .62 48 false(termination) 1 wit inspect 75     960  
termination-restricted-15/NO_21_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 13 error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 4.5   230  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 error (1) 0 wit inspect .63 45 false(termination) 1 wit inspect 66     940  
termination-restricted-15/NO_23_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 16 error (1) 0 wit inspect .60 47 false(termination) 1 wit inspect 10     380  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 error (1) 0 wit inspect .62 45 unknown 0 wit inspect 32     440  
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .63 45 timeout 0 wit inspect 96     1600  
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 55 15 error (1) 0 wit inspect .63 45 false(termination) 1 wit inspect 43     750  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 11 error (1) 0 wit inspect .62 45 false(termination) 1 wit inspect 12     510  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 error (1) 0 wit inspect .73 45 unknown 0 wit inspect 34     530  
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 14 error (1) 0 wit inspect .45 46 false(termination) 1 wit inspect 3.6   250  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .63 45 false(termination) 1 wit inspect 40     770  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 12 error (1) 0 wit inspect .60 47 timeout 0 wit inspect 98     3100  
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 56 13 error (1) 0 wit inspect .62 46 false(termination) 1 wit inspect 5.4   230  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c unknown 0 wit inspect 1.2 57 14 error (1) 0 wit inspect .63 45 false(termination) 1 wit inspect 3.4   230  
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
total 250 0 14000 290000 170000 56 0 34 2600 56 49 920 23000
    correct results 0 0 49 49 560 16000
        correct true 0 0 0
        correct false 0 0 49 49 560 16000
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (250 tasks, max score: 444) 0 0 49
Run set depthk.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.Termination-MainControlFlow