Tool 2LS 0.6.0 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-12-01 11:41:06 CET 2017-12-01 17:31:39 CET 2017-12-01 17:38:09 CET
Run set 2ls.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Termination-MainControlFlow
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-12-01_1141.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/2ls.2017-12-01_1141.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 false(termination) 1 wit inspect 6.9  220 75    unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.5   250  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c false(termination) 1 wit inspect 7.0  220 75    unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 5.8   250  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .26 44 1.3  unknown 0 wit inspect 2.3  260 false(termination) 1 wit inspect 5.0   260  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .23 44 .98 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .55 58 5.0  error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .019 5.0
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .23 45 1.6  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 5.0   260  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .24 44 1.4  unknown 0 wit inspect 2.3  170 false(termination) 1 wit inspect 5.0   260  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .23 43 1.2  error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
termination-crafted/Mysore_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3100 9500    error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .17 44 1.2  error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.9
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .24 44 .98 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8
termination-crafted/NonTermination3_false-termination_false-valid-deref.c false(termination) 1 wit inspect .27 50 1.5  unknown 0 wit inspect 3.2  260 false(termination) 1 wit inspect 6.0   260  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c false(termination) 1 wit inspect .30 49 1.6  unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 6.0   260  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .24 44 1.1  unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 5.2   260  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c error (5) 0 wit inspect .22 44 1.1  error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .22 45 1.2  false(termination) 1 wit inspect 3.4  260 false(termination) 1 wit inspect 4.9   270  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 0 wit inspect .22 43 1.3  error 0 wit inspect 2.1  160 true -32 wit inspect 4.2   210  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    1700 11000    - wit inspect - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 1.2  100 8.8  - wit inspect - wit inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    300 10000    - wit inspect - wit inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .20 44 1.5  - wit inspect - wit inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 1.3  340 14    - wit inspect - wit inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 1.8  360 18    - wit inspect - wit inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .26 45 1.2  - wit inspect - wit inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    1900 11000    - wit inspect - wit inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3800 7900    - wit inspect - wit inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    4000 9100    - wit inspect - wit inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2100 9700    - wit inspect - wit inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2100 9300    - wit inspect - wit inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3100 8800    - wit inspect - wit inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .64 62 5.2  - wit inspect - wit inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    640 7600    - wit inspect - wit inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    660 9100    - wit inspect - wit inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 54    15000 620    - wit inspect - wit inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c error (134) 0 wit inspect .37 46 2.4  - wit inspect - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3000 9600    - wit inspect - wit inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .31 49 2.0  - wit inspect - wit inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .22 44 1.2  - wit inspect - wit inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2900 10000    - wit inspect - wit inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .24 44 1.0  - wit inspect - wit inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3000 11000    - wit inspect - wit inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .23 43 1.0  - wit inspect - wit inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .21 43 1.2  - wit inspect - wit inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .24 43 1.2  - wit inspect - wit inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .19 43 1.3  - wit inspect - wit inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .33 54 2.7  - wit inspect - wit inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .25 49 1.7  - wit inspect - wit inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    250 11000    - wit inspect - wit inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    4800 9500    - wit inspect - wit inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    4000 11000    - wit inspect - wit inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c error (5) 0 wit inspect .22 43 1.0  - wit inspect - wit inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    3000 11000    - wit inspect - wit inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true 2 wit inspect .35 50 2.4  - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect .48 51 3.1  - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 wit inspect .49 49 2.4  - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true 2 wit inspect .47 49 2.3  - wit inspect - wit inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    190 10000    - wit inspect - wit inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2700 9300    - wit inspect - wit inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2900 11000    - wit inspect - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    2900 8700    - wit inspect - wit inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .29 47 1.8  - wit inspect - wit inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 40    15000 350    - wit inspect - wit inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true 2 wit inspect .45 51 3.7  - wit inspect - wit inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900    280 10000    - wit inspect - wit inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .27 48 1.9  - wit inspect - wit inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .42 59 3.3  - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) 1 wit inspect .25 47 1.2  unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 4.9   260  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) 1 wit inspect .25 44 1.3  unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 5.6   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) 1 wit inspect .22 46 1.5  unknown 0 wit inspect 3.7  270 false(termination) 1 wit inspect 7.1   310  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) 1 wit inspect .23 44 1.4  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 6.3   260  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) 1 wit inspect .27 44 1.3  unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 4.9   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2900 4500    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect .42 54 2.6  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .31 48 1.4  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 wit inspect .39 59 3.2  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 0 wit inspect 900    5500 4200    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 0 wit inspect 900    1800 5600    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 wit inspect .30 53 2.2  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect .49 62 4.6  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect .47 54 3.2  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect .42 53 3.0  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect .33 47 2.6  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect .30 55 2.1  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect .54 73 4.5  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect .44 52 2.8  - wit inspect - wit inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 2 wit inspect .68 64 5.2  - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    260 10000    - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .46 59 3.1  - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2300 4700    - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2300 9900    - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .29 48 1.8  - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 wit inspect .42 57 2.5  - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900    3600 11000    - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect .49 64 4.2  - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect .31 51 1.8  - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect .29 51 1.9  - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .42 55 3.1  - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect .62 59 5.5  - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect .79 61 6.9  - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 0 wit inspect 900    320 8800    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2100 11000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 0 wit inspect 900    220 10000    - wit inspect - wit inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c timeout 0 wit inspect 900    2700 11000    - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    1600 7000    - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect .27 48 1.9  - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2700 10000    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect .26 47 2.1  - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2100 11000    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect .36 53 2.6  - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect .26 45 1.3  - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2300 9000    - wit inspect - wit inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    250 11000    - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (5) 0 wit inspect .18 43 1.2  - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (5) 0 wit inspect .22 43 1.2  - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect .24 46 1.7  - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .32 51 1.6  - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .29 50 1.6  - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900    6400 5100    - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .29 47 1.6  - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .37 58 3.0  - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect .48 60 3.3  - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect 1.9  200 18    - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .47 62 3.2  - wit inspect - wit inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900    670 6600    - wit inspect - wit inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect .51 67 3.9  - wit inspect - wit inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c error (134) 0 wit inspect .34 46 2.6  - wit inspect - wit inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c error (134) 0 wit inspect .37 46 2.1  - wit inspect - wit inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c error (134) 0 wit inspect .36 46 2.0  - wit inspect - wit inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c error (134) 0 wit inspect .41 46 2.0  - wit inspect - wit inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c error (134) 0 wit inspect .39 46 2.0  - wit inspect - wit inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect .36 53 2.4  - wit inspect - wit inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c error (134) 0 wit inspect .38 46 2.4  - wit inspect - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (5) 0 wit inspect .18 44 1.4  - wit inspect - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c error (5) 0 wit inspect .21 44 1.3  - wit inspect - wit inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (5) 0 wit inspect .23 44 1.2  - wit inspect - wit inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (5) 0 wit inspect .18 44 1.6  - wit inspect - wit inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (5) 0 wit inspect .23 44 1.0  - wit inspect - wit inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (5) 0 wit inspect .17 44 1.3  - wit inspect - wit inspect
termination-numeric/Parts_true-termination_true-no-overflow.c error (5) 0 wit inspect .20 44 1.1  - wit inspect - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (5) 0 wit inspect .18 43 1.1  - wit inspect - wit inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (5) 0 wit inspect .20 43 1.4  - wit inspect - wit inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c error (5) 0 wit inspect .21 44 1.1  - wit inspect - wit inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .33 56 2.6  - wit inspect - wit inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (5) 0 wit inspect .21 43 .97 - wit inspect - wit inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (5) 0 wit inspect .21 43 1.1  - wit inspect - wit inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (5) 0 wit inspect .24 44 1.2  - wit inspect - wit inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900    53 10000    - wit inspect - wit inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2400 5700    - wit inspect - wit inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c true 2 wit inspect .28 55 2.3  - wit inspect - wit inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c true 2 wit inspect .74 59 6.4  - wit inspect - wit inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c true 2 wit inspect .73 60 7.3  - wit inspect - wit inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c timeout 0 wit inspect 900    3500 11000    - wit inspect - wit inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c out of memory 0 wit inspect 270    15000 1700    - wit inspect - wit inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 wit inspect .62 88 6.8  - wit inspect - wit inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c true 2 wit inspect .34 51 1.9  - wit inspect - wit inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .22 46 1.4  - wit inspect - wit inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c timeout 0 wit inspect 900    1700 7800    - wit inspect - wit inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 wit inspect .33 60 2.9  - wit inspect - wit inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true 2 wit inspect .25 53 1.6  - wit inspect - wit inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 wit inspect .41 57 3.1  - wit inspect - wit inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 wit inspect .22 45 1.3  - wit inspect - wit inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 wit inspect .33 51 1.8  - wit inspect - wit inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 wit inspect .47 60 4.4  - wit inspect - wit inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 wit inspect .50 54 3.7  - wit inspect - wit inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 wit inspect .29 56 2.5  - wit inspect - wit inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 wit inspect .40 54 3.2  - wit inspect - wit inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 wit inspect .24 47 1.9  - wit inspect - wit inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true 2 wit inspect .28 49 1.7  - wit inspect - wit inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true 2 wit inspect .39 58 2.8  - wit inspect - wit inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true 2 wit inspect .27 47 1.3  - wit inspect - wit inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 wit inspect .29 51 1.9  - wit inspect - wit inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true 2 wit inspect .34 50 1.7  - wit inspect - wit inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true 2 wit inspect .42 59 3.4  - wit inspect - wit inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true 2 wit inspect .69 65 6.2  - wit inspect - wit inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 wit inspect .28 51 2.6  - wit inspect - wit inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 wit inspect .27 48 1.6  - wit inspect - wit inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 wit inspect .40 59 3.5  - wit inspect - wit inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 wit inspect .21 45 1.1  - wit inspect - wit inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 wit inspect .25 47 1.3  - wit inspect - wit inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c true 2 wit inspect .26 47 1.4  - wit inspect - wit inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 wit inspect .27 49 2.2  - wit inspect - wit inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c true 2 wit inspect .27 49 1.5  - wit inspect - wit inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c true 2 wit inspect .27 46 1.4  - wit inspect - wit inspect
termination-restricted-15/a.10_true-termination.c true 2 wit inspect .26 51 1.8  - wit inspect - wit inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 wit inspect .25 47 1.6  - wit inspect - wit inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c true 2 wit inspect .24 50 1.7  - wit inspect - wit inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c true 2 wit inspect .22 47 1.4  - wit inspect - wit inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c true 2 wit inspect .22 45 1.2  - wit inspect - wit inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c true 2 wit inspect .42 57 2.9  - wit inspect - wit inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 wit inspect .38 54 2.4  - wit inspect - wit inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c true 2 wit inspect .29 53 2.1  - wit inspect - wit inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 wit inspect .29 51 2.3  - wit inspect - wit inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900    2300 8800    - wit inspect - wit inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true 2 wit inspect .40 58 2.5  - wit inspect - wit inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c true 2 wit inspect .32 51 2.7  - wit inspect - wit inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c true 2 wit inspect .38 51 2.2  - wit inspect - wit inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c true 2 wit inspect .34 53 2.5  - wit inspect - wit inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c true 2 wit inspect .38 49 2.1  - wit inspect - wit inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 wit inspect .94 91 8.8  - wit inspect - wit inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 wit inspect .51 55 4.0  - wit inspect - wit inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 wit inspect .32 56 2.3  - wit inspect - wit inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 wit inspect .39 55 2.7  - wit inspect - wit inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 wit inspect .55 66 4.6  - wit inspect - wit inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c out of memory 0 wit inspect 140    15000 1500    - wit inspect - wit inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true 2 wit inspect .39 61 2.5  - wit inspect - wit inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c true 2 wit inspect .39 59 3.4  - wit inspect - wit inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c true 2 wit inspect .30 49 1.5  - wit inspect - wit inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c true 2 wit inspect .61 63 4.4  - wit inspect - wit inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 wit inspect .40 57 2.8  - wit inspect - wit inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c true 2 wit inspect .36 58 2.1  - wit inspect - wit inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c true 2 wit inspect .29 53 1.9  - wit inspect - wit inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c true 2 wit inspect .34 54 2.0  - wit inspect - wit inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 wit inspect .35 54 2.3  - wit inspect - wit inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 wit inspect .38 53 2.5  - wit inspect - wit inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 wit inspect .57 75 4.2  - wit inspect - wit inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 wit inspect .52 61 3.6  - wit inspect - wit inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect .29 47 1.4  unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 8.2   300  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) 1 wit inspect .27 44 1.3  unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.0   260  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) 1 wit inspect .19 46 1.5  unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 5.1   260  
termination-restricted-15/Ex02_false-termination_true-no-overflow.c false(termination) 1 wit inspect .20 44 1.2  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 4.9   270  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) 1 wit inspect .26 44 1.2  unknown 0 wit inspect 3.0  250 false(termination) 1 wit inspect 5.6   260  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 0 wit inspect .19 44 1.4  error 0 wit inspect 2.2  160 true -32 wit inspect 4.1   210  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) 1 wit inspect .26 44 1.1  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 7.3   290  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) 1 wit inspect .26 44 1.2  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 9.2   330  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) 0 wit inspect .38 55 2.9  unknown 0 wit inspect 4.1  270 true -32 wit inspect 14     510  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c false(termination) 1 wit inspect .28 47 2.5  unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 10     330  
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) 1 wit inspect .24 45 1.8  unknown 0 wit inspect 4.2  260 false(termination) 1 wit inspect 5.2   260  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c false(termination) 1 wit inspect .22 46 1.8  unknown 0 wit inspect 2.4  260 false(termination) 1 wit inspect 5.5   270  
termination-restricted-15/GCD_false-termination_true-no-overflow.c false(termination) 1 wit inspect .29 46 1.4  unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 6.8   280  
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) 0 wit inspect .26 44 1.2  error 0 wit inspect 2.2  170 true -32 wit inspect 4.1   210  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) 1 wit inspect .27 44 1.3  unknown 0 wit inspect 3.8  260 false(termination) 1 wit inspect 5.2   260  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) 1 wit inspect .25 44 1.2  unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.1   260  
termination-restricted-15/NO_01_false-termination_true-no-overflow.c false(termination) 1 wit inspect .27 47 1.3  unknown 0 wit inspect 3.2  260 false(termination) 1 wit inspect 5.2   260  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) 1 wit inspect .23 46 1.1  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 5.3   270  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) 1 wit inspect .21 45 1.4  unknown 0 wit inspect 3.2  260 false(termination) 1 wit inspect 5.1   260  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) 1 wit inspect .41 58 3.5  unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 5.6   260  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c false(termination) 1 wit inspect .81 75 7.1  unknown 0 wit inspect 19    540 false(termination) 1 wit inspect 79     3000  
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) 1 wit inspect .22 43 1.1  unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 4.7   260  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c false(termination) 0 wit inspect .41 47 3.7  unknown 0 wit inspect 7.2  310 timeout (false(termination)) 0 wit inspect 93     3000  
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) 1 wit inspect .24 44 1.3  unknown 0 wit inspect 2.5  260 false(termination) 1 wit inspect 6.3   260  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c false(termination) 0 wit inspect .24 45 1.4  unknown 0 wit inspect 3.3  260 unknown 0 wit inspect 19     500  
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c false(termination) 0 wit inspect 47    370 330    unknown 0 wit inspect 7.0  320 timeout 0 wit inspect 96     4800  
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c false(termination) 1 wit inspect .57 56 5.0  unknown 0 wit inspect 3.2  270 false(termination) 1 wit inspect 18     600  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) 1 wit inspect .21 45 1.5  unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 13     500  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c false(termination) 0 wit inspect .24 46 1.5  unknown 0 wit inspect 2.3  260 unknown 0 wit inspect 28     550  
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) 1 wit inspect .23 45 1.4  unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c false(termination) 0 wit inspect .47 59 3.8  unknown 0 wit inspect 4.0  270 true -32 wit inspect 14     590  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c false(termination) 0 wit inspect .46 56 3.6  unknown 0 wit inspect 4.0  270 true -32 wit inspect 16     570  
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) 1 wit inspect .22 44 1.2  unknown 0 wit inspect 3.1  260 false(termination) 1 wit inspect 4.9   260  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) 1 wit inspect .21 44 1.3  unknown 0 wit inspect 3.1  250 false(termination) 1 wit inspect 5.4   250  
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 269 42000 170000 430000 56 1 190   13000 56 -153 610 25000
    correct results 154 269 73 9200 580 1 1 3.4 260 39 39 320 14000
        correct true 115 230 49 7000 370 0 0
        correct false 39 39 24 2200 210 1 1 3.4 260 39 39 320 14000
    correct-unconfimed results 10 0 49 810 360 0 0
        correct-unconfirmed true 0 0 0
        correct-unconfirmed false 10 0 49 810 360 0 0
    incorrect results 0 0 6 -192 57 2300
        incorrect true 0 0 6 -192 57 2300
        incorrect false 0 0 0
score (250 tasks, max score: 444) 269 1 -153
Run set 2ls.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.Termination-MainControlFlow