Tool 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 12:27:04 CET 2017-12-01 18:45:24 CET 2017-12-01 18:50:14 CET
Run set cpa-seq.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainControlFlow
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-12-01_1227.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/cpa-seq.2017-12-01_1227.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 timeout 0 wit inspect 910   4600 12000 error (invalid witness file) 0 wit inspect .83 41 error (2) 0 wit inspect .019 5.0
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout 0 wit inspect 900   4500 12000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.9
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 2.8 270 26 false(termination) 1 wit inspect 3.4  260 false(termination) 1 wit inspect 4.9   260  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.6 270 21 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 5.6 420 43 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.0 270 26 false(termination) 1 wit inspect 2.3  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 2.7 270 23 false(termination) 1 wit inspect 4.3  260 false(termination) 1 wit inspect 5.2   250  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.7 290 27 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
termination-crafted/Mysore_false-termination_true-valid-memsafety.c unknown 0 wit inspect 8.5 560 67 error (invalid witness file) 0 wit inspect .76 42 error (2) 0 wit inspect .048 4.9
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.5 260 20 error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .021 5.0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.8 290 24 error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .019 4.9
termination-crafted/NonTermination3_false-termination_false-valid-deref.c unknown 0 wit inspect 720   4400 10000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c unknown 0 wit inspect 710   4400 9800 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 2.8 270 25 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 4.8   260  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.6 270 22 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .036 4.9
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 2.9 270 30 false(termination) 1 wit inspect 3.6  260 false(termination) 1 wit inspect 5.0   260  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 2.7 280 24 false(termination) 1 wit inspect 2.2  260 true -32 wit inspect 4.3   220  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c true 2 wit inspect 50   490 520 - wit inspect - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.6 260 20 - wit inspect - wit inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 370   15000 3800 - wit inspect - wit inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 340   15000 3800 - wit inspect - wit inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.3 270 30 - wit inspect - wit inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 wit inspect 3.2 280 26 - wit inspect - wit inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   800 11000 - wit inspect - wit inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.1 440 56 - wit inspect - wit inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.0 300 33 - wit inspect - wit inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.5 280 28 - wit inspect - wit inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1200 9400 - wit inspect - wit inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.7 280 35 - wit inspect - wit inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 420 44 - wit inspect - wit inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c true 2 wit inspect 5.2 330 46 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4400 11000 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c unknown 0 wit inspect 5.1 360 41 - wit inspect - wit inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   640 9800 - wit inspect - wit inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.9 290 23 - wit inspect - wit inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 390 49 - wit inspect - wit inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.8 290 23 - wit inspect - wit inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c true 2 wit inspect 5.9 430 45 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.8 290 23 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.8 290 24 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.9 290 26 - wit inspect - wit inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.8 290 20 - wit inspect - wit inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.4 290 38 - wit inspect - wit inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.5 280 37 - wit inspect - wit inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 4.9 320 39 - wit inspect - wit inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c true 2 wit inspect 5.0 310 46 - wit inspect - wit inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c true 2 wit inspect 6.9 460 54 - wit inspect - wit inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c error (recursion) 0 wit inspect 2.5 270 23 - wit inspect - wit inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 wit inspect 11   990 100 - wit inspect - wit inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true 2 wit inspect 4.3 300 38 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 4.8 320 40 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 wit inspect 4.3 310 34 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true 2 wit inspect 3.8 280 32 - wit inspect - wit inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.3 340 44 - wit inspect - wit inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 wit inspect 5.1 310 43 - wit inspect - wit inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c true 2 wit inspect 5.6 350 43 - wit inspect - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c true 2 wit inspect 7.7 490 61 - wit inspect - wit inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.2 280 29 - wit inspect - wit inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 2.5 270 23 - wit inspect - wit inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true 2 wit inspect 4.0 300 35 - wit inspect - wit inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c true 2 wit inspect 21   640 200 - wit inspect - wit inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 67   2200 720 - wit inspect - wit inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.9 280 34 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.0 270 28 false(termination) 1 wit inspect 3.4  260 false(termination) 1 wit inspect 8.9   340  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 25 unknown 0 wit inspect 3.4  270 false(termination) 1 wit inspect 5.1   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.4 280 30 unknown 0 wit inspect 4.8  270 false(termination) 1 wit inspect 7.2   280  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 270 27 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 5.7   260  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 26 false(termination) 1 wit inspect 2.9  260 false(termination) 1 wit inspect 6.9   280  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 43   640 490 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 35 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 67   2200 730 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 wit inspect 3.8 280 34 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 7.3 460 57 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect 7.3 350 60 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 36 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 4.1 290 34 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c unknown 0 wit inspect 7.9 470 66 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 5.5 320 46 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c unknown 0 wit inspect 3.3 280 28 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 7.4 400 63 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 43 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 4.5 300 37 - wit inspect - wit inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 2 wit inspect 5.1 310 45 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c unknown 0 wit inspect 3.3 280 32 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 32   1100 280 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c true 2 wit inspect 18   470 200 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 wit inspect 3.8 290 37 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 67   2200 710 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 wit inspect 4.1 300 38 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c true 2 wit inspect 4.4 290 41 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 34 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 3.7 280 32 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 35 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 4.7 310 46 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 6.2 360 55 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 5.6 310 51 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 4.4 280 35 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 3.8 300 35 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c unknown 0 wit inspect 3.1 270 28 - wit inspect - wit inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c out of memory 0 wit inspect 470   15000 5800 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 8.4 480 69 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 3.5 270 34 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 3.9 290 28 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 3.9 280 30 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 wit inspect 4.3 340 40 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 3.4 270 31 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect 4.0 290 33 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   5200 13000 - wit inspect - wit inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900   6300 7900 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.6 270 22 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 270 23 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 31 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 4.2 290 37 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c unknown 0 wit inspect 4.3 300 38 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 4.6 320 39 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 3.3 280 29 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 4.3 280 39 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 4.9 310 42 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c out of memory 0 wit inspect 470   15000 5300 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 10   470 85 - wit inspect - wit inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 5.6 330 47 - wit inspect - wit inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c unknown 0 wit inspect 21   880 160 - wit inspect - wit inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3000 13000 - wit inspect - wit inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 0 wit inspect 28   1400 260 - wit inspect - wit inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3700 11000 - wit inspect - wit inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3500 12000 - wit inspect - wit inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c out of memory 0 wit inspect 480   15000 5500 - wit inspect - wit inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c unknown 0 wit inspect 27   940 190 - wit inspect - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.6 270 24 - wit inspect - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c error (recursion) 0 wit inspect 2.7 270 22 - wit inspect - wit inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.8 260 23 - wit inspect - wit inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 260 23 - wit inspect - wit inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 260 24 - wit inspect - wit inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 260 24 - wit inspect - wit inspect
termination-numeric/Parts_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.7 270 21 - wit inspect - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c error (recursion) 0 wit inspect 2.8 290 25 - wit inspect - wit inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.6 270 22 - wit inspect - wit inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.6 270 22 - wit inspect - wit inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c unknown 0 wit inspect 19   870 160 - wit inspect - wit inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 260 23 - wit inspect - wit inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 260 20 - wit inspect - wit inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (recursion) 0 wit inspect 2.5 270 24 - wit inspect - wit inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900   4300 11000 - wit inspect - wit inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 41 - wit inspect - wit inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c unknown 0 wit inspect 3.9 290 34 - wit inspect - wit inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c unknown 0 wit inspect 4.0 290 37 - wit inspect - wit inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c unknown 0 wit inspect 3.8 290 33 - wit inspect - wit inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c true 2 wit inspect 4.9 300 43 - wit inspect - wit inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 40 - wit inspect - wit inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c timeout 0 wit inspect 900   3500 11000 - wit inspect - wit inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 32 - wit inspect - wit inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c true 2 wit inspect 6.3 360 56 - wit inspect - wit inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 wit inspect 21   670 180 - wit inspect - wit inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 34 - wit inspect - wit inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 wit inspect 4.5 310 40 - wit inspect - wit inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 34 - wit inspect - wit inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 wit inspect 4.0 290 34 - wit inspect - wit inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 wit inspect 5.0 310 47 - wit inspect - wit inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 wit inspect 5.1 320 43 - wit inspect - wit inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 wit inspect 3.8 280 36 - wit inspect - wit inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 wit inspect 4.0 280 35 - wit inspect - wit inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 wit inspect 3.4 270 32 - wit inspect - wit inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true 2 wit inspect 3.8 280 33 - wit inspect - wit inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c unknown 0 wit inspect 3.5 280 28 - wit inspect - wit inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 30 - wit inspect - wit inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 30 - wit inspect - wit inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true 2 wit inspect 4.2 290 35 - wit inspect - wit inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true 2 wit inspect 3.7 280 31 - wit inspect - wit inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true 2 wit inspect 4.6 320 38 - wit inspect - wit inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 wit inspect 90   3100 940 - wit inspect - wit inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 wit inspect 3.4 270 29 - wit inspect - wit inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 wit inspect 4.5 280 40 - wit inspect - wit inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 29 - wit inspect - wit inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 wit inspect 3.8 300 36 - wit inspect - wit inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c true 2 wit inspect 4.3 300 38 - wit inspect - wit inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 wit inspect 3.8 290 37 - wit inspect - wit inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c true 2 wit inspect 4.0 290 30 - wit inspect - wit inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 3.4 280 30 - wit inspect - wit inspect
termination-restricted-15/a.10_true-termination.c true 2 wit inspect 4.1 290 36 - wit inspect - wit inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 28 - wit inspect - wit inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c true 2 wit inspect 3.6 270 33 - wit inspect - wit inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 3.2 280 28 - wit inspect - wit inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c unknown 0 wit inspect 3.2 270 32 - wit inspect - wit inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c unknown 0 wit inspect 3.7 290 32 - wit inspect - wit inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 wit inspect 4.1 300 32 - wit inspect - wit inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c true 2 wit inspect 4.1 290 34 - wit inspect - wit inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 wit inspect 3.7 280 36 - wit inspect - wit inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c true 2 wit inspect 4.6 310 42 - wit inspect - wit inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true 2 wit inspect 3.9 280 30 - wit inspect - wit inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c true 2 wit inspect 4.7 310 43 - wit inspect - wit inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c true 2 wit inspect 5.1 320 47 - wit inspect - wit inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c true 2 wit inspect 4.1 290 37 - wit inspect - wit inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c true 2 wit inspect 4.3 280 39 - wit inspect - wit inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 42 - wit inspect - wit inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 wit inspect 4.7 290 44 - wit inspect - wit inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 wit inspect 4.1 280 35 - wit inspect - wit inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 wit inspect 4.2 280 38 - wit inspect - wit inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 wit inspect 5.9 320 46 - wit inspect - wit inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c true 2 wit inspect 110   6600 1300 - wit inspect - wit inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true 2 wit inspect 6.3 350 51 - wit inspect - wit inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c true 2 wit inspect 4.7 320 40 - wit inspect - wit inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 48 - wit inspect - wit inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c true 2 wit inspect 4.1 310 32 - wit inspect - wit inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 wit inspect 4.5 300 40 - wit inspect - wit inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c unknown 0 wit inspect 4.3 300 32 - wit inspect - wit inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c unknown 0 wit inspect 4.6 360 39 - wit inspect - wit inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c unknown 0 wit inspect 3.7 280 33 - wit inspect - wit inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 wit inspect 3.5 280 30 - wit inspect - wit inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 wit inspect 32   960 360 - wit inspect - wit inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 wit inspect 11   480 100 - wit inspect - wit inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 wit inspect 100   3400 1100 - wit inspect - wit inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.3 290 40 timeout 0 wit inspect 91    300 false(termination) 1 wit inspect 7.7   290  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 280 26 false(termination) 1 wit inspect 4.5  270 false(termination) 1 wit inspect 6.5   270  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 270 24 false(termination) 1 wit inspect 4.4  260 false(termination) 1 wit inspect 5.3   270  
termination-restricted-15/Ex02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 270 26 false(termination) 1 wit inspect 3.5  260 false(termination) 1 wit inspect 5.6   260  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 280 28 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 5.0   260  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.7 270 25 false(termination) 1 wit inspect 3.0  260 true -32 wit inspect 4.1   210  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.0 290 35 false(termination) 1 wit inspect 3.5  270 false(termination) 1 wit inspect 7.1   290  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 280 36 false(termination) 1 wit inspect 2.3  260 false(termination) 1 wit inspect 8.6   330  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) 1 wit inspect 240   3900 2900 false(termination) 1 wit inspect 5.4  290 timeout 0 wit inspect 98     5500  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c unknown 0 wit inspect 3.3 290 32 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.8
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.1 270 24 unknown 0 wit inspect 3.3  270 false(termination) 1 wit inspect 4.8   260  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c unknown 0 wit inspect 3.8 280 32 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .024 4.9
termination-restricted-15/GCD_false-termination_true-no-overflow.c unknown 0 wit inspect 3.8 290 32 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 24 false(termination) 1 wit inspect 3.3  260 false(termination) 1 wit inspect 5.6   260  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 25 false(termination) 1 wit inspect 3.5  260 false(termination) 1 wit inspect 6.6   280  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.7 280 26 false(termination) 1 wit inspect 3.4  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 3.1 270 29 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 5.1   270  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 25 false(termination) 1 wit inspect 3.4  260 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.9 280 33 unknown 0 wit inspect 3.4  270 false(termination) 1 wit inspect 5.6   260  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.0 270 29 false(termination) 1 wit inspect 3.7  270 false(termination) 1 wit inspect 5.7   260  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c out of memory 0 wit inspect 510   15000 6500 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 4.8
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.9 270 27 false(termination) 1 wit inspect 4.5  260 false(termination) 1 wit inspect 5.5   270  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c out of memory 0 wit inspect 510   15000 6000 error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .020 4.8
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.9 300 44 false(termination) 1 wit inspect 4.2  260 false(termination) 1 wit inspect 6.8   270  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c unknown 0 wit inspect 6.7 540 57 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c timeout 0 wit inspect 900   520 8300 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 5.0
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c false(termination) 1 wit inspect 840   1400 8600 false(termination) 1 wit inspect 13    410 false(termination) 1 wit inspect 32     2300  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.5 300 47 false(termination) 1 wit inspect 3.5  270 false(termination) 1 wit inspect 24     590  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c unknown 0 wit inspect 280   4400 3200 error (invalid witness file) 0 wit inspect .81 41 error (2) 0 wit inspect .019 4.8
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.0 280 26 false(termination) 1 wit inspect 3.7  260 false(termination) 1 wit inspect 7.5   280  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c unknown 0 wit inspect 6.1 450 47 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c unknown 0 wit inspect 6.2 440 46 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .017 4.9
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 270 29 false(termination) 1 wit inspect 3.3  260 false(termination) 1 wit inspect 5.7   260  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) 1 wit inspect 2.8 270 23 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 4.9   260  
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 291 24000 280000 290000 56 30 230 10000 56 -32 340   17000
    correct results 163 291 2400 75000 25000 30 30 110 8100 32 32 240   11000
        correct true 128 256 1300 61000 12000 0 0
        correct false 35 35 1200 14000 12000 30 30 110 8100 32 32 240   11000
    incorrect results 0 0 2 -64 8.4 430
        incorrect true 0 0 2 -64 8.4 430
        incorrect false 0 0 0
score (250 tasks, max score: 444) 291 30 -32
Run set cpa-seq.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.Termination-MainControlFlow