Tool CBMC 5.8 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* [apollon029; apollon035; apollon037; apollon075; apollon077; apollon078] [apollon029; apollon077; apollon078]
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 13:00:07 CET 2017-12-01 19:39:59 CET 2017-12-01 19:43:03 CET
Run set cbmc.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainControlFlow
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_1300.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/cbmc.2017-12-01_1300.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 880    5000 3700   0 .52 42 0 .018 4.8
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 0 870    4700 3000   0 .52 41 0 .017 4.9
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 0 880    8400 3900   0 .41 43 0 .022 4.8
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c 0 650    15000 6400   0 .41 43 0 .018 5.0
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 0 880    7600 3000   0 .41 41 0 .022 4.8
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 0 880    8400 3900   0 .51 42 0 .018 5.0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 0 210    15000 2600   0 .43 42 0 .019 5.0
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 0 870    330 4100   0 .54 41 0 .021 4.9
termination-crafted/Mysore_false-termination_true-valid-memsafety.c 0 870    6600 5200   0 .56 42 0 .018 4.9
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c 0 870    650 3600   0 .44 42 0 .042 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 0 870    750 5600   0 .42 43 0 .018 4.8
termination-crafted/NonTermination3_false-termination_false-valid-deref.c 0 870    2700 5800   0 .43 44 0 .023 4.8
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 0 870    2700 5200   0 .54 41 0 .023 4.8
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 0 880    8500 3100   0 .43 43 0 .041 4.8
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c 0 270    15000 2400   0 .50 42 0 .022 4.9
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c 0 310    15000 4300   0 .46 43 0 .018 4.9
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 0 210    15000 2900   0 .44 46 0 .017 4.8
termination-crafted/2Nested_true-termination_true-valid-memsafety.c 0 870    6700 4100   - -
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 2 2.4  34 20   - -
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c 0 870    1100 5800   - -
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c 0 870    410 3100   - -
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    7200 3700   - -
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    7600 3000   - -
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    7700 3000   - -
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 2 .44 33 3.9 - -
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c 0 870    3800 2600   - -
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    3800 3700   - -
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    8100 5500   - -
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 0 880    8100 3600   - -
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c 0 870    5200 3500   - -
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 0 880    5700 4200   - -
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c 0 870    5800 2900   - -
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c 0 880    6100 4700   - -
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    13000 6400   - -
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c 0 870    13000 8200   - -
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c 0 870    3100 7000   - -
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    3000 5500   - -
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    280 2900   - -
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    5200 4800   - -
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    320 2900   - -
termination-crafted/Mysore_true-termination_true-valid-memsafety.c 0 870    460 10000   - -
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    650 3000   - -
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    440 3500   - -
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    660 3000   - -
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 0 820    15000 6600   - -
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    3300 7400   - -
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    3500 7100   - -
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    670 6200   - -
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c 0 870    200 9600   - -
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c 0 870    580 7300   - -
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c 0 870    12000 11000   - -
termination-crafted/Singapore_true-termination_true-valid-memsafety.c 2 6.6  39 75   - -
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c 0 880    7800 4000   - -
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 0 870    6500 4500   - -
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c 0 870    6000 3300   - -
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c 0 870    6300 3400   - -
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    1100 7900   - -
termination-crafted/Thun_true-termination_true-valid-memsafety.c 2 2.0  33 21   - -
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c 0 870    5900 3400   - -
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c 0 870    6000 4200   - -
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 0 880    8200 3000   - -
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2 .42 33 3.9 - -
termination-crafted/aaron2_true-termination_true-valid-memsafety.c 0 870    600 7700   - -
termination-crafted/aaron3_true-termination_true-valid-memsafety.c 0 870    260 10000   - -
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 2 3.2  43 35   - -
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 0 870    4700 3100   - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 0 870    3100 6000   0 .54 41 0 .046 5.0
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 0 870    8100 3500   0 .40 43 0 .050 4.8
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 0 870    2100 5900   0 .42 41 0 .047 5.0
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 0 870    3400 6700   0 .43 43 0 .018 4.8
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 0 870    2400 6800   0 .44 44 0 .023 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 0 870    1400 4600   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 0 870    3200 5700   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2 3.3  47 32   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 0 870    4700 3800   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 0 870    640 4900   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 0 870    1100 3200   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 0 870    3000 7800   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 2 1.2  33 12   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 0 870    3200 5900   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 0 870    3300 8900   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 0 870    3200 7200   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 0 870    2400 7100   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 0 870    670 3500   - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 0 870    3300 6200   - -
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 0 870    6200 5200   - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 0 870    3100 7000   - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 0 870    660 2800   - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 0 870    670 3600   - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 0 870    6100 3200   - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2 3.2  45 33   - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 0 870    4900 4100   - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 0 870    2800 5800   - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 2 1.2  33 12   - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 0 870    5300 3700   - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 0 870    6000 3200   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 0 870    2300 5900   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 0 870    1900 4900   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 0 870    1900 6400   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 0 870    3200 7200   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 0 870    3300 6400   - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 0 870    3400 5600   - -
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 2 2.7  33 29   - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 0 870    2700 7600   - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 0 870    1800 6100   - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 0 870    5400 3300   - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 0 860    8500 4300   - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 0 870    6200 3700   - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 0 870    5900 3400   - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 0 870    1900 8900   - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 0 880    3100 5300   - -
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 0 870    990 3300   - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 0 870    13000 10000   - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 0 870    13000 9500   - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 0 870    3300 6200   - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 0 870    2800 7000   - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2 2.5  38 25   - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 0 880    630 3500   - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 0 880    7900 3900   - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 0 870    660 3300   - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 0 870    2200 6400   - -
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 0 870    4900 8500   - -
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 0 870    1100 3800   - -
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 0 870    2400 5900   - -
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 2 5.1  160 55   - -
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 0 870    8500 3800   - -
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 0 870    1200 3600   - -
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 0 880    7700 5000   - -
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 0 870    1200 3600   - -
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 0 870    1200 3700   - -
termination-crafted-lit/genady_true-termination_true-no-overflow.c 2 7.7  79 82   - -
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 0 720    8500 4300   - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 0 870    440 5900   - -
termination-numeric/Binomial_true-termination_false-no-overflow.c 0 870    1000 5000   - -
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 0 870    8700 5200   - -
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 0 870    270 2500   - -
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 0 590    15000 3200   - -
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 2 4.3  86 52   - -
termination-numeric/Parts_true-termination_true-no-overflow.c 0 870    590 4100   - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 0 410    15000 2600   - -
termination-numeric/TwoWay_true-termination_true-no-overflow.c 0 870    11000 4500   - -
termination-numeric/gcd01_true-termination_true-no-overflow.c 0 710    15000 10000   - -
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 2 2.6  38 30   - -
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 2 2.4  35 23   - -
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 0 870    660 3800   - -
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 0 870    660 3400   - -
termination-numeric/twisted_true-termination_true-no-overflow.c 0 870    1300 5100   - -
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c 0 870    2100 4100   - -
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c 0 870    5300 2900   - -
termination-restricted-15/GCD3_true-termination_true-no-overflow.c 0 870    1300 3700   - -
termination-restricted-15/GCD4_true-termination_true-no-overflow.c 0 870    690 3900   - -
termination-restricted-15/IntPath_true-termination_true-no-overflow.c 2 .41 33 3.6 - -
termination-restricted-15/LogAG_true-termination_true-no-overflow.c 0 870    960 3800   - -
termination-restricted-15/Log_true-termination_true-no-overflow.c 0 870    960 3900   - -
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c 0 870    2900 6000   - -
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c 2 .41 33 3.3 - -
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c 0 870    1000 3100   - -
termination-restricted-15/Nested_true-termination_true-no-overflow.c 2 1.1  33 11   - -
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c 0 870    3300 6200   - -
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c 0 870    660 4900   - -
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c 0 880    7400 3700   - -
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c 0 870    5900 3800   - -
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c 0 870    960 4500   - -
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c 0 880    960 3100   - -
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c 0 870    660 3200   - -
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c 0 870    660 3200   - -
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c 0 880    7800 3900   - -
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c 0 870    6200 4800   - -
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c 2 .44 33 4.4 - -
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c 0 870    6200 3400   - -
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c 0 870    6300 3800   - -
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c 0 870    3300 6600   - -
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c 0 880    5600 4200   - -
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c 0 870    1600 5800   - -
termination-restricted-15/Sequence_true-termination_true-no-overflow.c 2 2.7  33 27   - -
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c 0 870    7600 2500   - -
termination-restricted-15/a.01_true-termination_true-no-overflow.c 0 870    650 3000   - -
termination-restricted-15/a.04_true-termination_true-no-overflow.c 0 870    7200 2900   - -
termination-restricted-15/a.05_true-termination_true-no-overflow.c 0 870    8300 3500   - -
termination-restricted-15/a.06_true-termination_true-no-overflow.c 0 870    6400 3200   - -
termination-restricted-15/a.07_true-termination_true-no-overflow.c 0 870    5800 3100   - -
termination-restricted-15/a.08_true-termination_true-no-overflow.c 0 880    5000 2900   - -
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c 0 880    8000 2900   - -
termination-restricted-15/a.10_true-termination.c 0 870    3300 7400   - -
termination-restricted-15/b.01_true-termination_true-no-overflow.c 0 870    7100 2200   - -
termination-restricted-15/b.02_true-termination_true-no-overflow.c 0 880    6100 3200   - -
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c 0 880    4100 3700   - -
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c 0 870    4000 4500   - -
termination-restricted-15/b.04_true-termination_true-no-overflow.c 2 .41 33 3.8 - -
termination-restricted-15/b.05_true-termination_true-no-overflow.c 2 .42 33 3.8 - -
termination-restricted-15/b.06_true-termination_true-no-overflow.c 0 880    4500 3000   - -
termination-restricted-15/b.07_true-termination_true-no-overflow.c 0 870    6300 5000   - -
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c 0 870    3300 6800   - -
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c 0 870    3100 6000   - -
termination-restricted-15/b.10_true-termination_true-no-overflow.c 0 870    2700 6600   - -
termination-restricted-15/b.11_true-termination_true-no-overflow.c 0 870    3100 6900   - -
termination-restricted-15/b.12_true-termination_true-no-overflow.c 0 870    2800 6100   - -
termination-restricted-15/b.13_true-termination_true-no-overflow.c 0 870    2900 6600   - -
termination-restricted-15/b.14_true-termination_true-no-overflow.c 0 870    1300 3100   - -
termination-restricted-15/b.15_true-termination_true-no-overflow.c 0 870    960 3400   - -
termination-restricted-15/b.16_true-termination_true-no-overflow.c 0 870    660 3700   - -
termination-restricted-15/b.17_true-termination_true-no-overflow.c 0 870    660 3500   - -
termination-restricted-15/b.18_true-termination_true-no-overflow.c 0 870    1300 4400   - -
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c 0 870    7900 8000   - -
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c 0 870    7900 7500   - -
termination-restricted-15/c.02_true-termination_true-no-overflow.c 0 870    660 4000   - -
termination-restricted-15/c.03_true-termination_true-no-overflow.c 0 870    3300 6000   - -
termination-restricted-15/c.07_true-termination_true-no-overflow.c 0 870    3600 2700   - -
termination-restricted-15/c.08_true-termination_true-no-overflow.c 0 870    650 4600   - -
termination-restricted-15/ex3a_true-termination_true-no-overflow.c 2 .89 34 7.6 - -
termination-restricted-15/ex3b_true-termination_true-no-overflow.c 2 .84 35 9.1 - -
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c 0 870    5000 3300   - -
termination-restricted-15/java_Break_true-termination_true-no-overflow.c 2 1.1  33 11   - -
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c 2 1.9  33 21   - -
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c 2 1.2  33 11   - -
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c 2 2.6  33 31   - -
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c 0 870    4000 6400   0 .52 41 0 .020 4.8
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c 0 870    2200 6200   0 .44 43 0 .020 4.9
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c 0 870    3500 9900   0 .52 41 0 .047 4.8
termination-restricted-15/Ex02_false-termination_true-no-overflow.c 0 870    3500 7800   0 .55 41 0 .019 4.9
termination-restricted-15/Ex03_false-termination_true-no-overflow.c 0 870    3400 7700   0 .43 43 0 .045 5.0
termination-restricted-15/Ex05_false-termination_true-no-overflow.c 0 190    15000 2700   0 .43 43 0 .047 5.0
termination-restricted-15/Ex06_false-termination_true-no-overflow.c 0 870    2600 6600   0 .44 41 0 .049 4.8
termination-restricted-15/Ex07_false-termination_true-no-overflow.c 0 350    15000 4400   0 .45 44 0 .021 4.9
termination-restricted-15/Ex08_false-termination_true-no-overflow.c 0 880    2700 6700   0 .51 41 0 .019 5.0
termination-restricted-15/Flip2_false-termination_true-no-overflow.c 0 870    2700 5900   0 .52 42 0 .020 4.8
termination-restricted-15/Flip_false-termination_true-no-overflow.c 0 870    4600 2800   0 .56 41 0 .022 4.9
termination-restricted-15/GCD2_false-termination_true-no-overflow.c 0 870    670 3700   0 .57 43 0 .018 4.9
termination-restricted-15/GCD_false-termination_true-no-overflow.c 0 870    680 2800   0 .41 43 0 .028 4.9
termination-restricted-15/Loop_false-termination_true-no-overflow.c 0 340    15000 4400   0 .57 41 0 .036 4.9
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c 0 870    2300 7500   0 .42 42 0 .019 4.9
termination-restricted-15/NO_00_false-termination_true-no-overflow.c 0 350    15000 4900   0 .39 43 0 .017 4.8
termination-restricted-15/NO_01_false-termination_true-no-overflow.c 0 340    15000 4200   0 .66 43 0 .022 4.8
termination-restricted-15/NO_02_false-termination_true-no-overflow.c 0 370    15000 5400   0 .50 41 0 .023 4.8
termination-restricted-15/NO_03_false-termination_true-no-overflow.c 0 350    15000 4500   0 .41 43 0 .046 4.8
termination-restricted-15/NO_04_false-termination_true-no-overflow.c 0 580    15000 7800   0 .44 41 0 .034 4.9
termination-restricted-15/NO_13_false-termination_true-no-overflow.c 0 440    15000 6700   0 .53 41 0 .019 4.9
termination-restricted-15/NO_21_false-termination_true-no-overflow.c 0 340    15000 4200   0 .58 43 0 .048 4.8
termination-restricted-15/NO_22_false-termination_true-no-overflow.c 0 420    15000 5800   0 .51 41 0 .017 5.0
termination-restricted-15/NO_23_false-termination_true-no-overflow.c 0 330    15000 4000   0 .55 42 0 .022 4.8
termination-restricted-15/NO_24_false-termination_true-no-overflow.c 0 450    15000 6800   0 .50 41 0 .023 4.8
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c 0 870    2600 7100   0 .51 41 0 .037 4.9
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c 0 870    2400 8800   0 .51 41 0 .019 4.9
termination-restricted-15/Sunset_false-termination_true-no-overflow.c 0 870    2800 7000   0 .62 43 0 .022 4.8
termination-restricted-15/Swingers_false-termination_true-no-overflow.c 0 360    15000 4600   0 .42 43 0 .019 4.9
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c 0 870    2400 7500   0 .53 41 0 .020 4.8
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c 0 870    2800 6900   0 .43 42 0 .018 4.9
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c 0 870    2700 6700   0 .51 41 0 .046 4.8
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c 0 870    3400 7500   0 .41 45 0 .023 4.8
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c 0 870    3300 8500   0 .56 42 0 .048 4.8
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 60 180000 1100000 1100000 56 0 27 2400 56 0 1.5 270
    correct results 30 60 66 1300 690 0 0
        correct true 30 60 66 1300 690 0 0
        correct false 0 0 0
    incorrect results 0 0 0
        incorrect true 0 0 0
        incorrect false 0 0 0
score (250 tasks, max score: 444) 60 0 0
Run set cbmc.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.Termination-MainControlFlow