Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098]
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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET
Run set symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow
Options --witness witness.graphml -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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 timeout (verification) 0 --- inspect 900    900    63 9800   .025  0      error (invalid witness file) 0 --- inspect .61 .36 42 0     0     error (2) 0 --- inspect .021 .022 5.7 0    0  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    75 14000   .016  0      error (invalid witness file) 0 --- inspect .60 .37 40 0     0     error (2) 0 --- inspect .021 .023 5.7 0    0  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    93 12000   .025  0      error (invalid witness file) 0 --- inspect .66 .40 40 0     0     error (2) 0 --- inspect .023 .026 5.6 0    0  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    260 12000   .025  0      error (invalid witness file) 0 --- inspect .56 .34 40 0     0     error (2) 0 --- inspect .023 .024 5.6 0    0  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    1100 11000   .016  0      error (invalid witness file) 0 --- inspect .60 .38 41 0     0     error (2) 0 --- inspect .022 .025 5.7 0    0  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .13 .13 15 1.6 .0082 0      false(termination) 1 --- inspect 3.9  2.1  240 .033 .041 true -32 --- inspect 6.3   3.9   290   .62 0  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    850 9200   .025  0      error (invalid witness file) 0 --- inspect .76 .46 40 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-crafted/Mysore_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    19 11000   .016  0      error (invalid witness file) 0 --- inspect .70 .43 41 0     0     error (2) 0 --- inspect .024 .024 5.6 0    0  
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    7600 12000   .041  0      error (invalid witness file) 0 --- inspect .56 .34 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    5000 9700   .074  0      error (invalid witness file) 0 --- inspect .69 .43 40 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-crafted/NonTermination3_false-termination_false-valid-deref.c timeout (verification) 0 --- inspect 900    900    170 11000   .025  0      error (invalid witness file) 0 --- inspect .61 .38 41 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout (verification) 0 --- inspect 900    900    150 8100   .012  0      error (invalid witness file) 0 --- inspect .59 .37 41 0     0     error (2) 0 --- inspect .023 .024 5.6 0    0  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    18 13000   .016  0      error (invalid witness file) 0 --- inspect .57 .35 40 0     0     error (2) 0 --- inspect .022 .023 5.8 0    0  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    51 13000   .025  0      error (invalid witness file) 0 --- inspect .62 .38 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .16 .16 17 2.1 .016  0      false(termination) 1 --- inspect 3.7  2.1  250 .033 0     true -32 --- inspect 6.7   3.7   300   .62 0  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect .13 .12 15 1.2 .0082 0      false(termination) 1 --- inspect 3.9  2.1  250 .033 0     true -32 --- inspect 6.4   4.1   290   .62 0  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    300 7600   .025  0      - --- inspect - --- inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .11 .11 15 1.2 0      .28   - --- inspect - --- inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    200 5800   .012  0      - --- inspect - --- inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 530    540    15000 8700   .066  .0041 - --- inspect - --- inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .14 .14 17 1.6 0      0      - --- inspect - --- inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    210 9900   .020  0      - --- inspect - --- inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    71 12000   .016  0      - --- inspect - --- inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .16 .15 19 1.6 0      0      - --- inspect - --- inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    140 9500   .016  0      - --- inspect - --- inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    520 6400   .025  0      - --- inspect - --- inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    560 10000   .025  0      - --- inspect - --- inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    610 8000   .016  0      - --- inspect - --- inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    620 5900   .025  0      - --- inspect - --- inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    580 6200   .016  0      - --- inspect - --- inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    330 6200   .025  0      - --- inspect - --- inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    2800 6700   .025  0      - --- inspect - --- inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    2800 7000   .033  0      - --- inspect - --- inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    440 6800   .025  0      - --- inspect - --- inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    110 9800   .025  0      - --- inspect - --- inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    270 11000   .025  0      - --- inspect - --- inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    530 7800   .025  0      - --- inspect - --- inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    470 12000   .020  0      - --- inspect - --- inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    100 11000   .016  0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    800 10000   .025  0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    560 8500   .025  0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    640 7000   .025  0      - --- inspect - --- inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    1300 11000   .025  0      - --- inspect - --- inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    3200 11000   .029  0      - --- inspect - --- inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12 .12 16 1.4 0      0      - --- inspect - --- inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    300 14000   .025  0      - --- inspect - --- inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    460 8200   .025  0      - --- inspect - --- inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    90 11000   .012  0      - --- inspect - --- inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    660 12000   .025  0      - --- inspect - --- inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 wit inspect 36    36    56 480   0      0      - --- inspect - --- inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    500 7100   .025  0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 wit inspect .12 .12 15 1.4 0      0      - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c timeout (verification) 0 --- inspect 900    900    530 8700   .029  0      - --- inspect - --- inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    310 12000   .025  0      - --- inspect - --- inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 wit inspect .94 .94 23 13   0      0      - --- inspect - --- inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    170 11000   .016  0      - --- inspect - --- inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    150 12000   .016  0      - --- inspect - --- inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .15 .15 16 1.3 0      0      - --- inspect - --- inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12 .12 16 1.1 0      0      - --- inspect - --- inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    210 13000   .025  0      - --- inspect - --- inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c timeout (verification) 0 --- inspect 900    900    420 12000   .025  0      - --- inspect - --- inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .12 .12 16 1.4 0      0      - --- inspect - --- inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 wit inspect .13 .13 15 1.5 0      0      - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    62 12000   .025  0      error (invalid witness file) 0 --- inspect .73 .44 41 0     0     error (2) 0 --- inspect .020 .022 5.6 0    0  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    65 10000   .025  0      error (invalid witness file) 0 --- inspect .61 .37 41 0     0     error (2) 0 --- inspect .024 .025 5.6 0    0  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    200 7400   .025  0      error (invalid witness file) 0 --- inspect .59 .36 40 0     0     error (2) 0 --- inspect .035 .037 5.6 0    0  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 290    300    15000 4200   .13   .0041 error (invalid witness file) 0 --- inspect .80 .48 42 0     0     error (2) 0 --- inspect .021 .025 5.6 0    0  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    180 9000   .025  0      error (invalid witness file) 0 --- inspect .59 .36 41 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    3100 10000   .029  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 17 1.3 0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 wit inspect .15 .15 16 1.4 0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 15 1.5 0      .41   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    310 12000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    100 11000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    430 13000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 wit inspect 23    23    120 310   0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    470 6400   .025  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    630 6100   .016  0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.6 0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 15 1.4 0      0      - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    53 10000   .012  0      - --- inspect - --- inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    460 8000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    63 11000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 15 1.3 0      0      - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    130 9900   .025  0      - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    470 8000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.4 0      0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    1800 11000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 wit inspect 23    23    120 280   0      0      - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    500 4900   .012  0      - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    470 6900   .020  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2800 10000   .029  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2600 9600   .025  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2800 8600   .029  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 9900   .016  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    100 11000   .016  0      - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    140 9800   .012  0      - --- inspect - --- inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c true 2 wit inspect .11 .10 14 1.2 0      0      - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2900 8300   .029  0      - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    460 7600   .025  0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    520 6900   .025  0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    520 7000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    79 11000   .012  0      - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    98 9800   .016  0      - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    130 10000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    140 8100   .012  0      - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    440 7500   .025  0      - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    470 11000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    130 11000   .016  0      - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    42 14000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c true 2 wit inspect .43 .43 18 5.6 0      0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    320 12000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.4 0      0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.3 0      0      - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2900 9500   .025  0      - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.3 0      0      - --- inspect - --- inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2900 9300   .033  0      - --- inspect - --- inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c true 2 wit inspect 590    590    120 5800   0      0      - --- inspect - --- inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 12000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    330 11000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    420 12000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    410 13000   .033  0      - --- inspect - --- inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    420 12000   .025  0      - --- inspect - --- inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 15 1.3 0      .28   - --- inspect - --- inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c timeout (verification) 0 --- inspect 900    900    480 11000   .025  0      - --- inspect - --- inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 830    840    15000 11000   .033  0      - --- inspect - --- inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c true 2 wit inspect 2.0  2.0  110 30   0      0      - --- inspect - --- inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    1700 13000   .025  0      - --- inspect - --- inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    14000 8600   .053  0      - --- inspect - --- inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 wit inspect .15 .14 18 2.1 0      0      - --- inspect - --- inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c true 2 wit inspect 21    21    160 250   0      0      - --- inspect - --- inspect
termination-numeric/Parts_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    10000 11000   .045  0      - --- inspect - --- inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c timeout (verification) 0 --- inspect 900    900    460 8000   .025  0      - --- inspect - --- inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    430 6500   .025  0      - --- inspect - --- inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    50 12000   .012  0      - --- inspect - --- inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .38 .38 17 5.0 0      0      - --- inspect - --- inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2 wit inspect .40 .40 18 4.5 0      0      - --- inspect - --- inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    960 12000   .025  0      - --- inspect - --- inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    800 13000   .025  0      - --- inspect - --- inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    1300 11000   .025  0      - --- inspect - --- inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    410 8500   .025  0      - --- inspect - --- inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    92 13000   .016  0      - --- inspect - --- inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    64 12000   .037  0      - --- inspect - --- inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    66 12000   .012  0      - --- inspect - --- inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 wit inspect .14 .14 17 1.7 0      0      - --- inspect - --- inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c true 2 wit inspect .23 .23 18 3.2 0      0      - --- inspect - --- inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 wit inspect .18 .18 17 1.9 0      0      - --- inspect - --- inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    96 9500   .012  0      - --- inspect - --- inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 wit inspect .18 .18 17 1.8 0      0      - --- inspect - --- inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    420 8200   .025  0      - --- inspect - --- inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 wit inspect .11 .11 15 1.2 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    41 12000   .016  0      - --- inspect - --- inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.6 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 wit inspect .13 .12 16 1.3 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 wit inspect .16 .16 17 2.2 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 wit inspect .28 .28 18 3.3 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.6 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 wit inspect .14 .14 15 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    490 6200   .016  0      - --- inspect - --- inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c true 2 wit inspect .15 .15 18 1.8 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    530 6700   .025  0      - --- inspect - --- inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.4 0      0      - --- inspect - --- inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 13000   .025  0      - --- inspect - --- inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    570 6600   .025  0      - --- inspect - --- inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    2800 8700   .029  0      - --- inspect - --- inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 wit inspect .11 .10 15 1.2 0      0      - --- inspect - --- inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.1 0      0      - --- inspect - --- inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 wit inspect .14 .14 15 1.4 0      0      - --- inspect - --- inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.3 0      0      - --- inspect - --- inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.4 0      0      - --- inspect - --- inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    450 8000   .025  0      - --- inspect - --- inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.3 0      0      - --- inspect - --- inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    580 6100   .025  0      - --- inspect - --- inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 8900   .016  0      - --- inspect - --- inspect
termination-restricted-15/a.10_true-termination.c timeout (verification) 0 --- inspect 900    900    42 12000   .016  0      - --- inspect - --- inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.8 0      0      - --- inspect - --- inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    500 7400   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    110 11000   .016  0      - --- inspect - --- inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 11000   .016  0      - --- inspect - --- inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c true 2 wit inspect .15 .15 18 1.7 0      0      - --- inspect - --- inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 wit inspect .16 .16 18 2.1 0      0      - --- inspect - --- inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    530 7800   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 wit inspect .13 .12 15 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    240 7800   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 9100   .016  0      - --- inspect - --- inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    210 7800   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    150 7400   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    460 6400   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    480 6800   .025  0      - --- inspect - --- inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 wit inspect .15 .15 17 1.7 0      0      - --- inspect - --- inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 wit inspect .29 .29 18 2.9 0      0      - --- inspect - --- inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 wit inspect .13 .13 16 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 15 1.7 0      0      - --- inspect - --- inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 wit inspect .18 .17 18 2.1 0      0      - --- inspect - --- inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    300 11000   .025  0      - --- inspect - --- inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    300 13000   .025  0      - --- inspect - --- inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    510 6000   .025  0      - --- inspect - --- inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    170 11000   .025  0      - --- inspect - --- inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    620 7700   .025  0      - --- inspect - --- inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.7 0      0      - --- inspect - --- inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c true 2 wit inspect .29 .29 31 3.7 0      0      - --- inspect - --- inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c true 2 wit inspect 1.5  1.5  46 18   0      .41   - --- inspect - --- inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    80 14000   .016  0      - --- inspect - --- inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 wit inspect .11 .11 15 1.2 0      0      - --- inspect - --- inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 wit inspect .11 .11 15 1.5 0      0      - --- inspect - --- inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 wit inspect .12 .12 16 1.2 0      0      - --- inspect - --- inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 wit inspect .11 .11 15 1.2 0      0      - --- inspect - --- inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    110 11000   .025  1.5    error (invalid witness file) 0 --- inspect .68 .43 40 0     0     error (2) 0 --- inspect .030 .032 5.6 0    0  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    18 12000   .016  0      error (invalid witness file) 0 --- inspect .59 .36 41 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    51 11000   .016  0      error (invalid witness file) 0 --- inspect .67 .41 41 0     0     error (2) 0 --- inspect .023 .024 5.6 0    0  
termination-restricted-15/Ex02_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    51 11000   .016  0      error (invalid witness file) 0 --- inspect .61 .39 41 0     0     error (2) 0 --- inspect .030 .033 5.6 0    0  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    45 12000   .012  0      error (invalid witness file) 0 --- inspect .71 .44 40 0     0     error (2) 0 --- inspect .023 .024 5.6 0    0  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 1 wit inspect .14 .14 15 1.6 .016  0      false(termination) 1 --- inspect 3.5  2.0  240 .033 0     true -32 --- inspect 6.2   3.7   290   .62 0  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    170 9900   .025  0      error (invalid witness file) 0 --- inspect .69 .42 41 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 14000   .016  0      error (invalid witness file) 0 --- inspect .69 .42 40 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    75 9900   .012  0      error (invalid witness file) 0 --- inspect .59 .38 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    52 12000   .016  0      error (invalid witness file) 0 --- inspect .78 .48 42 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/Flip_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 780    780    15000 11000   .061  .0041 error (invalid witness file) 0 --- inspect .58 .35 41 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    49 12000   .012  0      error (invalid witness file) 0 --- inspect .75 .45 42 0     0     error (2) 0 --- inspect .023 .025 5.6 0    0  
termination-restricted-15/GCD_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    92 12000   .012  0      error (invalid witness file) 0 --- inspect .60 .37 41 0     0     error (2) 0 --- inspect .022 .023 5.8 0    0  
termination-restricted-15/Loop_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    14 12000   .016  0      error (invalid witness file) 0 --- inspect .62 .37 40 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    180 11000   .020  0      error (invalid witness file) 0 --- inspect .59 .37 42 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 13000   .016  0      error (invalid witness file) 0 --- inspect .74 .46 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/NO_01_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 15000   .016  0      error (invalid witness file) 0 --- inspect .60 .36 42 0     0     error (2) 0 --- inspect .020 .021 5.6 0    0  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 12000   .016  0      error (invalid witness file) 0 --- inspect .59 .37 40 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 13000   .016  0      error (invalid witness file) 0 --- inspect .64 .39 42 0     0     error (2) 0 --- inspect .024 .025 5.6 0    0  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 13000   .016  0      error (invalid witness file) 0 --- inspect .70 .45 41 0     0     error (2) 0 --- inspect .022 .022 5.6 0    0  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 290    300    15000 4200   .082  0      error (invalid witness file) 0 --- inspect .63 .39 40 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/NO_21_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    16 12000   .016  0      error (invalid witness file) 0 --- inspect .68 .42 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 13000   .0041 0      error (invalid witness file) 0 --- inspect .62 .38 41 0     0     error (2) 0 --- inspect .021 .023 5.6 0    0  
termination-restricted-15/NO_23_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    15 11000   .016  0      error (invalid witness file) 0 --- inspect .63 .39 41 0     0     error (2) 0 --- inspect .022 .022 5.6 0    0  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 2600   .23   .0041 error (invalid witness file) 0 --- inspect .59 .37 42 0     0     error (2) 0 --- inspect .022 .025 5.6 0    0  
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 2100   .11   0      error (invalid witness file) 0 --- inspect .77 .48 40 0     0     error (2) 0 --- inspect .021 .022 5.7 0    0  
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    97 9700   .016  0      error (invalid witness file) 0 --- inspect .59 .37 40 0     0     error (2) 0 --- inspect .020 .020 5.6 0    0  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    67 13000   .016  0      error (invalid witness file) 0 --- inspect .63 .39 41 0     0     error (2) 0 --- inspect .024 .025 5.6 0    0  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 170    180    15000 2300   .11   0      error (invalid witness file) 0 --- inspect .80 .48 41 0     0     error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    100 9100   .012  0      error (invalid witness file) 0 --- inspect .56 .35 40 0     0     error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    75 9500   .012  0      error (invalid witness file) 0 --- inspect .59 .38 42 0     0     error (2) 0 --- inspect .022 .023 5.7 0    0  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    120 8500   .025  0      error (invalid witness file) 0 --- inspect .72 .44 42 0     0     error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c probably out of memory (killed (signal 9, verification)) 0 --- inspect 290    300    15000 3900   .11   .0041 error (invalid witness file) 0 --- inspect .57 .36 41 0     0     error (2) 0 --- inspect .022 .025 5.6 0    0  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c timeout (verification) 0 --- inspect 900    900    48 12000   .012  0      error (invalid witness file) 0 --- inspect .63 .39 40 0     0     error (2) 0 --- inspect .021 .024 5.6 0    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 154 150000    150000    250000 1700000   4.5   2.9 55 4 48 29   3100 .13 .041 55 -128 27 17 1500 2.5 0  
    correct results 79 154 710    710    1900 7300   .049 1.4 4 4 15 8.3 980 .13 .041 0
        correct true 75 150 710    710    1900 7300   0     1.4 0 0
        correct false 4 4 .56 .56 62 6.4 .049 0   4 4 15 8.3 980 .13 .041 0
    incorrect results 0 0 4 -128 26 15 1200 2.5 0  
        incorrect true 0 0 4 -128 26 15 1200 2.5 0  
        incorrect false 0 0 0
score (249 tasks, max score: 443) 154 4 -128
Run set symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-termination.Termination-MainControlFlow