Tool AProVE 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* [apollon077; apollon078; apollon084; apollon161] [apollon077; apollon078; apollon084; apollon124]
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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 15:55:47 CET 2017-11-30 15:57:34 CET
Run set aprove.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/aprove.2017-11-30_1120.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/aprove.2017-11-30_1120.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 0 6.0 350 50 0 .60 44 0 .021 4.8
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 1 7.1 380 52 0 1.6  170 1 3.5   260  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 0 6.0 450 45 0 .43 41 0 .049 4.9
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c 0 25   1300 180 0 .42 43 0 .018 5.0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 0 11   540 65 0 2.1  160 0 61     530  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 1 6.9 390 52 0 2.1  160 1 5.3   260  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 0 5.1 330 39 0 .40 45 0 .018 4.9
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 0 11   670 79 0 .51 44 0 .045 4.8
termination-crafted/Mysore_false-termination_true-valid-memsafety.c 0 900   3500 10000 0 .40 43 0 .023 4.8
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c 0 15   820 100 0 .43 42 0 .041 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 0 8.1 440 65 0 .42 41 0 .028 4.8
termination-crafted/NonTermination3_false-termination_false-valid-deref.c 0 8.6 540 62 0 .43 41 0 .036 4.8
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 0 9.8 570 73 0 .41 43 0 .037 4.8
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 0 5.6 410 44 0 .41 41 0 .019 4.9
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c 1 8.5 590 63 0 2.2  170 1 5.7   260  
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c 1 6.2 370 48 0 1.6  160 1 3.7   260  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 0 1.9 230 17 0 .44 42 0 .026 5.0
termination-crafted/2Nested_true-termination_true-valid-memsafety.c 2 7.1 470 51 - -
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.8 340 29 - -
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c 2 18   1300 130 - -
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c 2 30   2700 240 - -
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 2 9.2 570 61 - -
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 2 10   770 76 - -
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 2 6.1 470 46 - -
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.3 280 28 - -
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c 2 13   850 86 - -
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 2 6.4 440 45 - -
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 2 5.7 440 41 - -
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 2 4.4 360 33 - -
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c 2 9.3 670 65 - -
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 2 2.1 220 18 - -
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c 2 29   2200 190 - -
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c 0 900   3600 12000 - -
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 2 36   2300 270 - -
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c 0 900   14000 8400 - -
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c 2 5.1 340 37 - -
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 2 2.6 250 18 - -
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 0 730   15000 6300 - -
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 0 23   920 190 - -
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 2 9.5 730 74 - -
termination-crafted/Mysore_true-termination_true-valid-memsafety.c 2 7.7 490 58 - -
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 13   720 84 - -
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 2 5.6 410 41 - -
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 2 8.1 670 60 - -
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 2 8.4 650 58 - -
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 2 2.8 270 22 - -
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.0 260 22 - -
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 2 46   2200 260 - -
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c 2 9.8 630 74 - -
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c 0 910   10000 4900 - -
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c 2 9.6 730 82 - -
termination-crafted/Singapore_true-termination_true-valid-memsafety.c 0 640   15000 3000 - -
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c 2 6.3 460 45 - -
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 2 4.3 310 32 - -
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c 2 4.8 330 36 - -
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c 2 3.8 300 30 - -
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 0 910   14000 4900 - -
termination-crafted/Thun_true-termination_true-valid-memsafety.c 2 6.1 420 49 - -
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c 2 8.0 520 66 - -
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c 2 7.8 510 54 - -
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.9 320 27 - -
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2 1.9 200 18 - -
termination-crafted/aaron2_true-termination_true-valid-memsafety.c 2 52   2600 350 - -
termination-crafted/aaron3_true-termination_true-valid-memsafety.c 0 910   8300 4900 - -
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.1 260 24 - -
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 2 2.1 220 20 - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 0 5.9 450 43 0 .55 42 0 .024 4.9
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 0 5.7 430 44 0 .44 42 0 .021 4.9
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 1 120   5600 680 0 2.2  170 1 11     500  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 0 6.3 500 45 0 .44 44 0 .050 4.8
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 0 10   630 58 0 .43 43 0 .018 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 2 3.7 290 27 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 2 2.7 250 23 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2 8.3 540 57 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 2 6.8 490 54 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 2 23   1100 160 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 2 4.7 330 36 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 2 2.7 250 24 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 2 8.2 600 57 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 2 5.1 430 38 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 2 3.0 270 26 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 2 5.4 440 41 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 2 2.9 270 22 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 2 2.6 250 21 - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 2 5.8 440 36 - -
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 2 2.9 270 25 - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 2 6.5 460 47 - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 2 2.7 260 24 - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 2 44   1900 310 - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 2 3.6 290 25 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2 6.8 490 47 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 2 6.1 480 48 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 2 2.7 260 20 - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 2 8.0 510 55 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 2 2.5 260 19 - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 2 2.1 230 19 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 2 3.0 270 26 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 2 3.2 270 27 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 2 4.0 290 31 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 2 4.7 400 34 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 2 4.3 350 29 - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 2 12   590 80 - -
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 2 2.8 260 20 - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 2 81   3600 580 - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 2 13   740 72 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 2 3.0 280 24 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 2 2.0 270 16 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 2 5.0 350 36 - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 2 2.2 240 21 - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 2 2.8 270 22 - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 0 900   3500 12000 - -
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 2 14   650 88 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 2 16   1100 110 - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 2 8.7 590 62 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 2 2.6 260 22 - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 2 3.3 280 27 - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2 3.8 310 30 - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 2 14   710 83 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 2 2.2 220 17 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 2 2.5 250 20 - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 2 2.9 270 22 - -
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 2 2.6 260 23 - -
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 2 2.7 260 21 - -
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 2 120   4300 660 - -
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 2 34   2700 200 - -
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 2 14   820 110 - -
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 2 90   5300 530 - -
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 2 8.4 480 57 - -
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 2 50   4600 350 - -
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 2 52   3900 320 - -
termination-crafted-lit/genady_true-termination_true-no-overflow.c 2 2.2 230 18 - -
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 2 8.2 650 66 - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 2 27   2000 240 - -
termination-numeric/Binomial_true-termination_false-no-overflow.c 0 10   720 81 - -
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 2 10   720 67 - -
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 2 15   1100 120 - -
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 2 8.9 600 58 - -
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 0 900   5500 13000 - -
termination-numeric/Parts_true-termination_true-no-overflow.c 0 900   13000 7800 - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 2 7.2 500 61 - -
termination-numeric/TwoWay_true-termination_true-no-overflow.c 2 11   800 71 - -
termination-numeric/gcd01_true-termination_true-no-overflow.c 2 12   730 93 - -
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 2 5.4 380 43 - -
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 2 7.3 460 53 - -
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 2 15   1000 100 - -
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 2 12   970 87 - -
termination-numeric/twisted_true-termination_true-no-overflow.c 2 69   5200 460 - -
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c 2 4.8 410 34 - -
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c 2 2.1 230 19 - -
termination-restricted-15/GCD3_true-termination_true-no-overflow.c 2 18   850 110 - -
termination-restricted-15/GCD4_true-termination_true-no-overflow.c 2 3.4 280 23 - -
termination-restricted-15/IntPath_true-termination_true-no-overflow.c 2 3.3 280 29 - -
termination-restricted-15/LogAG_true-termination_true-no-overflow.c 2 2.9 270 22 - -
termination-restricted-15/Log_true-termination_true-no-overflow.c 2 2.7 250 22 - -
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c 2 2.8 260 23 - -
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c 2 2.6 230 21 - -
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c 2 3.4 270 24 - -
termination-restricted-15/Nested_true-termination_true-no-overflow.c 2 2.7 260 21 - -
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c 2 8.5 550 55 - -
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c 2 2.7 260 21 - -
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c 2 2.3 250 20 - -
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c 2 2.1 230 18 - -
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c 2 2.7 270 23 - -
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c 2 2.6 250 20 - -
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c 2 2.6 250 21 - -
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c 2 2.6 250 21 - -
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c 2 2.2 220 17 - -
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c 2 2.1 230 18 - -
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c 2 2.1 230 18 - -
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c 2 2.5 250 20 - -
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c 2 2.6 260 20 - -
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c 2 2.9 260 20 - -
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c 2 2.5 240 20 - -
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c 2 3.0 270 19 - -
termination-restricted-15/Sequence_true-termination_true-no-overflow.c 2 2.5 230 19 - -
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c 2 2.1 220 20 - -
termination-restricted-15/a.01_true-termination_true-no-overflow.c 2 2.6 270 22 - -
termination-restricted-15/a.04_true-termination_true-no-overflow.c 2 2.2 230 20 - -
termination-restricted-15/a.05_true-termination_true-no-overflow.c 2 2.2 230 17 - -
termination-restricted-15/a.06_true-termination_true-no-overflow.c 2 2.9 270 23 - -
termination-restricted-15/a.07_true-termination_true-no-overflow.c 2 2.5 280 23 - -
termination-restricted-15/a.08_true-termination_true-no-overflow.c 2 2.1 230 18 - -
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c 2 2.6 250 23 - -
termination-restricted-15/a.10_true-termination.c 2 4.5 350 33 - -
termination-restricted-15/b.01_true-termination_true-no-overflow.c 2 2.1 230 19 - -
termination-restricted-15/b.02_true-termination_true-no-overflow.c 2 2.1 220 19 - -
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c 2 6.6 450 44 - -
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c 2 2.4 270 19 - -
termination-restricted-15/b.04_true-termination_true-no-overflow.c 2 2.2 230 18 - -
termination-restricted-15/b.05_true-termination_true-no-overflow.c 2 2.5 250 23 - -
termination-restricted-15/b.06_true-termination_true-no-overflow.c 2 2.2 230 19 - -
termination-restricted-15/b.07_true-termination_true-no-overflow.c 2 2.9 280 24 - -
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c 2 4.3 300 29 - -
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c 2 2.8 280 22 - -
termination-restricted-15/b.10_true-termination_true-no-overflow.c 2 4.4 340 30 - -
termination-restricted-15/b.11_true-termination_true-no-overflow.c 2 3.0 270 23 - -
termination-restricted-15/b.12_true-termination_true-no-overflow.c 2 3.5 280 26 - -
termination-restricted-15/b.13_true-termination_true-no-overflow.c 2 3.6 280 25 - -
termination-restricted-15/b.14_true-termination_true-no-overflow.c 2 2.8 270 21 - -
termination-restricted-15/b.15_true-termination_true-no-overflow.c 2 2.6 260 22 - -
termination-restricted-15/b.16_true-termination_true-no-overflow.c 2 2.6 250 24 - -
termination-restricted-15/b.17_true-termination_true-no-overflow.c 2 2.8 260 21 - -
termination-restricted-15/b.18_true-termination_true-no-overflow.c 2 3.4 280 26 - -
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c 2 5.5 430 38 - -
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c 2 3.8 310 26 - -
termination-restricted-15/c.02_true-termination_true-no-overflow.c 2 2.3 260 17 - -
termination-restricted-15/c.03_true-termination_true-no-overflow.c 2 3.3 280 24 - -
termination-restricted-15/c.07_true-termination_true-no-overflow.c 2 2.8 250 21 - -
termination-restricted-15/c.08_true-termination_true-no-overflow.c 2 2.8 260 25 - -
termination-restricted-15/ex3a_true-termination_true-no-overflow.c 2 2.2 230 21 - -
termination-restricted-15/ex3b_true-termination_true-no-overflow.c 2 6.4 480 49 - -
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c 2 2.6 250 21 - -
termination-restricted-15/java_Break_true-termination_true-no-overflow.c 2 2.1 230 21 - -
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c 2 2.5 270 21 - -
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c 2 2.6 270 21 - -
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c 2 2.6 250 20 - -
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c 1 28   1600 150 0 1.6  170 1 4.3   270  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c 0 8.3 570 51 0 .45 45 0 .049 4.8
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c 0 7.1 520 52 0 .43 41 0 .022 4.8
termination-restricted-15/Ex02_false-termination_true-no-overflow.c 0 9.7 510 60 0 .54 43 0 .043 5.0
termination-restricted-15/Ex03_false-termination_true-no-overflow.c 0 6.2 490 46 0 .54 45 0 .033 5.0
termination-restricted-15/Ex05_false-termination_true-no-overflow.c 0 5.7 380 37 0 .44 43 0 .018 5.0
termination-restricted-15/Ex06_false-termination_true-no-overflow.c 0 7.6 520 49 0 .55 43 0 .048 5.0
termination-restricted-15/Ex07_false-termination_true-no-overflow.c 1 18   720 110 0 2.2  170 1 5.7   340  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c 1 42   1900 250 0 1.6  170 1 32     1200  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c 1 20   1000 120 0 1.5  160 1 6.0   280  
termination-restricted-15/Flip_false-termination_true-no-overflow.c 0 6.8 470 49 0 .42 41 0 .024 4.8
termination-restricted-15/GCD2_false-termination_true-no-overflow.c 0 6.9 590 50 0 .42 43 0 .019 4.8
termination-restricted-15/GCD_false-termination_true-no-overflow.c 0 6.7 460 50 0 .44 41 0 .037 4.8
termination-restricted-15/Loop_false-termination_true-no-overflow.c 0 6.0 440 40 0 .54 41 0 .050 4.8
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c 0 8.0 500 53 0 .55 45 0 .018 4.9
termination-restricted-15/NO_00_false-termination_true-no-overflow.c 0 4.9 340 34 0 .54 43 0 .045 4.8
termination-restricted-15/NO_01_false-termination_true-no-overflow.c 1 8.6 490 58 0 2.1  170 1 5.2   260  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c 0 5.8 390 39 0 .43 44 0 .019 4.8
termination-restricted-15/NO_03_false-termination_true-no-overflow.c 0 5.7 410 42 0 .55 44 0 .023 4.8
termination-restricted-15/NO_04_false-termination_true-no-overflow.c 1 11   580 82 0 2.3  170 1 3.8   260  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c 0 6.3 440 47 0 .44 43 0 .018 5.0
termination-restricted-15/NO_21_false-termination_true-no-overflow.c 0 5.3 370 38 0 .54 46 0 .025 4.9
termination-restricted-15/NO_22_false-termination_true-no-overflow.c 0 6.9 480 48 0 .53 43 0 .047 4.9
termination-restricted-15/NO_23_false-termination_true-no-overflow.c 0 6.2 420 48 0 .54 43 0 .019 5.0
termination-restricted-15/NO_24_false-termination_true-no-overflow.c 0 5.3 450 36 0 .39 43 0 .047 4.8
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c 0 910   14000 4400 0 .42 43 0 .040 4.9
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c 0 900   7800 7800 0 .50 43 0 .023 4.8
termination-restricted-15/Sunset_false-termination_true-no-overflow.c 1 23   980 120 0 2.3  160 1 12     500  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c 0 6.2 460 42 0 .40 43 0 .047 4.9
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c 0 6.6 470 45 0 .40 43 0 .019 4.8
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c 1 54   1800 330 0 2.3  170 1 28     750  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c 1 49   1500 270 0 2.2  170 1 26     1000  
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c 0 6.7 490 41 0 .44 43 0 .049 4.8
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c 0 8.7 500 52 0 .52 43 0 .047 4.9
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 376 14000 280000 120000 56 0 49 4200 56 14 220 7100
    correct results 195 376 2000 130000 14000 0 14 14 150 6400
        correct true 181 362 1600 110000 11000 0 0
        correct false 14 14 410 18000 2400 0 14 14 150 6400
    correct-unconfimed results 32 0 210 15000 1500 0 0
        correct-unconfirmed true 0 0 0
        correct-unconfirmed false 32 0 210 15000 1500 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (250 tasks, max score: 444) 376 0 14
Run set aprove.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-aprove.sv-comp18-violation-witness.Termination-MainControlFlow