Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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-02 08:45:19 CET 2017-12-02 17:16:42 CET 2017-12-02 17:21:25 CET
Run set esbmc-incr.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Termination-MainControlFlow
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0845.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/esbmc-incr.2017-12-02_0845.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 900     970 13000    0 .51 41 0 .031 4.9
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c 0 900     970 12000    0 .40 41 0 .027 4.8
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c 0 900     150 12000    0 .40 43 0 .044 4.8
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c 0 340     15000 4200    0 .52 43 0 .025 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c 0 .031 15 .30 0 .55 43 0 .025 4.9
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c 0 900     840 12000    0 .52 43 0 .023 5.0
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c 0 900     11000 9800    0 .57 44 0 .035 4.9
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c 0 290     15000 3100    0 .40 43 0 .023 4.8
termination-crafted/Mysore_false-termination_true-valid-memsafety.c 0 900     210 12000    0 .54 43 0 .024 4.9
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c 0 330     15000 4200    0 .68 41 0 .046 5.0
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c 0 330     15000 3600    0 .54 45 0 .019 4.8
termination-crafted/NonTermination3_false-termination_false-valid-deref.c 0 900     1600 11000    0 .53 41 0 .019 5.0
termination-crafted/NonTermination3_true-no-overflow_false-termination.c 0 900     1600 11000    0 .53 45 0 .023 4.8
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c 0 900     690 12000    0 .54 41 0 .020 4.8
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c 0 900     1800 8600    0 .53 43 0 .018 5.0
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c 0 900     3700 13000    0 .52 43 0 .024 4.8
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c 0 290     15000 4000    0 .51 41 0 .018 4.8
termination-crafted/2Nested_true-termination_true-valid-memsafety.c 0 900     370 10000    - -
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c 2 .079 27 .94 - -
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c 0 900     300 12000    - -
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c 0 430     15000 6500    - -
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1100 11000    - -
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     670 10000    - -
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     95 11000    - -
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c 2 .12  26 1.2  - -
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c 0 900     280 10000    - -
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1300 12000    - -
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     830 11000    - -
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     800 11000    - -
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c 0 900     770 10000    - -
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     810 12000    - -
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c 0 900     290 12000    - -
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c 0 900     260 11000    - -
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     2100 11000    - -
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c 0 900     5100 11000    - -
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c 0 900     1100 9600    - -
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     310 11000    - -
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     15000 7400    - -
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     1000 9700    - -
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 290     15000 4300    - -
termination-crafted/Mysore_true-termination_true-valid-memsafety.c 0 900     160 10000    - -
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c 0 700     15000 6800    - -
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     9100 8300    - -
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c 0 370     15000 4400    - -
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c 0 310     15000 3700    - -
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     260 9800    - -
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     260 10000    - -
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     270 11000    - -
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c 0 900     510 11000    - -
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c 0 900     490 8900    - -
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c 0 350     15000 4100    - -
termination-crafted/Singapore_true-termination_true-valid-memsafety.c 2 4.8   31 58    - -
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c 0 900     210 12000    - -
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c 0 900     580 9800    - -
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c 0 900     590 11000    - -
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c 0 900     590 12000    - -
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     320 9900    - -
termination-crafted/Thun_true-termination_true-valid-memsafety.c 2 1.0   26 11    - -
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c 0 900     340 10000    - -
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c 0 900     340 13000    - -
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     600 11000    - -
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c 2 .074 26 .75 - -
termination-crafted/aaron2_true-termination_true-valid-memsafety.c 0 900     140 14000    - -
termination-crafted/aaron3_true-termination_true-valid-memsafety.c 0 900     280 12000    - -
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c 2 .22  26 2.4  - -
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c 0 900     820 11000    - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 0 900     240 11000    0 .58 44 0 .051 4.9
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 0 900     990 10000    0 .41 44 0 .023 4.9
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 0 900     1500 10000    0 .55 44 0 .025 4.8
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 0 900     380 11000    0 .60 43 0 .020 5.0
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 0 900     640 11000    0 .54 41 0 .023 4.8
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 0 900     800 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 0 900     470 12000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 2 .23  26 2.2  - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 0 900     820 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c 0 900     1400 9900    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 0 900     1800 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 0 900     1300 10000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 2 .088 26 1.1  - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 0 900     470 9800    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 0 900     450 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 0 900     280 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 0 900     1400 12000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 0 900     320 11000    - -
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 0 900     320 12000    - -
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 0 900     450 9600    - -
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 0 900     240 10000    - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 0 900     1400 9200    - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 0 900     440 13000    - -
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 0 900     600 10000    - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 2 .23  26 2.1  - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 0 900     820 11000    - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 0 900     1300 10000    - -
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 2 .093 26 1.0  - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 0 900     250 12000    - -
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 0 900     340 12000    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 0 900     560 12000    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 0 900     610 9600    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 0 900     750 10000    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 0 900     270 11000    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 0 900     290 12000    - -
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 0 900     370 12000    - -
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 2 .21  26 2.2  - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 0 900     510 9400    - -
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 0 900     970 9600    - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 0 900     880 9600    - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 0 900     470 11000    - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 0 900     950 9700    - -
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 0 900     210 11000    - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 0 900     280 11000    - -
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 0 900     440 9800    - -
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 0 900     920 9900    - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 0 400     15000 4600    - -
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 0 340     15000 4000    - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 0 900     360 11000    - -
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 0 900     470 9500    - -
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 2 .18  26 2.0  - -
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c 0 900     1300 8300    - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 0 900     590 10000    - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 0 900     1400 8600    - -
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 0 900     550 12000    - -
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 0 900     6500 9600    - -
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 0 900     1200 11000    - -
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 0 900     710 10000    - -
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 2 4.6   30 54    - -
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 0 900     3300 11000    - -
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 0 900     1300 9800    - -
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 0 900     2400 12000    - -
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 0 900     1700 9500    - -
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 0 900     1600 7900    - -
termination-crafted-lit/genady_true-termination_true-no-overflow.c 2 210     2900 3000    - -
termination-crafted-lit/strchr_true-no-overflow_true-termination.c 0 900     1200 12000    - -
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 0 420     15000 5200    - -
termination-numeric/Binomial_true-termination_false-no-overflow.c 0 900     6100 11000    - -
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 0 900     2300 8800    - -
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 0 340     15000 3800    - -
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 0 900     890 9700    - -
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 2 43     140 500    - -
termination-numeric/Parts_true-termination_true-no-overflow.c 0 900     9600 10000    - -
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 0 900     1200 11000    - -
termination-numeric/TwoWay_true-termination_true-no-overflow.c 0 900     990 9800    - -
termination-numeric/gcd01_true-termination_true-no-overflow.c 0 390     15000 4600    - -
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 2 .15  26 1.7  - -
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 2 .16  26 1.7  - -
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 0 900     1900 10000    - -
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 0 900     1600 7500    - -
termination-numeric/twisted_true-termination_true-no-overflow.c 0 900     1900 9400    - -
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c 0 900     1300 11000    - -
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c 0 900     140 10000    - -
termination-restricted-15/GCD3_true-termination_true-no-overflow.c 0 900     970 9300    - -
termination-restricted-15/GCD4_true-termination_true-no-overflow.c 0 900     1000 9800    - -
termination-restricted-15/IntPath_true-termination_true-no-overflow.c 2 .081 26 .67 - -
termination-restricted-15/LogAG_true-termination_true-no-overflow.c 0 900     890 8700    - -
termination-restricted-15/Log_true-termination_true-no-overflow.c 0 900     870 10000    - -
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c 0 900     310 11000    - -
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c 2 .11  26 .75 - -
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c 0 900     1100 12000    - -
termination-restricted-15/Nested_true-termination_true-no-overflow.c 2 .11  26 .67 - -
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c 0 900     290 8300    - -
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c 0 900     1400 11000    - -
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c 0 900     270 9800    - -
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c 0 900     370 11000    - -
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c 0 900     780 11000    - -
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c 0 900     1000 10000    - -
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c 0 900     790 12000    - -
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c 0 900     1100 11000    - -
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c 0 900     310 11000    - -
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c 0 900     270 11000    - -
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c 2 .11  26 .64 - -
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c 0 900     490 12000    - -
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c 0 900     380 11000    - -
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c 0 900     280 12000    - -
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c 0 900     350 12000    - -
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c 0 900     580 12000    - -
termination-restricted-15/Sequence_true-termination_true-no-overflow.c 2 .17  26 1.3  - -
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c 0 900     450 11000    - -
termination-restricted-15/a.01_true-termination_true-no-overflow.c 0 900     1400 8600    - -
termination-restricted-15/a.04_true-termination_true-no-overflow.c 0 900     260 10000    - -
termination-restricted-15/a.05_true-termination_true-no-overflow.c 0 900     290 9500    - -
termination-restricted-15/a.06_true-termination_true-no-overflow.c 0 900     330 9900    - -
termination-restricted-15/a.07_true-termination_true-no-overflow.c 0 900     360 10000    - -
termination-restricted-15/a.08_true-termination_true-no-overflow.c 0 900     290 10000    - -
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c 0 900     180 11000    - -
termination-restricted-15/a.10_true-termination.c 0 900     290 10000    - -
termination-restricted-15/b.01_true-termination_true-no-overflow.c 0 900     300 11000    - -
termination-restricted-15/b.02_true-termination_true-no-overflow.c 0 900     260 13000    - -
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c 0 900     180 10000    - -
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c 0 900     180 10000    - -
termination-restricted-15/b.04_true-termination_true-no-overflow.c 2 .10  26 .76 - -
termination-restricted-15/b.05_true-termination_true-no-overflow.c 2 .10  26 .71 - -
termination-restricted-15/b.06_true-termination_true-no-overflow.c 0 900     630 11000    - -
termination-restricted-15/b.07_true-termination_true-no-overflow.c 0 900     380 12000    - -
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c 0 900     540 10000    - -
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c 0 900     560 9900    - -
termination-restricted-15/b.10_true-termination_true-no-overflow.c 0 900     390 9700    - -
termination-restricted-15/b.11_true-termination_true-no-overflow.c 0 900     400 10000    - -
termination-restricted-15/b.12_true-termination_true-no-overflow.c 0 900     490 11000    - -
termination-restricted-15/b.13_true-termination_true-no-overflow.c 0 900     490 12000    - -
termination-restricted-15/b.14_true-termination_true-no-overflow.c 0 900     850 12000    - -
termination-restricted-15/b.15_true-termination_true-no-overflow.c 0 900     1000 11000    - -
termination-restricted-15/b.16_true-termination_true-no-overflow.c 0 900     790 13000    - -
termination-restricted-15/b.17_true-termination_true-no-overflow.c 0 900     1100 10000    - -
termination-restricted-15/b.18_true-termination_true-no-overflow.c 0 900     930 11000    - -
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c 0 900     2100 9400    - -
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c 0 900     2400 12000    - -
termination-restricted-15/c.02_true-termination_true-no-overflow.c 0 900     1300 8800    - -
termination-restricted-15/c.03_true-termination_true-no-overflow.c 0 900     330 11000    - -
termination-restricted-15/c.07_true-termination_true-no-overflow.c 0 900     420 11000    - -
termination-restricted-15/c.08_true-termination_true-no-overflow.c 0 900     1500 9000    - -
termination-restricted-15/ex3a_true-termination_true-no-overflow.c 2 .11  26 .80 - -
termination-restricted-15/ex3b_true-termination_true-no-overflow.c 2 .14  28 1.2  - -
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c 0 900     200 11000    - -
termination-restricted-15/java_Break_true-termination_true-no-overflow.c 2 .10  26 .77 - -
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c 2 .079 26 .90 - -
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c 2 .11  26 .84 - -
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c 2 .19  26 1.9  - -
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c 0 900     450 12000    0 .55 43 0 .019 4.9
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c 0 900     450 10000    0 .61 41 0 .023 4.8
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c 0 900     370 10000    0 .54 41 0 .019 4.9
termination-restricted-15/Ex02_false-termination_true-no-overflow.c 0 900     350 9900    0 .53 41 0 .046 4.8
termination-restricted-15/Ex03_false-termination_true-no-overflow.c 0 900     420 11000    0 .55 43 0 .018 4.9
termination-restricted-15/Ex05_false-termination_true-no-overflow.c 0 360     15000 4800    0 .54 41 0 .048 4.8
termination-restricted-15/Ex06_false-termination_true-no-overflow.c 0 900     450 9400    0 .40 43 0 .017 4.8
termination-restricted-15/Ex07_false-termination_true-no-overflow.c 0 900     6600 12000    0 .55 43 0 .046 4.8
termination-restricted-15/Ex08_false-termination_true-no-overflow.c 0 900     500 9900    0 .56 43 0 .024 4.9
termination-restricted-15/Flip2_false-termination_true-no-overflow.c 0 900     550 11000    0 .56 43 0 .023 4.9
termination-restricted-15/Flip_false-termination_true-no-overflow.c 0 900     1100 11000    0 .67 43 0 .018 4.9
termination-restricted-15/GCD2_false-termination_true-no-overflow.c 0 900     1000 11000    0 .41 41 0 .024 5.0
termination-restricted-15/GCD_false-termination_true-no-overflow.c 0 900     1900 11000    0 .53 43 0 .036 4.9
termination-restricted-15/Loop_false-termination_true-no-overflow.c 0 900     12000 9900    0 .62 44 0 .044 4.9
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c 0 900     650 13000    0 .51 41 0 .022 4.8
termination-restricted-15/NO_00_false-termination_true-no-overflow.c 0 900     12000 9900    0 .53 43 0 .023 4.8
termination-restricted-15/NO_01_false-termination_true-no-overflow.c 0 900     12000 12000    0 .54 42 0 .019 5.0
termination-restricted-15/NO_02_false-termination_true-no-overflow.c 0 900     12000 9800    0 .51 43 0 .019 5.0
termination-restricted-15/NO_03_false-termination_true-no-overflow.c 0 900     7800 13000    0 .53 43 0 .018 4.8
termination-restricted-15/NO_04_false-termination_true-no-overflow.c 0 900     12000 12000    0 .51 41 0 .019 5.0
termination-restricted-15/NO_13_false-termination_true-no-overflow.c 0 900     7800 10000    0 .53 43 0 .019 4.9
termination-restricted-15/NO_21_false-termination_true-no-overflow.c 0 900     10000 9800    0 .52 43 0 .018 4.8
termination-restricted-15/NO_22_false-termination_true-no-overflow.c 0 900     7800 14000    0 .40 43 0 .023 4.9
termination-restricted-15/NO_23_false-termination_true-no-overflow.c 0 900     4600 11000    0 .53 43 0 .025 4.8
termination-restricted-15/NO_24_false-termination_true-no-overflow.c 0 900     11000 10000    0 .55 43 0 .042 4.9
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c 0 900     480 11000    0 .56 44 0 .046 4.8
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c 0 900     650 11000    0 .52 41 0 .018 4.9
termination-restricted-15/Sunset_false-termination_true-no-overflow.c 0 900     450 13000    0 .56 43 0 .018 4.8
termination-restricted-15/Swingers_false-termination_true-no-overflow.c 0 900     5900 11000    0 .52 41 0 .021 4.8
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c 0 900     410 13000    0 .54 41 0 .050 4.9
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c 0 900     990 12000    0 .63 43 0 .024 4.9
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c 0 900     970 9200    0 .53 43 0 .022 4.9
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c 0 900     370 11000    0 .60 41 0 .023 5.0
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c 0 900     350 11000    0 .53 41 0 .018 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 60 190000 580000 2200000 56 0 30 2400 56 0 1.5 270
    correct results 30 60 270 3700 3700 0 0
        correct true 30 60 270 3700 3700 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 esbmc-incr.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.Termination-MainControlFlow