Tool ULTIMATE Automizer 0.1.23-635dfa2a CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET
Run set uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
termination-crafted/Arrays02-EquivalentConstantIndices_false-termination_true-valid-memsafety_true-no-overflow.c false(termination) 1 wit inspect 8.7 2.9 370 63 .66 0      timeout 0 --- inspect 91    82    1900 .033  0     false(termination) 1 --- inspect 7.6   4.3   310   .62 0     
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 7.1 2.6 350 58 .66 0      false(termination) 1 wit inspect 5.6  3.1  270 .033  0     false(termination) 1 --- inspect 7.2   4.5   310   .62 0     
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 8.6 3.2 370 77 .66 .0082 error (recursion) 0 --- inspect 5.4  3.0  250 .0082 .82  false(termination) 1 --- inspect 7.8   4.5   310   .62 0     
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 --- inspect 65   52   570 710 .62 0      error (invalid witness file) 0 --- inspect .62 .40 41 0      0     error (2) 0 --- inspect .022 .023 5.6 0    0     
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 7.8 2.6 370 63 .66 0      false(termination) 1 wit inspect 6.3  3.4  270 .033  0     false(termination) 1 --- inspect 6.6   4.2   300   .62 .0041
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 7.9 2.9 340 54 .66 0      false(termination) 1 --- inspect 4.6  2.5  240 .033  0     false(termination) 1 --- inspect 7.7   4.4   310   .62 0     
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 0 wit inspect 11   3.9 490 91 .66 0      error (recursion) 0 --- inspect 5.3  2.9  240 .0082 0     timeout 0 --- inspect 97     91     3700   1.2  0     
termination-crafted/Mysore_false-termination_true-valid-memsafety.c unknown 0 --- inspect 43   30   700 430 .66 0      error (invalid witness file) 0 --- inspect .75 .46 41 0      0     error (2) 0 --- inspect .047 .051 5.7 0    0     
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 8.7 3.0 360 68 .66 0      error (recursion) 0 --- inspect 4.5  2.5  250 .0082 0     false(termination) 1 --- inspect 15     8.5   490   .62 0     
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 13   5.7 500 120 .66 0      error (recursion) 0 --- inspect 4.2  2.4  250 .0082 0     false(termination) 1 --- inspect 9.4   5.4   340   .62 0     
termination-crafted/NonTermination3_false-termination_false-valid-deref.c false(termination) 1 wit inspect 17   6.9 560 150 .66 0      timeout 0 --- inspect 92    71    1900 .033  0     false(termination) 1 --- inspect 13     8.2   400   .62 .012 
termination-crafted/NonTermination3_true-no-overflow_false-termination.c false(termination) 1 wit inspect 17   7.0 520 150 .66 0      timeout 0 --- inspect 92    73    1900 .033  0     false(termination) 1 --- inspect 13     8.4   400   .62 0     
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 8.4 2.8 370 62 .66 0      false(termination) 1 wit inspect 6.9  3.7  260 .033  0     false(termination) 1 --- inspect 6.8   4.3   300   .62 0     
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 8.8 2.8 380 69 .66 0      error (recursion) 0 --- inspect 5.2  2.8  250 .0082 0     false(termination) 1 --- inspect 7.7   4.9   310   .62 0     
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 7.7 2.6 370 58 .66 0      false(termination) 1 --- inspect 4.8  2.7  240 .033  0     false(termination) 1 --- inspect 7.6   4.4   320   .66 0     
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 7.4 2.6 350 65 .66 0      false(termination) 1 --- inspect 4.6  2.6  240 .033  0     true -32 --- inspect 6.9   3.8   300   .62 0     
termination-crafted/2Nested_true-termination_true-valid-memsafety.c true 2 --- inspect 8.5 3.3 350 63 .66 0      - --- inspect - --- inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 37   20   800 360 .66 0      - --- inspect - --- inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c true 2 --- inspect 21   15   370 250 .66 0      - --- inspect - --- inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c timeout 0 --- inspect 910   250   14000 4900 .63 0      - --- inspect - --- inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   870   960 11000 .63 0      - --- inspect - --- inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   870   760 12000 .63 0      - --- inspect - --- inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 7.8 3.0 340 60 .66 0      - --- inspect - --- inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 11   3.5 460 92 .66 .0082 - --- inspect - --- inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c true 2 --- inspect 11   5.5 390 120 .66 .049  - --- inspect - --- inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 12   6.7 350 120 .66 0      - --- inspect - --- inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 10   3.8 390 75 .66 0      - --- inspect - --- inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 9.6 3.2 390 67 .66 0      - --- inspect - --- inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c unknown 0 --- inspect 67   45   1600 690 .62 0      - --- inspect - --- inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 8.8 3.3 380 74 .66 0      - --- inspect - --- inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c true 2 --- inspect 26   17   820 210 .66 0      - --- inspect - --- inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c unknown 0 --- inspect 48   32   1300 550 .62 1.2    - --- inspect - --- inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   870   760 11000 .63 0      - --- inspect - --- inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   870   750 10000 .63 0      - --- inspect - --- inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c true 2 --- inspect 9.0 3.0 380 72 .66 0      - --- inspect - --- inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 26   9.2 800 230 .66 0      - --- inspect - --- inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 53   43   710 670 .62 0      - --- inspect - --- inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 10   3.8 380 83 .66 0      - --- inspect - --- inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   720   8500 11000 .64 0      - --- inspect - --- inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c true 2 --- inspect 11   5.0 380 94 .66 0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 24   12   530 230 .62 .92   - --- inspect - --- inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 11   4.1 530 91 .66 0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 16   5.6 680 140 .66 0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   690   12000 9900 .63 0      - --- inspect - --- inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 10   3.6 440 78 .66 0      - --- inspect - --- inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 9.3 3.1 400 78 .66 0      - --- inspect - --- inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 13   4.8 550 100 .66 0      - --- inspect - --- inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c true 2 --- inspect 10   3.8 460 87 .66 0      - --- inspect - --- inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c true 2 --- inspect 14   6.0 480 110 .66 0      - --- inspect - --- inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c true 2 --- inspect 12   5.5 490 110 .66 0      - --- inspect - --- inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 --- inspect 23   15   460 260 .66 0      - --- inspect - --- inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true 2 --- inspect 22   15   610 220 .66 0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 --- inspect 9.9 3.3 380 81 .66 0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 --- inspect 9.8 3.2 380 77 .66 0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true 2 --- inspect 8.5 3.4 370 71 .66 0      - --- inspect - --- inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 17   6.4 630 140 .66 .13   - --- inspect - --- inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 --- inspect 9.4 3.7 380 74 .66 0      - --- inspect - --- inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c true 2 --- inspect 34   28   650 350 .66 0      - --- inspect - --- inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c true 2 --- inspect 31   23   730 360 .66 0      - --- inspect - --- inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 7.9 2.9 340 62 .66 0      - --- inspect - --- inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 6.8 2.9 330 55 .66 .0082 - --- inspect - --- inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true 2 --- inspect 9.1 3.6 360 76 .66 0      - --- inspect - --- inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c true 2 --- inspect 25   17   530 310 .62 0      - --- inspect - --- inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 8.7 3.0 380 62 .66 .0082 - --- inspect - --- inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 8.6 2.9 360 70 .66 0      - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.7 2.5 370 68 .66 0      false(termination) 1 wit inspect 6.6  3.6  270 .033  0     false(termination) 1 --- inspect 7.4   4.6   310   .66 0     
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.0 2.7 370 60 .66 0      false(termination) 1 wit inspect 6.1  3.3  270 .033  0     false(termination) 1 --- inspect 7.8   4.4   310   .62 0     
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.9 3.0 360 65 .66 0      false(termination) 1 wit inspect 6.9  3.8  260 .0082 .025 false(termination) 1 --- inspect 7.5   4.3   310   .62 0     
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.0 3.4 380 71 .66 0      false(termination) 1 wit inspect 5.6  3.1  250 .0082 0     false(termination) 1 --- inspect 10     6.4   350   .62 0     
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) 1 wit inspect 13   3.8 570 95 .66 0      false(termination) 1 wit inspect 6.9  3.7  300 .033  0     false(termination) 1 --- inspect 7.2   4.6   310   .62 0     
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 14   5.3 560 120 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 --- inspect 10   3.7 490 84 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 --- inspect 8.8 2.9 370 64 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 --- inspect 8.2 3.3 360 59 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 --- inspect 24   17   500 240 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 --- inspect 27   18   660 310 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 --- inspect 8.9 3.1 380 80 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 --- inspect 9.0 3.0 380 75 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c true 2 --- inspect 10   4.1 460 87 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 --- inspect 10   4.0 470 85 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c true 2 --- inspect 11   4.0 490 87 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 --- inspect 11   4.2 510 88 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 --- inspect 9.8 3.5 420 89 .66 0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 --- inspect 10   4.2 450 86 .66 0      - --- inspect - --- inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 2 --- inspect 9.5 3.3 400 78 .66 0      - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 14   6.0 500 120 .66 .26   - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 11   4.1 440 83 .66 0      - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c true 2 --- inspect 12   5.1 500 110 .66 0      - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 --- inspect 11   5.1 360 93 .66 1.2    - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 --- inspect 8.2 2.8 370 69 .66 0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 --- inspect 8.9 3.0 370 66 .66 0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c true 2 --- inspect 7.9 3.0 330 74 .66 0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 --- inspect 9.2 3.4 370 71 .66 0      - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 --- inspect 8.3 2.9 360 59 .66 0      - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 --- inspect 10   5.2 370 100 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 11   3.9 520 95 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 --- inspect 12   4.4 520 110 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 --- inspect 12   4.7 510 99 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 --- inspect 14   7.7 490 160 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 --- inspect 10   4.2 490 92 .66 0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c true 2 --- inspect 13   6.7 440 120 .66 0      - --- inspect - --- inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 --- inspect 10   4.0 470 87 .66 0      - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 47   35   550 570 .62 .13   - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 --- inspect 9.0 2.8 370 76 .66 0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 11   5.2 380 100 .66 0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 --- inspect 9.2 3.1 380 62 .66 0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 --- inspect 19   5.9 770 140 .66 0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 --- inspect 8.7 2.9 370 75 .66 0      - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 --- inspect 8.6 3.3 380 69 .66 0      - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 18   5.7 580 140 .66 0      - --- inspect - --- inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 20   12   560 200 .66 0      - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 --- inspect 46   36   640 520 .37 0      - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c unknown 0 --- inspect 38   16   2000 390 .66 .18   - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 --- inspect 9.0 2.9 380 75 .66 0      - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 --- inspect 9.5 3.7 380 77 .66 0      - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.0 370 68 .66 0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 25   18   530 290 .66 0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 8.2 2.8 360 66 .66 0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 --- inspect 9.8 3.5 450 86 .66 0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 --- inspect 10   3.6 460 81 .66 0      - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c timeout 0 --- inspect 900   720   840 12000 .64 0      - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 --- inspect 12   4.1 530 90 .66 0      - --- inspect - --- inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 --- inspect 12   4.6 470 120 .66 0      - --- inspect - --- inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 --- inspect 8.5 2.9 350 71 .66 0      - --- inspect - --- inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c true 2 --- inspect 12   4.3 560 91 .66 0      - --- inspect - --- inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c true 2 --- inspect 110   93   760 1300 .62 0      - --- inspect - --- inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c true 2 --- inspect 10   3.5 470 77 .66 0      - --- inspect - --- inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c true 2 --- inspect 20   8.7 610 180 .66 0      - --- inspect - --- inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c true 2 --- inspect 22   9.1 730 210 .66 0      - --- inspect - --- inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.0 380 68 .66 0      - --- inspect - --- inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c true 2 --- inspect 12   4.0 580 100 .66 0      - --- inspect - --- inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c true 2 --- inspect 40   18   970 380 .66 0      - --- inspect - --- inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c timeout 0 --- inspect 900   850   1100 11000 .63 0      - --- inspect - --- inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 2 --- inspect 10   4.2 480 86 .66 0      - --- inspect - --- inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout 0 --- inspect 900   370   14000 7800 .63 .11   - --- inspect - --- inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 --- inspect 8.8 3.0 380 64 .66 0      - --- inspect - --- inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c unknown 0 --- inspect 58   44   660 710 .62 0      - --- inspect - --- inspect
termination-numeric/Parts_true-termination_true-no-overflow.c true 2 --- inspect 67   35   1100 560 .62 0      - --- inspect - --- inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c true 2 --- inspect 8.8 3.0 380 69 .66 0      - --- inspect - --- inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c true 2 --- inspect 23   16   460 240 .66 0      - --- inspect - --- inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c true 2 --- inspect 14   7.6 520 150 .66 1.4    - --- inspect - --- inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 --- inspect 8.6 3.3 350 79 .66 0      - --- inspect - --- inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2 --- inspect 11   3.6 410 84 .66 0      - --- inspect - --- inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c true 2 --- inspect 12   4.5 480 89 .66 0      - --- inspect - --- inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c true 2 --- inspect 12   4.4 530 120 .66 0      - --- inspect - --- inspect
termination-numeric/twisted_true-termination_true-no-overflow.c true 2 --- inspect 11   4.1 400 110 .66 0      - --- inspect - --- inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c true 2 --- inspect 11   4.1 510 98 .66 0      - --- inspect - --- inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.0 380 78 .66 0      - --- inspect - --- inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c true 2 --- inspect 26   18   500 270 .62 0      - --- inspect - --- inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c true 2 --- inspect 23   15   530 270 .66 0      - --- inspect - --- inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 --- inspect 7.7 2.7 340 64 .66 0      - --- inspect - --- inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c true 2 --- inspect 10   3.8 450 99 .66 .19   - --- inspect - --- inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 --- inspect 11   4.3 460 94 .66 0      - --- inspect - --- inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c true 2 --- inspect 19   6.9 550 170 .66 .97   - --- inspect - --- inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 --- inspect 9.7 3.9 380 86 .66 0      - --- inspect - --- inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c true 2 --- inspect 9.3 3.4 390 73 .66 0      - --- inspect - --- inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 --- inspect 9.8 3.3 380 82 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true 2 --- inspect 14   7.4 490 150 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 --- inspect 11   3.8 460 83 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.0 370 68 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 --- inspect 8.2 3.1 360 67 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 --- inspect 8.9 3.1 370 81 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 --- inspect 10   4.0 400 88 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.5 350 78 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 --- inspect 9.3 3.3 400 80 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 --- inspect 8.3 3.0 360 65 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true 2 --- inspect 8.4 3.0 350 66 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true 2 --- inspect 11   5.9 390 100 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true 2 --- inspect 8.5 3.2 360 64 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 --- inspect 7.8 2.9 340 67 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true 2 --- inspect 11   4.3 450 93 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true 2 --- inspect 19   14   380 240 .66 0      - --- inspect - --- inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true 2 --- inspect 10   3.7 450 78 .66 0      - --- inspect - --- inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 --- inspect 9.6 3.6 380 74 .66 0      - --- inspect - --- inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 --- inspect 8.7 2.9 380 69 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 --- inspect 11   3.8 410 83 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 --- inspect 8.2 3.0 360 65 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 --- inspect 7.8 2.9 350 68 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c true 2 --- inspect 9.8 3.5 470 86 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 --- inspect 9.0 3.5 370 74 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.0 360 66 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c true 2 --- inspect 21   15   660 210 .66 0      - --- inspect - --- inspect
termination-restricted-15/a.10_true-termination.c true 2 --- inspect 14   7.5 450 140 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 --- inspect 8.1 3.4 350 74 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.3 370 68 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c true 2 --- inspect 21   15   640 190 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c true 2 --- inspect 20   15   610 200 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c true 2 --- inspect 13   6.9 380 120 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 --- inspect 9.0 3.4 380 71 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c true 2 --- inspect 8.4 3.3 350 63 .66 .0082 - --- inspect - --- inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 --- inspect 8.2 3.0 350 68 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c true 2 --- inspect 14   5.3 540 110 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true 2 --- inspect 8.8 3.1 370 66 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c true 2 --- inspect 24   18   540 210 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c true 2 --- inspect 43   36   560 520 .62 0      - --- inspect - --- inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c true 2 --- inspect 9.7 3.3 420 71 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c true 2 --- inspect 10   3.7 410 98 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 --- inspect 9.5 3.6 400 72 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 --- inspect 10   3.8 410 84 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 --- inspect 9.4 3.2 380 69 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 --- inspect 8.7 3.4 350 68 .66 0      - --- inspect - --- inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 --- inspect 9.6 3.6 390 69 .66 1.2    - --- inspect - --- inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c true 2 --- inspect 12   4.1 500 83 .66 0      - --- inspect - --- inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true 2 --- inspect 9.9 3.6 440 93 .66 0      - --- inspect - --- inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c true 2 --- inspect 11   4.0 450 100 .66 0      - --- inspect - --- inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c true 2 --- inspect 33   27   610 400 .66 0      - --- inspect - --- inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c true 2 --- inspect 8.3 2.9 360 71 .66 0      - --- inspect - --- inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 --- inspect 11   3.7 440 84 .66 0      - --- inspect - --- inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c unknown 0 --- inspect 16   4.6 610 130 .66 0      - --- inspect - --- inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c unknown 0 --- inspect 17   4.9 610 150 .66 .0082 - --- inspect - --- inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c true 2 --- inspect 8.6 3.0 370 75 .66 0      - --- inspect - --- inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 --- inspect 9.1 3.4 380 80 .66 0      - --- inspect - --- inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 --- inspect 9.7 3.7 400 78 .66 0      - --- inspect - --- inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 --- inspect 13   4.4 550 99 .66 0      - --- inspect - --- inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 --- inspect 9.6 3.3 400 75 .66 0      - --- inspect - --- inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 11   4.0 520 96 .66 0      false(termination) 1 wit inspect 9.7  5.3  330 .033  .061 false(termination) 1 --- inspect 25     20     450   .62 0     
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.7 2.7 350 59 .66 0      false(termination) 1 wit inspect 5.3  2.9  270 .033  0     false(termination) 1 --- inspect 7.7   4.2   310   .62 0     
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.1 3.4 380 71 .66 .0041 false(termination) 1 wit inspect 4.7  2.6  250 .0082 0     false(termination) 1 --- inspect 11     6.6   370   .62 0     
termination-restricted-15/Ex02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.8 3.0 380 72 .66 0      false(termination) 1 wit inspect 5.4  3.0  250 .0082 0     false(termination) 1 --- inspect 10     5.9   370   .62 0     
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.5 3.0 350 78 .66 .0082 false(termination) 1 wit inspect 5.0  2.8  260 .0082 0     false(termination) 1 --- inspect 11     6.1   370   .62 .0041
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.0 2.7 370 61 .66 0      false(termination) 1 --- inspect 4.6  2.5  240 .033  0     false(termination) 1 --- inspect 7.2   4.0   300   .66 0     
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.8 3.3 390 76 .66 .012  false(termination) 1 wit inspect 6.2  3.4  260 .0082 0     false(termination) 1 --- inspect 10     6.5   370   .24 .012 
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.6 3.3 410 77 .66 0      false(termination) 1 wit inspect 7.4  4.0  260 .0082 0     false(termination) 1 --- inspect 10     6.2   370   .62 0     
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) 1 wit inspect 28   11   820 260 .66 .18   false(termination) 1 wit inspect 79    44    2100 .0082 0     false(termination) 1 --- inspect 13     7.7   470   .62 .0041
termination-restricted-15/Flip2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 13   5.6 530 120 .66 0      false(termination) 1 wit inspect 13    6.7  450 .033  0     false(termination) 1 --- inspect 8.4   5.2   310   .66 0     
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.1 3.1 390 70 .66 0      false(termination) 1 wit inspect 5.1  2.8  270 .033  0     false(termination) 1 --- inspect 8.6   5.0   320   .62 0     
termination-restricted-15/GCD2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.1 3.1 360 69 .66 0      false(termination) 1 wit inspect 6.7  3.6  330 .033  0     false(termination) 1 --- inspect 7.5   4.3   320   .62 .0041
termination-restricted-15/GCD_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.0 2.7 370 59 .66 0      false(termination) 1 wit inspect 8.1  4.3  330 .033  0     false(termination) 1 --- inspect 7.5   4.3   320   .62 0     
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.9 3.0 370 61 .66 0      false(termination) 1 wit inspect 6.3  3.4  270 .033  0     false(termination) 1 --- inspect 7.3   4.1   310   .62 0     
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) 1 wit inspect 13   4.0 560 110 .66 0      false(termination) 1 wit inspect 8.5  4.6  300 .033  0     false(termination) 1 --- inspect 7.2   4.5   310   .62 0     
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.3 2.6 360 65 .66 0      false(termination) 1 wit inspect 6.2  3.4  260 .033  0     false(termination) 1 --- inspect 7.2   4.1   310   .62 0     
termination-restricted-15/NO_01_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.5 3.4 360 69 .66 0      false(termination) 1 wit inspect 5.7  3.1  270 .033  .033 false(termination) 1 --- inspect 7.2   4.6   310   .62 0     
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.8 2.8 370 68 .66 0      false(termination) 1 wit inspect 5.4  3.0  270 .033  0     false(termination) 1 --- inspect 7.1   4.4   310   .66 .0041
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.0 2.9 350 62 .66 0      false(termination) 1 wit inspect 8.4  4.5  290 .033  0     false(termination) 1 --- inspect 7.7   4.4   310   .62 0     
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) 1 wit inspect 11   4.2 470 98 .66 0      false(termination) 1 wit inspect 5.6  3.1  270 .033  0     false(termination) 1 --- inspect 7.6   4.7   310   .62 .0082
termination-restricted-15/NO_13_false-termination_true-no-overflow.c false(termination) 0 wit inspect 47   23   810 520 .66 0      timeout 0 --- inspect 91    73    2100 .0082 .016 timeout 0 --- inspect 97     67     3900   .65 0     
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.5 2.6 340 58 .66 0      false(termination) 1 wit inspect 5.5  3.1  260 .033  .016 false(termination) 1 --- inspect 7.0   4.0   310   .62 .0082
termination-restricted-15/NO_22_false-termination_true-no-overflow.c false(termination) 0 wit inspect 45   22   990 470 .66 0      timeout 0 --- inspect 91    74    2300 .0082 0     timeout 0 --- inspect 97     66     4300   .83 0     
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) 1 wit inspect 12   4.0 560 96 .66 0      false(termination) 1 wit inspect 7.9  4.3  350 .033  0     false(termination) 1 --- inspect 9.0   5.6   320   .62 0     
termination-restricted-15/NO_24_false-termination_true-no-overflow.c unknown 0 --- inspect 13   4.2 580 100 .66 0      error (invalid witness file) 0 --- inspect .61 .36 41 0      0     error (2) 0 --- inspect .020 .021 5.6 0    0     
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 84   53   1000 960 .62 0      timeout 0 --- inspect 92    86    340 .0082 0     false(termination) 1 --- inspect 52     39     2000   .62 0     
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c false(termination) 1 wit inspect 30   11   820 260 .66 0      timeout 0 --- inspect 91    78    770 .033  0     false(termination) 1 --- inspect 27     17     750   .62 0     
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) 1 wit inspect 15   5.9 650 160 .66 0      false(termination) 1 wit inspect 20    10    470 .033  1.1   false(termination) 1 --- inspect 9.1   5.1   320   .62 0     
termination-restricted-15/Swingers_false-termination_true-no-overflow.c unknown 0 --- inspect 26   17   540 290 .66 0      error (invalid witness file) 0 --- inspect .75 .47 41 0      0     error (2) 0 --- inspect .021 .023 5.7 0    0     
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.7 2.9 370 67 .66 0      false(termination) 1 wit inspect 8.0  4.3  340 .033  0     false(termination) 1 --- inspect 7.8   4.8   310   .66 0     
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c false(termination) 1 wit inspect 33   13   920 300 .66 0      timeout 0 --- inspect 91    60    2000 .0082 0     false(termination) 1 --- inspect 25     15     700   .62 0     
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c false(termination) 0 wit inspect 33   13   950 310 .66 0      timeout 0 --- inspect 91    59    2300 .0082 0     timeout 0 --- inspect 97     71     1700   1.5  .045 
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) 1 wit inspect 9.3 3.1 380 73 .66 0      false(termination) 1 wit inspect 5.6  3.1  260 .0082 0     false(termination) 1 --- inspect 10     6.3   360   .62 .0041
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) 1 wit inspect 8.4 3.0 360 71 .66 0      false(termination) 1 wit inspect 4.9  2.7  260 .0082 0     false(termination) 1 --- inspect 10     6.4   370   .62 0     
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 249 401 13000 8900 170000 130000 160   8.1  55 37 1200 850 29000 1.2  2.1 55 14 890   610   32000 33    .11 
    correct results 224 401 3100 1500 100000 29000 150   6.6  37 37 320 180 12000 .97 1.2 46 46 490   310   18000 28    .066
        correct true 177 354 2500 1300 81000 23000 120   6.4  0 0
        correct false 47 47 580 230 21000 5200 31   .22 37 37 320 180 12000 .97 1.2 46 46 490   310   18000 28    .066
    correct-unconfimed results 4 0 140 62 3200 1400 2.6 0    0 0
        correct-unconfirmed true 0 0 0
        correct-unconfirmed false 4 0 140 62 3200 1400 2.6 0    0 0
    incorrect results 0 0 1 -32 6.9 3.8 300 .62 0    
        incorrect true 0 0 1 -32 6.9 3.8 300 .62 0    
        incorrect false 0 0 0
score (249 tasks, max score: 443) 401 37 14
Run set uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-termination.Termination-MainControlFlow