Tool ULTIMATE Automizer 0.1.23-3204b741 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-03 12:12:33 CET 2017-12-03 12:33:05 CET 2017-12-03 12:34:35 CET
Run set uautomizer.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainControlFlow
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_1212.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/uautomizer.2017-12-03_1212.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 4.5 250 36 unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 5.3   250  
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c false(termination) 1 wit inspect 4.4 270 36 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.5   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.4 250 34 unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 5.1   250  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 5.5 290 47 unknown 0 wit inspect 2.5  180 false(termination) 1 wit inspect 5.9   270  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect 59   540 670 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.9
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.4 250 37 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 6.5   320  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.7 300 42 false(termination) 1 wit inspect 3.3  260 false(termination) 1 wit inspect 5.9   270  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 0 wit inspect 7.6 360 61 unknown 0 wit inspect 2.5  170 timeout 0 wit inspect 97     4700  
termination-crafted/Mysore_false-termination_true-valid-memsafety.c unknown 0 wit inspect 38   720 410 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .033 4.8
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 5.5 300 43 unknown 0 wit inspect 2.4  170 false(termination) 1 wit inspect 22     620  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 17   500 170 unknown 0 wit inspect 2.3  170 false(termination) 1 wit inspect 9.8   360  
termination-crafted/NonTermination3_false-termination_false-valid-deref.c false(termination) 1 wit inspect 4.7 280 37 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.8   260  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c false(termination) 1 wit inspect 4.6 270 37 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.4   260  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.3 240 35 unknown 0 wit inspect 3.4  270 false(termination) 1 wit inspect 5.1   250  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.6 270 40 unknown 0 wit inspect 2.4  170 false(termination) 1 wit inspect 5.9   250  
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.3 260 41 false(termination) 1 wit inspect 3.2  260 false(termination) 1 wit inspect 5.3   270  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 0 wit inspect 4.4 250 36 timeout 0 wit inspect 96    5200 true -32 wit inspect 4.4   210  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c true 2 wit inspect 5.6 300 48 - wit inspect - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 39   900 400 - wit inspect - wit inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c true 2 wit inspect 18   350 220 - wit inspect - wit inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c timeout 0 wit inspect 910   13000 7300 - wit inspect - wit inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   2100 10000 - wit inspect - wit inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   2400 12000 - wit inspect - wit inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.2 320 47 - wit inspect - wit inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.7 360 49 - wit inspect - wit inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c true 2 wit inspect 17   310 230 - wit inspect - wit inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 16   310 190 - wit inspect - wit inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.4 340 55 - wit inspect - wit inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.0 330 51 - wit inspect - wit inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c unknown 0 wit inspect 77   1500 800 - wit inspect - wit inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.4 300 50 - wit inspect - wit inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c true 2 wit inspect 22   520 190 - wit inspect - wit inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c unknown 0 wit inspect 45   1000 400 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   2400 9600 - wit inspect - wit inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   1100 9600 - wit inspect - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c true 2 wit inspect 22   510 230 - wit inspect - wit inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 12   540 110 - wit inspect - wit inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 49   630 510 - wit inspect - wit inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 6.3 330 54 - wit inspect - wit inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900   13000 5700 - wit inspect - wit inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c true 2 wit inspect 18   340 210 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 38   670 390 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.4 460 72 - wit inspect - wit inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 11   610 97 - wit inspect - wit inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 910   13000 8700 - wit inspect - wit inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 7.3 350 57 - wit inspect - wit inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 300 44 - wit inspect - wit inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 15   490 150 - wit inspect - wit inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c true 2 wit inspect 7.1 370 57 - wit inspect - wit inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c timeout 0 wit inspect 910   9700 7700 - wit inspect - wit inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c true 2 wit inspect 15   370 140 - wit inspect - wit inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 wit inspect 16   380 190 - wit inspect - wit inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true 2 wit inspect 18   400 170 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect 6.8 360 61 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 wit inspect 7.2 350 57 - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true 2 wit inspect 6.8 360 57 - wit inspect - wit inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 23   520 250 - wit inspect - wit inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 wit inspect 6.3 310 62 - wit inspect - wit inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c true 2 wit inspect 25   470 240 - wit inspect - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c true 2 wit inspect 32   520 400 - wit inspect - wit inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.1 290 40 - wit inspect - wit inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 3.9 230 31 - wit inspect - wit inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true 2 wit inspect 5.7 300 46 - wit inspect - wit inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c true 2 wit inspect 20   430 220 - wit inspect - wit inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.2 310 47 - wit inspect - wit inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect 5.6 320 51 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.5 250 36 unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 5.3   260  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.8 280 38 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.3   260  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.5 260 35 unknown 0 wit inspect 2.5  170 false(termination) 1 wit inspect 5.5   260  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.3 240 34 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 4.8   250  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.7 370 61 unknown 0 wit inspect 3.7  270 false(termination) 1 wit inspect 5.2   260  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 23   540 260 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect 6.4 320 53 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect 4.9 300 47 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 43 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 wit inspect 20   440 210 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 wit inspect 21   560 270 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 44 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 42 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 wit inspect 7.1 330 57 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect 7.3 360 60 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 wit inspect 7.2 370 61 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect 9.4 550 75 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect 6.6 340 48 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 wit inspect 7.1 340 52 - wit inspect - wit inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 2 wit inspect 6.1 310 52 - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 10   550 94 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 9.2 430 85 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c true 2 wit inspect 12   530 110 - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 wit inspect 9.4 300 99 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect 5.0 300 39 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 43 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 44 - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 44 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 wit inspect 5.2 310 43 - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 wit inspect 17   300 220 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 7.2 340 57 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 wit inspect 8.0 470 69 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 wit inspect 8.4 540 69 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 wit inspect 7.4 350 69 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 wit inspect 6.8 350 52 - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 wit inspect 7.1 330 59 - wit inspect - wit inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect 7.7 390 57 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 40   680 430 - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 41 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 9.6 290 97 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 5.0 290 40 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 wit inspect 16   840 140 - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 43 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 wit inspect 5.1 310 48 - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 7.9 410 63 - wit inspect - wit inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 57   670 690 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 wit inspect 48   580 560 - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c unknown 0 wit inspect 49   1700 470 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 6.1 300 51 - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect 5.1 310 43 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 20   460 210 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect 4.9 290 36 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 6.7 330 57 - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 wit inspect 7.1 370 60 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 wit inspect 900   2600 12000 - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect 8.1 460 62 - wit inspect - wit inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 wit inspect 9.7 530 79 - wit inspect - wit inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 6.2 330 48 - wit inspect - wit inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 wit inspect 8.9 540 73 - wit inspect - wit inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 wit inspect 110   750 1500 - wit inspect - wit inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 wit inspect 7.5 460 61 - wit inspect - wit inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 wit inspect 19   720 160 - wit inspect - wit inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 wit inspect 18   710 150 - wit inspect - wit inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 44 - wit inspect - wit inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 wit inspect 8.7 530 64 - wit inspect - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c timeout 0 wit inspect 910   13000 5600 - wit inspect - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900   2800 11000 - wit inspect - wit inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 2 wit inspect 7.7 430 70 - wit inspect - wit inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 wit inspect 900   13000 9800 - wit inspect - wit inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect 5.4 310 42 - wit inspect - wit inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c unknown 0 wit inspect 71   670 740 - wit inspect - wit inspect
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900   8400 9600 - wit inspect - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c true 2 wit inspect 5.6 310 48 - wit inspect - wit inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c true 2 wit inspect 19   380 230 - wit inspect - wit inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 wit inspect 9.7 440 90 - wit inspect - wit inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 5.8 320 45 - wit inspect - wit inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2 wit inspect 6.9 370 60 - wit inspect - wit inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c true 2 wit inspect 8.4 430 73 - wit inspect - wit inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c true 2 wit inspect 8.5 430 73 - wit inspect - wit inspect
termination-numeric/twisted_true-termination_true-no-overflow.c true 2 wit inspect 6.6 340 61 - wit inspect - wit inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c true 2 wit inspect 7.7 450 65 - wit inspect - wit inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c true 2 wit inspect 5.4 300 49 - wit inspect - wit inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c true 2 wit inspect 35   510 400 - wit inspect - wit inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c true 2 wit inspect 34   540 370 - wit inspect - wit inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c true 2 wit inspect 7.1 370 59 - wit inspect - wit inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 wit inspect 7.4 370 62 - wit inspect - wit inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c true 2 wit inspect 11   560 76 - wit inspect - wit inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect 6.4 300 58 - wit inspect - wit inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c true 2 wit inspect 7.7 430 58 - wit inspect - wit inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 wit inspect 5.7 280 44 - wit inspect - wit inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true 2 wit inspect 7.3 350 58 - wit inspect - wit inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 wit inspect 6.8 340 56 - wit inspect - wit inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 wit inspect 5.0 290 45 - wit inspect - wit inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 wit inspect 5.3 300 38 - wit inspect - wit inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 wit inspect 5.7 290 45 - wit inspect - wit inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 wit inspect 5.9 280 49 - wit inspect - wit inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 wit inspect 5.5 280 41 - wit inspect - wit inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 wit inspect 6.4 290 54 - wit inspect - wit inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 44 - wit inspect - wit inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true 2 wit inspect 5.1 290 45 - wit inspect - wit inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true 2 wit inspect 7.5 300 68 - wit inspect - wit inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true 2 wit inspect 4.8 300 44 - wit inspect - wit inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 wit inspect 5.5 300 45 - wit inspect - wit inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true 2 wit inspect 8.0 360 73 - wit inspect - wit inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true 2 wit inspect 11   300 130 - wit inspect - wit inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true 2 wit inspect 6.9 380 54 - wit inspect - wit inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 wit inspect 5.4 290 44 - wit inspect - wit inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 wit inspect 4.7 290 37 - wit inspect - wit inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 wit inspect 6.4 330 62 - wit inspect - wit inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 wit inspect 4.9 300 40 - wit inspect - wit inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 wit inspect 4.8 300 37 - wit inspect - wit inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c true 2 wit inspect 6.7 370 53 - wit inspect - wit inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 43 - wit inspect - wit inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c true 2 wit inspect 5.3 300 42 - wit inspect - wit inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c true 2 wit inspect 17   400 210 - wit inspect - wit inspect
termination-restricted-15/a.10_true-termination.c true 2 wit inspect 7.5 350 67 - wit inspect - wit inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 wit inspect 5.0 290 39 - wit inspect - wit inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c true 2 wit inspect 5.1 300 41 - wit inspect - wit inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c true 2 wit inspect 18   400 160 - wit inspect - wit inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c true 2 wit inspect 17   380 180 - wit inspect - wit inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c true 2 wit inspect 7.0 300 59 - wit inspect - wit inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 wit inspect 5.5 310 47 - wit inspect - wit inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 43 - wit inspect - wit inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 wit inspect 5.5 300 45 - wit inspect - wit inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c true 2 wit inspect 9.2 530 76 - wit inspect - wit inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true 2 wit inspect 5.7 310 44 - wit inspect - wit inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c true 2 wit inspect 18   360 200 - wit inspect - wit inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c true 2 wit inspect 31   370 380 - wit inspect - wit inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c true 2 wit inspect 5.6 300 47 - wit inspect - wit inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c true 2 wit inspect 5.9 310 47 - wit inspect - wit inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 wit inspect 5.6 290 49 - wit inspect - wit inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 wit inspect 6.0 300 48 - wit inspect - wit inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 wit inspect 5.6 290 49 - wit inspect - wit inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 wit inspect 5.9 280 50 - wit inspect - wit inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 wit inspect 6.5 320 54 - wit inspect - wit inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c true 2 wit inspect 11   470 93 - wit inspect - wit inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true 2 wit inspect 6.7 340 53 - wit inspect - wit inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c true 2 wit inspect 7.0 320 64 - wit inspect - wit inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c true 2 wit inspect 30   400 330 - wit inspect - wit inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c true 2 wit inspect 5.5 310 43 - wit inspect - wit inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 wit inspect 6.6 330 60 - wit inspect - wit inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c unknown 0 wit inspect 10   540 86 - wit inspect - wit inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c unknown 0 wit inspect 11   580 97 - wit inspect - wit inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 42 - wit inspect - wit inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 wit inspect 5.2 310 47 - wit inspect - wit inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 wit inspect 5.3 310 44 - wit inspect - wit inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 wit inspect 8.8 500 67 - wit inspect - wit inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 wit inspect 5.6 320 46 - wit inspect - wit inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 6.0 310 48 unknown 0 wit inspect 4.1  270 false(termination) 1 wit inspect 4.9   260  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 250 32 unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 5.0   250  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 240 34 unknown 0 wit inspect 3.5  250 false(termination) 1 wit inspect 5.2   260  
termination-restricted-15/Ex02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.4 240 34 unknown 0 wit inspect 3.4  260 false(termination) 1 wit inspect 4.8   250  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.4 250 35 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.0   260  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 240 34 timeout 0 wit inspect 97    5200 false(termination) 1 wit inspect 4.9   240  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.6 300 41 unknown 0 wit inspect 2.3  170 false(termination) 1 wit inspect 9.0   340  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.8 320 39 unknown 0 wit inspect 2.3  170 false(termination) 1 wit inspect 8.0   320  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) 1 wit inspect 24   840 190 unknown 0 wit inspect 3.3  210 false(termination) 1 wit inspect 12     530  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.5 400 80 unknown 0 wit inspect 4.4  270 false(termination) 1 wit inspect 6.4   270  
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.4 330 50 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 6.5   270  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.8 260 40 unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 5.4   260  
termination-restricted-15/GCD_false-termination_true-no-overflow.c false(termination) 1 wit inspect 6.7 350 60 unknown 0 wit inspect 3.7  270 false(termination) 1 wit inspect 5.4   260  
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.3 240 32 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.4   250  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.5 350 54 unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 240 35 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.3   260  
termination-restricted-15/NO_01_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.7 300 48 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.5   260  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.7 280 41 unknown 0 wit inspect 3.5  260 false(termination) 1 wit inspect 5.2   250  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.5 280 38 unknown 0 wit inspect 3.4  270 false(termination) 1 wit inspect 5.2   260  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) 1 wit inspect 19   350 210 unknown 0 wit inspect 3.7  270 false(termination) 1 wit inspect 6.2   260  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c false(termination) 1 wit inspect 41   1200 420 unknown 0 wit inspect 23    460 false(termination) 1 wit inspect 84     3000  
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.5 240 35 unknown 0 wit inspect 3.3  260 false(termination) 1 wit inspect 5.0   260  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c false(termination) 1 wit inspect 40   1200 350 unknown 0 wit inspect 23    470 false(termination) 1 wit inspect 88     3200  
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.8 380 63 unknown 0 wit inspect 3.6  260 false(termination) 1 wit inspect 8.4   340  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c unknown 0 wit inspect 34   430 430 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .041 4.9
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 74   1700 960 unknown 0 wit inspect 7.3  300 false(termination) 1 wit inspect 43     1300  
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c false(termination) 1 wit inspect 31   780 290 unknown 0 wit inspect 3.7  210 false(termination) 1 wit inspect 26     840  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.2 530 81 unknown 0 wit inspect 2.6  200 false(termination) 1 wit inspect 6.5   270  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c unknown 0 wit inspect 33   550 430 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .049 4.9
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.5 260 33 unknown 0 wit inspect 4.0  270 false(termination) 1 wit inspect 5.2   250  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c false(termination) 1 wit inspect 26   850 230 unknown 0 wit inspect 2.8  180 false(termination) 1 wit inspect 17     620  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c timeout 0 wit inspect 900   6200 13000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 4.9
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.2 240 35 unknown 0 wit inspect 3.5  270 false(termination) 1 wit inspect 5.1   250  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.3 240 37 unknown 0 wit inspect 3.4  270 false(termination) 1 wit inspect 5.0   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 397 16000 200000 160000 56 2 400   23000 56 17 630   26000
    correct results 223 397 2400 85000 24000 2 2 6.5 520 49 49 530   21000
        correct true 174 348 1900 66000 19000 0 0
        correct false 49 49 480 19000 4500 2 2 6.5 520 49 49 530   21000
    correct-unconfimed results 2 0 12 610 96 0 0
        correct-unconfirmed true 0 0 0
        correct-unconfirmed false 2 0 12 610 96 0 0
    incorrect results 0 0 1 -32 4.4 210
        incorrect true 0 0 1 -32 4.4 210
        incorrect false 0 0 0
score (250 tasks, max score: 444) 397 2 17
Run set uautomizer.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.Termination-MainControlFlow