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 20:38:57 CET 2017-12-03 03:39:33 CET 2017-12-03 03:40:31 CET
Run set esbmc-kind.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainControlFlow
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_2038.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-kind.2017-12-02_2038.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     970 11000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 5.0
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow_false-termination.c timeout 0 wit inspect 900     970 15000    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .026 4.8
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     140 11000    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 350     15000 4100    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 wit inspect .060 15 .20 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     860 11000    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.9
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     11000 9300    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 290     15000 3500    error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .024 4.8
termination-crafted/Mysore_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     210 11000    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 5.0
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 330     15000 4100    error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 320     15000 4000    error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.8
termination-crafted/NonTermination3_false-termination_false-valid-deref.c timeout 0 wit inspect 900     1600 14000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 4.9
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 0 wit inspect 900     1600 12000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     690 10000    error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1800 8600    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 5.0
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c timeout 0 wit inspect 900     3700 9500    error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .023 4.9
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c out of memory 0 wit inspect 290     15000 4100    error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .025 4.9
termination-crafted/2Nested_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     360 11000    - wit inspect - wit inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .081 27 .87 - wit inspect - wit inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     300 11000    - wit inspect - wit inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 430     15000 6000    - wit inspect - wit inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1100 12000    - wit inspect - wit inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     660 10000    - wit inspect - wit inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     95 12000    - wit inspect - wit inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .11  26 1.3  - wit inspect - wit inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     280 12000    - wit inspect - wit inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1300 9500    - wit inspect - wit inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     830 9700    - wit inspect - wit inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     810 10000    - wit inspect - wit inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     770 10000    - wit inspect - wit inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     820 11000    - wit inspect - wit inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     290 10000    - wit inspect - wit inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     260 11000    - wit inspect - wit inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     2100 11000    - wit inspect - wit inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     5100 12000    - wit inspect - wit inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     310 12000    - wit inspect - wit inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     15000 7900    - wit inspect - wit inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     1000 11000    - wit inspect - wit inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 290     15000 3700    - wit inspect - wit inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     160 12000    - wit inspect - wit inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 710     15000 6700    - wit inspect - wit inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     9100 9200    - wit inspect - wit inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 370     15000 4500    - wit inspect - wit inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 320     15000 3900    - wit inspect - wit inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     260 11000    - wit inspect - wit inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     260 11000    - wit inspect - wit inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     260 11000    - wit inspect - wit inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     510 11000    - wit inspect - wit inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     490 10000    - wit inspect - wit inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c out of memory 0 wit inspect 350     15000 3900    - wit inspect - wit inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 wit inspect 4.8   31 59    - wit inspect - wit inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     210 13000    - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c timeout 0 wit inspect 900     580 10000    - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     590 9900    - wit inspect - wit inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c timeout 0 wit inspect 900     590 10000    - wit inspect - wit inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     320 10000    - wit inspect - wit inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 wit inspect 1.0   26 12    - wit inspect - wit inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     340 10000    - wit inspect - wit inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     330 12000    - wit inspect - wit inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     600 9900    - wit inspect - wit inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .083 26 .70 - wit inspect - wit inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     140 10000    - wit inspect - wit inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     280 11000    - wit inspect - wit inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .20  26 2.3  - wit inspect - wit inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 wit inspect 900     810 12000    - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout 0 wit inspect 900     240 10000    error (invalid witness file) 0 wit inspect .66 46 error (2) 0 wit inspect .018 4.9
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout 0 wit inspect 900     990 13000    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 5.0
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout 0 wit inspect 900     1500 9800    error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c timeout 0 wit inspect 900     380 10000    error (invalid witness file) 0 wit inspect .44 42 error (2) 0 wit inspect .018 5.0
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout 0 wit inspect 900     640 11000    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     800 10000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 9700    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .21  26 2.4  - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     820 12000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 8300    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1800 11000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 9300    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect .095 26 .95 - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     480 13000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     450 12000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 9900    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1400 9900    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     320 13000    - wit inspect - wit inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout 0 wit inspect 900     320 10000    - wit inspect - wit inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     450 12000    - wit inspect - wit inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     240 10000    - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1500 12000    - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     440 11000    - wit inspect - wit inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout 0 wit inspect 900     600 11000    - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .21  26 2.5  - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     820 11000    - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 8300    - wit inspect - wit inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect .099 26 1.0  - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout 0 wit inspect 900     250 11000    - wit inspect - wit inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     340 11000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     560 11000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     620 11000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout 0 wit inspect 900     750 12000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 11000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout 0 wit inspect 900     290 10000    - wit inspect - wit inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout 0 wit inspect 900     370 9800    - wit inspect - wit inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .23  26 2.2  - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     510 9900    - wit inspect - wit inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     970 12000    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     880 11000    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 9200    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout 0 wit inspect 900     950 13000    - wit inspect - wit inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout 0 wit inspect 900     190 11000    - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 10000    - wit inspect - wit inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     440 11000    - wit inspect - wit inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     920 13000    - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c out of memory 0 wit inspect 400     15000 4200    - wit inspect - wit inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c out of memory 0 wit inspect 350     15000 3800    - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     360 10000    - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout 0 wit inspect 900     470 9800    - wit inspect - wit inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .14  26 1.9  - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 9400    - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     590 9100    - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1500 10000    - wit inspect - wit inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     550 11000    - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 wit inspect 900     6300 11000    - wit inspect - wit inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1200 11000    - wit inspect - wit inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     710 11000    - wit inspect - wit inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 4.7   30 58    - wit inspect - wit inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 0 wit inspect 900     3300 12000    - wit inspect - wit inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 11000    - wit inspect - wit inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2400 12000    - wit inspect - wit inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1700 9000    - wit inspect - wit inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1600 9900    - wit inspect - wit inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect 210     2900 2300    - wit inspect - wit inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout 0 wit inspect 900     1200 9800    - wit inspect - wit inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c out of memory 0 wit inspect 420     15000 5000    - wit inspect - wit inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 wit inspect 900     6000 12000    - wit inspect - wit inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2300 9800    - wit inspect - wit inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c out of memory 0 wit inspect 340     15000 3600    - wit inspect - wit inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 9600    - wit inspect - wit inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 2 wit inspect 43     130 570    - wit inspect - wit inspect
termination-numeric/Parts_true-termination_true-no-overflow.c timeout 0 wit inspect 900     9400 13000    - wit inspect - wit inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout 0 wit inspect 900     1200 12000    - wit inspect - wit inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout 0 wit inspect 900     990 9800    - wit inspect - wit inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c out of memory 0 wit inspect 400     15000 4100    - wit inspect - wit inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .17  26 1.6  - wit inspect - wit inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2 wit inspect .19  26 1.7  - wit inspect - wit inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2000 8300    - wit inspect - wit inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1700 8400    - wit inspect - wit inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2400 13000    - wit inspect - wit inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 10000    - wit inspect - wit inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c timeout 0 wit inspect 900     130 11000    - wit inspect - wit inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     970 11000    - wit inspect - wit inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1000 8900    - wit inspect - wit inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 wit inspect .075 26 .76 - wit inspect - wit inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c timeout 0 wit inspect 900     890 13000    - wit inspect - wit inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c timeout 0 wit inspect 900     870 10000    - wit inspect - wit inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c timeout 0 wit inspect 900     310 11000    - wit inspect - wit inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .093 26 .92 - wit inspect - wit inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 wit inspect .10  26 .80 - wit inspect - wit inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c timeout 0 wit inspect 900     290 12000    - wit inspect - wit inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1400 9500    - wit inspect - wit inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 12000    - wit inspect - wit inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c timeout 0 wit inspect 900     370 10000    - wit inspect - wit inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c timeout 0 wit inspect 900     780 10000    - wit inspect - wit inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c timeout 0 wit inspect 900     970 12000    - wit inspect - wit inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c timeout 0 wit inspect 900     790 12000    - wit inspect - wit inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 10000    - wit inspect - wit inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c timeout 0 wit inspect 900     300 12000    - wit inspect - wit inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 10000    - wit inspect - wit inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true 2 wit inspect .079 26 .72 - wit inspect - wit inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c timeout 0 wit inspect 900     500 9800    - wit inspect - wit inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c timeout 0 wit inspect 900     380 11000    - wit inspect - wit inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c timeout 0 wit inspect 900     280 11000    - wit inspect - wit inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c timeout 0 wit inspect 900     350 11000    - wit inspect - wit inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c timeout 0 wit inspect 900     590 13000    - wit inspect - wit inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 wit inspect .17  26 1.5  - wit inspect - wit inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c timeout 0 wit inspect 900     450 12000    - wit inspect - wit inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1400 8200    - wit inspect - wit inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 10000    - wit inspect - wit inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c timeout 0 wit inspect 900     290 11000    - wit inspect - wit inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c timeout 0 wit inspect 900     330 10000    - wit inspect - wit inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c timeout 0 wit inspect 900     370 9700    - wit inspect - wit inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c timeout 0 wit inspect 900     300 11000    - wit inspect - wit inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     180 10000    - wit inspect - wit inspect
termination-restricted-15/a.10_true-termination.c timeout 0 wit inspect 900     290 11000    - wit inspect - wit inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c timeout 0 wit inspect 900     300 10000    - wit inspect - wit inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c timeout 0 wit inspect 900     270 11000    - wit inspect - wit inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     170 11000    - wit inspect - wit inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     170 11000    - wit inspect - wit inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c true 2 wit inspect .088 26 .83 - wit inspect - wit inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 wit inspect .087 26 .80 - wit inspect - wit inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c timeout 0 wit inspect 900     630 11000    - wit inspect - wit inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c timeout 0 wit inspect 900     380 11000    - wit inspect - wit inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     530 12000    - wit inspect - wit inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     560 11000    - wit inspect - wit inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c timeout 0 wit inspect 900     390 9900    - wit inspect - wit inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c timeout 0 wit inspect 900     410 12000    - wit inspect - wit inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c timeout 0 wit inspect 900     490 11000    - wit inspect - wit inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c timeout 0 wit inspect 900     500 11000    - wit inspect - wit inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c timeout 0 wit inspect 900     840 12000    - wit inspect - wit inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1000 9500    - wit inspect - wit inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c timeout 0 wit inspect 900     790 11000    - wit inspect - wit inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 11000    - wit inspect - wit inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c timeout 0 wit inspect 900     930 10000    - wit inspect - wit inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2100 10000    - wit inspect - wit inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c timeout 0 wit inspect 900     2400 11000    - wit inspect - wit inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1300 9100    - wit inspect - wit inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c timeout 0 wit inspect 900     320 11000    - wit inspect - wit inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c timeout 0 wit inspect 900     440 12000    - wit inspect - wit inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c timeout 0 wit inspect 900     1400 9700    - wit inspect - wit inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c true 2 wit inspect .10  26 .88 - wit inspect - wit inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c true 2 wit inspect .12  29 1.3  - wit inspect - wit inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c timeout 0 wit inspect 900     200 10000    - wit inspect - wit inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 wit inspect .12  26 .66 - wit inspect - wit inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 wit inspect .081 26 .84 - wit inspect - wit inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 wit inspect .091 26 .91 - wit inspect - wit inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 wit inspect .18  26 1.6  - wit inspect - wit inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c timeout 0 wit inspect 900     450 10000    error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .018 4.9
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c timeout 0 wit inspect 900     440 11000    error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .025 4.8
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c timeout 0 wit inspect 900     370 10000    error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9
termination-restricted-15/Ex02_false-termination_true-no-overflow.c timeout 0 wit inspect 900     350 11000    error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8
termination-restricted-15/Ex03_false-termination_true-no-overflow.c timeout 0 wit inspect 900     420 9900    error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
termination-restricted-15/Ex05_false-termination_true-no-overflow.c out of memory 0 wit inspect 360     15000 4400    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 5.0
termination-restricted-15/Ex06_false-termination_true-no-overflow.c timeout 0 wit inspect 900     450 11000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .017 4.9
termination-restricted-15/Ex07_false-termination_true-no-overflow.c timeout 0 wit inspect 900     6500 9500    error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 4.8
termination-restricted-15/Ex08_false-termination_true-no-overflow.c timeout 0 wit inspect 900     510 11000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .049 4.9
termination-restricted-15/Flip2_false-termination_true-no-overflow.c timeout 0 wit inspect 900     550 10000    error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .018 4.8
termination-restricted-15/Flip_false-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 10000    error (invalid witness file) 0 wit inspect .44 41 error (2) 0 wit inspect .024 4.8
termination-restricted-15/GCD2_false-termination_true-no-overflow.c timeout 0 wit inspect 900     1100 9900    error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 4.9
termination-restricted-15/GCD_false-termination_true-no-overflow.c timeout 0 wit inspect 900     1900 10000    error (invalid witness file) 0 wit inspect .50 42 error (2) 0 wit inspect .026 4.9
termination-restricted-15/Loop_false-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 9800    error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .018 4.9
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c timeout 0 wit inspect 900     650 12000    error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8
termination-restricted-15/NO_00_false-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 11000    error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8
termination-restricted-15/NO_01_false-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 13000    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .023 4.8
termination-restricted-15/NO_02_false-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 11000    error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .021 4.8
termination-restricted-15/NO_03_false-termination_true-no-overflow.c timeout 0 wit inspect 900     7700 10000    error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.9
termination-restricted-15/NO_04_false-termination_true-no-overflow.c timeout 0 wit inspect 900     12000 11000    error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
termination-restricted-15/NO_13_false-termination_true-no-overflow.c timeout 0 wit inspect 900     7800 10000    error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .023 4.9
termination-restricted-15/NO_21_false-termination_true-no-overflow.c timeout 0 wit inspect 900     10000 8400    error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9
termination-restricted-15/NO_22_false-termination_true-no-overflow.c timeout 0 wit inspect 900     7800 11000    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 5.0
termination-restricted-15/NO_23_false-termination_true-no-overflow.c timeout 0 wit inspect 900     4600 11000    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9
termination-restricted-15/NO_24_false-termination_true-no-overflow.c timeout 0 wit inspect 900     11000 7800    error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 5.0
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c timeout 0 wit inspect 900     480 13000    error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .048 5.0
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c timeout 0 wit inspect 900     650 11000    error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0
termination-restricted-15/Sunset_false-termination_true-no-overflow.c timeout 0 wit inspect 900     450 11000    error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .048 4.9
termination-restricted-15/Swingers_false-termination_true-no-overflow.c timeout 0 wit inspect 900     5800 12000    error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .020 4.9
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c timeout 0 wit inspect 900     410 11000    error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .020 4.9
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c timeout 0 wit inspect 900     990 9500    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c timeout 0 wit inspect 900     950 11000    error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.8
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c timeout 0 wit inspect 900     370 12000    error (invalid witness file) 0 wit inspect .43 44 error (2) 0 wit inspect .017 5.0
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c timeout 0 wit inspect 900     350 9900    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .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.2 270
    correct results 30 60 260 3700 3100 0 0
        correct true 30 60 260 3700 3100 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-kind.sv-comp18.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainControlFlow uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.Termination-MainControlFlow