Tool 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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET
Run set cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 0 --- inspect 900   830   4300 11000 0   0   error (invalid witness file) 0 --- inspect .66 .39 41 0     0   error (2) 0 --- inspect .021 .021 5.6 0    0  
termination-crafted/Bangalore_v2_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.5 1.6 280 32 0   0   false(termination) 1 --- inspect 4.0  2.2  250 .033 0   false(termination) 1 --- inspect 7.3   4.7   300   .62 0  
termination-crafted/Binary_Search_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 5.2 2.0 310 45 0   0   error (recursion) 0 --- inspect 5.9  3.2  260 .033 0   false(termination) 1 --- inspect 10     5.8   330   .62 0  
termination-crafted/Cairo_step2_true-no-overflow_false-termination_true-valid-memsafety.c unknown 0 --- inspect 6.9 2.3 450 63 0   0   error (invalid witness file) 0 --- inspect .60 .39 41 0     0   error (2) 0 --- inspect .021 .023 5.6 0    0  
termination-crafted/Division_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.9 1.7 280 35 0   0   false(termination) 1 --- inspect 4.5  2.5  250 .033 0   false(termination) 1 --- inspect 7.6   4.3   310   .66 0  
termination-crafted/Madrid_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.6 1.6 280 33 0   0   false(termination) 1 --- inspect 3.8  2.1  240 .033 0   false(termination) 1 --- inspect 7.2   4.5   310   .62 0  
termination-crafted/MutualRecursion_1a_true-no-overflow_false-termination_true-valid-memsafety.c error (recursion) 0 --- inspect 6.8 2.4 300 65 0   0   error (invalid witness file) 0 --- inspect .57 .35 40 0     0   error (2) 0 --- inspect .045 .047 5.5 0    0  
termination-crafted/Mysore_false-termination_true-valid-memsafety.c unknown 0 --- inspect 11   3.6 720 98 0   0   error (invalid witness file) 0 --- inspect .64 .40 41 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-crafted/NestedRecursion_1a_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 5.9 2.1 320 53 0   0   false(termination) 1 --- inspect 4.1  2.2  250 .033 0   timeout 0 --- inspect 98     63     2600   1.7  0  
termination-crafted/NestedRecursion_2b_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 5.9 2.2 350 53 0   0   error (recursion) 0 --- inspect 4.7  2.6  260 .033 0   false(termination) 1 --- inspect 17     11     520   .66 0  
termination-crafted/NonTermination3_false-termination_false-valid-deref.c timeout 0 --- inspect 900   820   4400 11000 0   0   error (invalid witness file) 0 --- inspect .77 .48 41 0     0   error (2) 0 --- inspect .027 .030 5.6 0    0  
termination-crafted/NonTermination3_true-no-overflow_false-termination.c timeout 0 --- inspect 900   830   4300 11000 0   0   error (invalid witness file) 0 --- inspect .67 .42 40 0     0   error (2) 0 --- inspect .023 .025 5.6 0    0  
termination-crafted/NonTerminationSimple7_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.7 1.6 280 31 0   0   false(termination) 1 --- inspect 4.2  2.3  250 .033 0   false(termination) 1 --- inspect 7.6   4.3   310   .66 0  
termination-crafted/RecursiveNonterminating_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 4.0 1.7 280 39 0   0   false(termination) 1 --- inspect 4.7  2.6  240 .033 0   false(termination) 1 --- inspect 8.5   5.3   310   .62 0  
termination-crafted/Rotation180_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.7 1.6 280 33 0   0   false(termination) 1 --- inspect 4.4  2.5  240 .033 0   false(termination) 1 --- inspect 7.9   4.5   310   .62 0  
termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c false(termination) 1 wit inspect 3.5 1.5 270 35 0   0   false(termination) 1 --- inspect 3.8  2.1  240 .033 0   true -32 --- inspect 6.6   3.7   290   .66 0  
termination-crafted/2Nested_true-termination_true-valid-memsafety.c true 2 --- inspect 47   41   460 450 0   0   - --- inspect - --- inspect
termination-crafted/4BitCounterPointer_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 910   850   4100 12000 0   0   - --- inspect - --- inspect
termination-crafted/4NestedWith3Variables_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   720   4500 10000 0   0   - --- inspect - --- inspect
termination-crafted/Ackermann_true-termination_true-valid-memsafety.c true 2 --- inspect 6.3 2.1 350 56 0   0   - --- inspect - --- inspect
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 --- inspect 370   350   15000 4200 0   0   - --- inspect - --- inspect
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow_true-termination_true-valid-memsafety.c out of memory 0 --- inspect 380   360   15000 5100 0   0   - --- inspect - --- inspect
termination-crafted/Bangalore_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.3 1.7 290 41 0   0   - --- inspect - --- inspect
termination-crafted/Bangalore_v4_true-no-overflow_true-termination_true-valid-memsafety.c unknown 0 --- inspect 4.2 1.6 280 36 0   0   - --- inspect - --- inspect
termination-crafted/Benghazi_nondet_true-termination_true-valid-memsafety.c true 2 --- inspect 150   140   530 1700 0   0   - --- inspect - --- inspect
termination-crafted/Benghazi_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 7.9 2.6 340 68 0   0   - --- inspect - --- inspect
termination-crafted/Cairo_step2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.7 1.8 300 38 0   0   - --- inspect - --- inspect
termination-crafted/Cairo_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.6 1.8 290 45 0   0   - --- inspect - --- inspect
termination-crafted/Copenhagen_disj_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   880   1300 12000 0   0   - --- inspect - --- inspect
termination-crafted/Copenhagen_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.4 1.8 290 41 0   0   - --- inspect - --- inspect
termination-crafted/Gothenburg_true-termination_true-valid-memsafety.c true 2 --- inspect 7.0 2.3 460 64 0   0   - --- inspect - --- inspect
termination-crafted/Gothenburg_v2_true-termination_true-valid-memsafety.c true 2 --- inspect 6.4 2.2 460 53 0   0   - --- inspect - --- inspect
termination-crafted/LexIndexValue-Array_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 910   830   4400 12000 0   0   - --- inspect - --- inspect
termination-crafted/LexIndexValue-Pointer_true-termination_true-valid-memsafety.c timeout 0 --- inspect 910   830   4300 11000 0   0   - --- inspect - --- inspect
termination-crafted/Lobnya-Boolean-Reordered_true-termination_true-valid-memsafety.c unknown 0 --- inspect 6.6 2.3 470 55 0   0   - --- inspect - --- inspect
termination-crafted/McCarthy91_Iteration_true-no-overflow_true-termination_true-valid-memsafety.c timeout 0 --- inspect 900   870   2000 7000 0   0   - --- inspect - --- inspect
termination-crafted/McCarthy91_Recursion_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.5 1.8 290 40 0   0   - --- inspect - --- inspect
termination-crafted/MenloPark_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 6.4 2.2 430 57 0   0   - --- inspect - --- inspect
termination-crafted/MutualRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 --- inspect 6.7 2.4 370 57 0   0   - --- inspect - --- inspect
termination-crafted/Mysore_true-termination_true-valid-memsafety.c true 2 --- inspect 5.3 1.9 340 45 0   0   - --- inspect - --- inspect
termination-crafted/NestedRecursion_1b_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 --- inspect 5.6 2.1 300 48 0   0   - --- inspect - --- inspect
termination-crafted/NestedRecursion_1c_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 --- inspect 4.7 1.9 280 46 0   0   - --- inspect - --- inspect
termination-crafted/NestedRecursion_1d_true-no-overflow_true-termination_true-valid-memsafety.c error (recursion) 0 --- inspect 5.5 2.0 300 51 0   0   - --- inspect - --- inspect
termination-crafted/NestedRecursion_2c_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.5 1.8 290 37 0   0   - --- inspect - --- inspect
termination-crafted/Nyala-2lex_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 5.1 1.9 290 42 0   0   - --- inspect - --- inspect
termination-crafted/Parallel_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 5.2 2.0 290 46 0   0   - --- inspect - --- inspect
termination-crafted/Piecewise_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 5.5 2.0 300 49 0   0   - --- inspect - --- inspect
termination-crafted/Pure2Phase_true-termination_true-valid-memsafety.c true 2 --- inspect 6.0 2.1 340 51 0   0   - --- inspect - --- inspect
termination-crafted/Pure3Phase_true-termination_true-valid-memsafety.c true 2 --- inspect 8.9 2.8 500 83 0   0   - --- inspect - --- inspect
termination-crafted/RecursiveMultiplication_true-termination_true-valid-memsafety.c unknown 0 --- inspect 5.8 2.1 330 51 0   0   - --- inspect - --- inspect
termination-crafted/Singapore_true-termination_true-valid-memsafety.c true 2 --- inspect 7.7 2.5 460 69 0   0   - --- inspect - --- inspect
termination-crafted/Stockholm_true-termination_true-valid-memsafety.c true 2 --- inspect 5.0 1.9 300 43 0   0   - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-no-overflow_true-termination.c true 2 --- inspect 5.2 1.9 290 52 0   0   - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-termination_true-valid-memsafety.c true 2 --- inspect 5.1 1.9 290 46 0   0   - --- inspect - --- inspect
termination-crafted/SyntaxSupportPointer01_true-valid-memsafety_true-termination.c true 2 --- inspect 4.7 1.8 290 49 0   0   - --- inspect - --- inspect
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 6.1 2.1 310 56 0   0   - --- inspect - --- inspect
termination-crafted/Thun_true-termination_true-valid-memsafety.c true 2 --- inspect 5.6 2.0 310 52 0   0   - --- inspect - --- inspect
termination-crafted/Toulouse-BranchesToLoop_true-termination_true-valid-memsafety.c true 2 --- inspect 6.7 2.3 430 60 0   0   - --- inspect - --- inspect
termination-crafted/Toulouse-MultiBranchesToLoop_true-termination_true-valid-memsafety.c true 2 --- inspect 8.0 2.6 480 71 0   0   - --- inspect - --- inspect
termination-crafted/Waldkirch_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.1 1.7 280 41 0   0   - --- inspect - --- inspect
termination-crafted/WhileFalse_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 3.1 1.4 270 29 0   0   - --- inspect - --- inspect
termination-crafted/aaron2_true-termination_true-valid-memsafety.c true 2 --- inspect 5.1 1.9 300 44 0   0   - --- inspect - --- inspect
termination-crafted/aaron3_true-termination_true-valid-memsafety.c true 2 --- inspect 17   6.3 520 160 0   0   - --- inspect - --- inspect
termination-crafted/easy1_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 170   160   1400 1800 0   0   - --- inspect - --- inspect
termination-crafted/easy2_true-no-overflow_true-termination_true-valid-memsafety.c true 2 --- inspect 4.8 1.8 300 41 0   0   - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.6 280 31 0   0   false(termination) 1 --- inspect 4.9  2.7  250 .033 0   false(termination) 1 --- inspect 13     7.6   430   .62 0  
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.6 280 38 0   0   false(termination) 1 --- inspect 4.9  2.7  250 .033 0   false(termination) 1 --- inspect 7.8   4.4   310   .66 0  
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.4 1.8 290 37 0   0   false(termination) 1 --- inspect 4.6  2.5  250 .033 0   false(termination) 1 --- inspect 11     6.5   360   .62 0  
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.6 280 34 0   0   false(termination) 1 --- inspect 4.6  2.5  240 .033 0   false(termination) 1 --- inspect 11     6.1   360   .62 0  
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.6 280 36 0   0   false(termination) 1 --- inspect 3.9  2.2  250 .033 0   false(termination) 1 --- inspect 10     5.8   360   .62 0  
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 13   3.9 510 120 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c true 2 --- inspect 5.5 2.0 290 47 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c true 2 --- inspect 170   160   1400 2300 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.8 300 49 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_true-no-overflow.c true 2 --- inspect 7.4 2.4 410 60 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c true 2 --- inspect 7.9 2.6 420 69 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c true 2 --- inspect 5.0 1.9 290 42 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.8 290 49 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c unknown 0 --- inspect 6.5 2.2 450 58 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c true 2 --- inspect 7.0 2.3 380 57 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c unknown 0 --- inspect 4.2 1.7 280 37 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c true 2 --- inspect 5.3 1.9 300 46 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c true 2 --- inspect 6.5 2.2 330 53 0   0   - --- inspect - --- inspect
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c true 2 --- inspect 5.5 1.9 310 46 0   0   - --- inspect - --- inspect
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c true 2 --- inspect 6.9 2.3 400 58 0   0   - --- inspect - --- inspect
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c unknown 0 --- inspect 4.2 1.7 280 37 0   0   - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 6.4 2.2 350 55 0   0   - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c out of memory 0 --- inspect 780   740   15000 8500 0   0   - --- inspect - --- inspect
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c true 2 --- inspect 4.6 1.8 290 44 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c true 2 --- inspect 170   160   1400 1900 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 300 41 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 300 47 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.8 290 50 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c true 2 --- inspect 4.4 1.8 290 43 0   0   - --- inspect - --- inspect
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.0 300 54 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 300 46 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c true 2 --- inspect 7.1 2.3 410 61 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c true 2 --- inspect 6.6 2.2 390 58 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c true 2 --- inspect 5.0 1.9 290 42 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.9 290 42 0   0   - --- inspect - --- inspect
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c unknown 0 --- inspect 4.0 1.6 280 33 0   0   - --- inspect - --- inspect
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c out of memory 0 --- inspect 660   620   15000 7800 0   0   - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 10   3.0 510 81 0   0   - --- inspect - --- inspect
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c true 2 --- inspect 4.4 1.8 280 42 0   0   - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 44 0   0   - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 290 43 0   0   - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c unknown 0 --- inspect 5.9 2.1 450 47 0   0   - --- inspect - --- inspect
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c true 2 --- inspect 4.3 1.7 280 39 0   0   - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 300 38 0   0   - --- inspect - --- inspect
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c timeout 0 --- inspect 900   800   5100 11000 0   0   - --- inspect - --- inspect
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c timeout 0 --- inspect 900   850   5400 6800 0   0   - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.1 310 53 0   0   - --- inspect - --- inspect
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c true 2 --- inspect 5.1 1.9 290 46 0   0   - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c true 2 --- inspect 4.4 1.8 280 39 0   0   - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c true 2 --- inspect 5.1 1.9 300 46 0   0   - --- inspect - --- inspect
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c unknown 0 --- inspect 5.4 2.0 350 53 0   0   - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.0 310 45 0   0   - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c true 2 --- inspect 4.1 1.7 280 39 0   0   - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c true 2 --- inspect 5.2 1.9 300 41 0   0   - --- inspect - --- inspect
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.1 310 53 0   0   - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c out of memory 0 --- inspect 660   620   15000 7400 0   0   - --- inspect - --- inspect
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c true 2 --- inspect 11   3.8 470 110 0   0   - --- inspect - --- inspect
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c true 2 --- inspect 6.5 2.2 370 59 0   0   - --- inspect - --- inspect
termination-crafted-lit/aviad_true-termination_true-no-overflow.c unknown 0 --- inspect 25   6.6 870 190 0   0   - --- inspect - --- inspect
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c timeout 0 --- inspect 900   860   3000 13000 0   0   - --- inspect - --- inspect
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c timeout 0 --- inspect 900   860   3400 12000 0   0   - --- inspect - --- inspect
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c unknown 0 --- inspect 20   5.5 870 170 0   0   - --- inspect - --- inspect
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c timeout 0 --- inspect 900   860   3700 12000 0   0   - --- inspect - --- inspect
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c timeout 0 --- inspect 900   860   3700 13000 0   0   - --- inspect - --- inspect
termination-crafted-lit/genady_true-termination_true-no-overflow.c out of memory 0 --- inspect 670   630   15000 6900 0   0   - --- inspect - --- inspect
termination-crafted-lit/strchr_true-no-overflow_true-termination.c unknown 0 --- inspect 25   6.9 1000 210 0   0   - --- inspect - --- inspect
termination-numeric/Ackermann01_true-termination_true-no-overflow.c true 2 --- inspect 6.3 2.2 370 55 0   0   - --- inspect - --- inspect
termination-numeric/Binomial_true-termination_false-no-overflow.c error (recursion) 0 --- inspect 4.0 1.6 280 40 0   0   - --- inspect - --- inspect
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c true 2 --- inspect 4.9 1.8 300 40 0   0   - --- inspect - --- inspect
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c true 2 --- inspect 4.6 1.8 290 42 0   0   - --- inspect - --- inspect
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c true 2 --- inspect 4.9 1.8 290 49 0   0   - --- inspect - --- inspect
termination-numeric/LogRecursive_true-termination_true-no-overflow.c exception 0 --- inspect 3.6 1.5 280 33 0   0   - --- inspect - --- inspect
termination-numeric/Parts_true-termination_true-no-overflow.c error (recursion) 0 --- inspect 4.1 1.6 280 38 0   0   - --- inspect - --- inspect
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c true 2 --- inspect 4.7 1.8 290 42 0   0   - --- inspect - --- inspect
termination-numeric/TwoWay_true-termination_true-no-overflow.c unknown 0 --- inspect 7.3 2.4 490 64 0   0   - --- inspect - --- inspect
termination-numeric/gcd01_true-termination_true-no-overflow.c unknown 0 --- inspect 4.9 1.9 310 45 0   0   - --- inspect - --- inspect
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c unknown 0 --- inspect 11   3.4 520 100 0   0   - --- inspect - --- inspect
termination-numeric/recHanoi02_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 42 0   0   - --- inspect - --- inspect
termination-numeric/rec_counter1_true-termination_true-no-overflow.c error (recursion) 0 --- inspect 3.9 1.6 280 34 0   0   - --- inspect - --- inspect
termination-numeric/rec_counter3_true-termination_true-no-overflow.c error (recursion) 0 --- inspect 3.9 1.5 280 35 0   0   - --- inspect - --- inspect
termination-numeric/twisted_true-termination_true-no-overflow.c timeout 0 --- inspect 900   840   4100 12000 0   0   - --- inspect - --- inspect
termination-restricted-15/DivMinus2_true-termination_true-no-overflow.c true 2 --- inspect 6.9 2.3 350 64 0   0   - --- inspect - --- inspect
termination-restricted-15/DivMinus_true-termination_true-no-overflow.c unknown 0 --- inspect 4.8 1.8 290 42 0   0   - --- inspect - --- inspect
termination-restricted-15/GCD3_true-termination_true-no-overflow.c unknown 0 --- inspect 5.1 1.8 290 43 0   0   - --- inspect - --- inspect
termination-restricted-15/GCD4_true-termination_true-no-overflow.c unknown 0 --- inspect 4.6 1.7 300 40 0   0   - --- inspect - --- inspect
termination-restricted-15/IntPath_true-termination_true-no-overflow.c true 2 --- inspect 3.4 1.5 280 36 0   0   - --- inspect - --- inspect
termination-restricted-15/LogAG_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 340 52 0   0   - --- inspect - --- inspect
termination-restricted-15/Log_true-termination_true-no-overflow.c true 2 --- inspect 6.3 2.1 380 54 0   0   - --- inspect - --- inspect
termination-restricted-15/McCarthyIterative_true-termination_true-no-overflow.c true 2 --- inspect 9.6 4.0 460 81 0   0   - --- inspect - --- inspect
termination-restricted-15/MinusBuiltIn_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 290 45 0   0   - --- inspect - --- inspect
termination-restricted-15/MinusUserDefined_true-termination_true-no-overflow.c true 2 --- inspect 7.4 2.6 350 61 0   0   - --- inspect - --- inspect
termination-restricted-15/Nested_true-termination_true-no-overflow.c true 2 --- inspect 22   8.9 650 220 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaA10_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.8 290 45 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaA1_true-termination_true-no-overflow.c true 2 --- inspect 5.1 1.9 300 43 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaA4_true-termination_true-no-overflow.c true 2 --- inspect 4.3 1.7 290 40 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaA7_true-termination_true-no-overflow.c true 2 --- inspect 4.6 1.8 290 38 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB14_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 300 53 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB15_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.1 320 55 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB16_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 41 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB17_true-termination_true-no-overflow.c true 2 --- inspect 4.9 1.8 290 44 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB1_true-termination_true-no-overflow.c true 2 --- inspect 4.2 1.7 280 35 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB2_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.7 300 42 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB4_true-termination_true-no-overflow.c unknown 0 --- inspect 4.4 1.8 290 38 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB6_true-termination_true-no-overflow.c true 2 --- inspect 4.4 1.8 280 41 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaB7_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.7 290 42 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaC3_true-termination_true-no-overflow.c true 2 --- inspect 5.5 2.0 310 48 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaC7_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 290 38 0   0   - --- inspect - --- inspect
termination-restricted-15/PastaC9_true-termination_true-no-overflow.c true 2 --- inspect 5.5 2.0 300 48 0   0   - --- inspect - --- inspect
termination-restricted-15/Sequence_true-termination_true-no-overflow.c true 2 --- inspect 99   79   4300 1200 0   0   - --- inspect - --- inspect
termination-restricted-15/WhileDecr_true-termination_true-no-overflow.c true 2 --- inspect 4.3 1.7 290 41 0   0   - --- inspect - --- inspect
termination-restricted-15/a.01_true-termination_true-no-overflow.c true 2 --- inspect 5.7 2.1 310 46 0   0   - --- inspect - --- inspect
termination-restricted-15/a.04_true-termination_true-no-overflow.c true 2 --- inspect 4.3 1.8 280 36 0   0   - --- inspect - --- inspect
termination-restricted-15/a.05_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 41 0   0   - --- inspect - --- inspect
termination-restricted-15/a.06_true-termination_true-no-overflow.c true 2 --- inspect 5.2 1.9 310 48 0   0   - --- inspect - --- inspect
termination-restricted-15/a.07_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 43 0   0   - --- inspect - --- inspect
termination-restricted-15/a.08_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.8 290 41 0   0   - --- inspect - --- inspect
termination-restricted-15/a.09_assume_true-termination_true-no-overflow.c unknown 0 --- inspect 4.3 1.7 280 36 0   0   - --- inspect - --- inspect
termination-restricted-15/a.10_true-termination.c true 2 --- inspect 4.9 1.9 290 48 0   0   - --- inspect - --- inspect
termination-restricted-15/b.01_true-termination_true-no-overflow.c true 2 --- inspect 4.4 1.8 280 38 0   0   - --- inspect - --- inspect
termination-restricted-15/b.02_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 290 40 0   0   - --- inspect - --- inspect
termination-restricted-15/b.03-no-inv_assume_true-termination_true-no-overflow.c unknown 0 --- inspect 4.2 1.7 280 35 0   0   - --- inspect - --- inspect
termination-restricted-15/b.03_assume_true-termination_true-no-overflow.c unknown 0 --- inspect 4.2 1.7 280 40 0   0   - --- inspect - --- inspect
termination-restricted-15/b.04_true-termination_true-no-overflow.c unknown 0 --- inspect 4.5 1.9 300 48 0   0   - --- inspect - --- inspect
termination-restricted-15/b.05_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.9 310 42 0   0   - --- inspect - --- inspect
termination-restricted-15/b.06_true-termination_true-no-overflow.c true 2 --- inspect 4.6 1.8 290 38 0   0   - --- inspect - --- inspect
termination-restricted-15/b.07_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 280 39 0   0   - --- inspect - --- inspect
termination-restricted-15/b.09-no-inv_assume_true-termination_true-no-overflow.c true 2 --- inspect 4.8 1.9 290 46 0   0   - --- inspect - --- inspect
termination-restricted-15/b.09_assume_true-termination_true-no-overflow.c true 2 --- inspect 4.7 1.8 290 48 0   0   - --- inspect - --- inspect
termination-restricted-15/b.10_true-termination_true-no-overflow.c true 2 --- inspect 5.8 2.0 310 52 0   0   - --- inspect - --- inspect
termination-restricted-15/b.11_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 300 44 0   0   - --- inspect - --- inspect
termination-restricted-15/b.12_true-termination_true-no-overflow.c true 2 --- inspect 5.0 1.9 290 44 0   0   - --- inspect - --- inspect
termination-restricted-15/b.13_true-termination_true-no-overflow.c true 2 --- inspect 5.4 2.0 290 49 0   0   - --- inspect - --- inspect
termination-restricted-15/b.14_true-termination_true-no-overflow.c true 2 --- inspect 5.8 2.0 310 58 0   0   - --- inspect - --- inspect
termination-restricted-15/b.15_true-termination_true-no-overflow.c true 2 --- inspect 5.8 2.0 310 52 0   0   - --- inspect - --- inspect
termination-restricted-15/b.16_true-termination_true-no-overflow.c true 2 --- inspect 4.9 1.9 300 43 0   0   - --- inspect - --- inspect
termination-restricted-15/b.17_true-termination_true-no-overflow.c true 2 --- inspect 5.1 1.9 300 43 0   0   - --- inspect - --- inspect
termination-restricted-15/b.18_true-termination_true-no-overflow.c true 2 --- inspect 7.1 2.4 360 63 0   0   - --- inspect - --- inspect
termination-restricted-15/c.01-no-inv_true-termination_true-no-overflow.c true 2 --- inspect 110   93   4000 1200 0   0   - --- inspect - --- inspect
termination-restricted-15/c.01_assume_true-termination_true-no-overflow.c true 2 --- inspect 7.5 2.4 430 54 0   0   - --- inspect - --- inspect
termination-restricted-15/c.02_true-termination_true-no-overflow.c true 2 --- inspect 5.6 2.0 330 50 0   0   - --- inspect - --- inspect
termination-restricted-15/c.03_true-termination_true-no-overflow.c true 2 --- inspect 5.4 2.0 310 50 0   0   - --- inspect - --- inspect
termination-restricted-15/c.07_true-termination_true-no-overflow.c true 2 --- inspect 4.9 1.8 290 46 0   0   - --- inspect - --- inspect
termination-restricted-15/c.08_true-termination_true-no-overflow.c true 2 --- inspect 5.2 1.9 310 49 0   0   - --- inspect - --- inspect
termination-restricted-15/ex3a_true-termination_true-no-overflow.c exception 0 --- inspect 3.5 1.4 270 31 0   0   - --- inspect - --- inspect
termination-restricted-15/ex3b_true-termination_true-no-overflow.c exception 0 --- inspect 3.4 1.5 270 35 0   0   - --- inspect - --- inspect
termination-restricted-15/java_AG313_true-termination_true-no-overflow.c unknown 0 --- inspect 4.7 1.8 300 40 0   0   - --- inspect - --- inspect
termination-restricted-15/java_Break_true-termination_true-no-overflow.c true 2 --- inspect 4.5 1.8 290 36 0   0   - --- inspect - --- inspect
termination-restricted-15/java_Continue1_true-termination_true-no-overflow.c true 2 --- inspect 27   18   820 290 0   0   - --- inspect - --- inspect
termination-restricted-15/java_Nested_true-termination_true-no-overflow.c true 2 --- inspect 13   4.3 490 110 0   0   - --- inspect - --- inspect
termination-restricted-15/java_Sequence_true-termination_true-no-overflow.c true 2 --- inspect 100   79   3600 1100 0   0   - --- inspect - --- inspect
termination-restricted-15/AlternKonv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.9 1.9 290 44 0   0   false(termination) 1 --- inspect 4.4  2.4  250 .033 0   false(termination) 1 --- inspect 10     6.2   340   .66 0  
termination-restricted-15/ComplInterv2_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.6 280 32 0   0   false(termination) 1 --- inspect 4.0  2.2  250 .033 0   false(termination) 1 --- inspect 7.4   4.7   310   .62 0  
termination-restricted-15/ConvLower_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.7 280 34 0   0   false(termination) 1 --- inspect 4.2  2.3  240 .033 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 3.6 1.6 280 37 0   0   false(termination) 1 --- inspect 4.5  2.5  240 .033 0   false(termination) 1 --- inspect 11     6.5   380   .66 0  
termination-restricted-15/Ex03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.6 1.6 280 30 0   0   false(termination) 1 --- inspect 4.1  2.3  250 .033 0   false(termination) 1 --- inspect 11     6.3   390   .66 0  
termination-restricted-15/Ex05_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.5 1.5 280 36 0   0   false(termination) 1 --- inspect 3.8  2.1  240 .033 0   false(termination) 1 --- inspect 7.2   4.1   300   .66 0  
termination-restricted-15/Ex06_false-termination_true-no-overflow.c false(termination) 1 wit inspect 5.0 1.9 290 50 0   0   false(termination) 1 --- inspect 3.9  2.2  240 .033 0   false(termination) 1 --- inspect 10     5.6   320   .62 0  
termination-restricted-15/Ex07_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.7 1.8 290 46 0   0   false(termination) 1 --- inspect 3.9  2.1  250 .033 0   false(termination) 1 --- inspect 9.3   5.3   320   .66 0  
termination-restricted-15/Ex08_false-termination_true-no-overflow.c false(termination) 1 wit inspect 250   220   3800 3200 0   0   false(termination) 1 --- inspect 5.3  2.9  250 .033 0   false(termination) 1 --- inspect 46     26     1000   .62 0  
termination-restricted-15/Flip2_false-termination_true-no-overflow.c unknown 0 --- inspect 4.2 1.7 280 41 0   0   error (invalid witness file) 0 --- inspect .75 .45 41 0     0   error (2) 0 --- inspect .022 .024 5.6 0    0  
termination-restricted-15/Flip_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.9 1.7 280 36 0   0   false(termination) 1 --- inspect 5.0  2.7  250 .033 0   false(termination) 1 --- inspect 7.1   4.1   300   .66 0  
termination-restricted-15/GCD2_false-termination_true-no-overflow.c unknown 0 --- inspect 4.8 1.8 290 43 0   0   error (invalid witness file) 0 --- inspect .71 .45 41 0     0   error (2) 0 --- inspect .022 .025 5.6 0    0  
termination-restricted-15/GCD_false-termination_true-no-overflow.c unknown 0 --- inspect 4.8 1.9 290 43 0   0   error (invalid witness file) 0 --- inspect .67 .40 42 0     0   error (2) 0 --- inspect .021 .022 5.6 0    0  
termination-restricted-15/Loop_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.6 280 30 0   0   false(termination) 1 --- inspect 4.1  2.3  250 .033 0   false(termination) 1 --- inspect 8.2   5.0   310   .66 0  
termination-restricted-15/MirrorIntervSim_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.6 280 35 0   0   false(termination) 1 --- inspect 4.5  2.5  240 .033 0   false(termination) 1 --- inspect 10     5.9   360   .66 0  
termination-restricted-15/NO_00_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.8 1.6 280 33 0   0   false(termination) 1 --- inspect 4.4  2.5  240 .033 0   false(termination) 1 --- inspect 7.3   4.5   320   .62 0  
termination-restricted-15/NO_01_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.9 1.8 280 42 0   0   false(termination) 1 --- inspect 3.8  2.1  240 .033 0   false(termination) 1 --- inspect 7.5   4.3   310   .62 0  
termination-restricted-15/NO_02_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.6 280 34 0   0   false(termination) 1 --- inspect 4.4  2.4  240 .033 0   false(termination) 1 --- inspect 7.8   4.3   310   .62 0  
termination-restricted-15/NO_03_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.8 1.9 290 44 0   0   false(termination) 1 --- inspect 4.6  2.5  250 .033 0   false(termination) 1 --- inspect 7.6   4.3   310   .66 0  
termination-restricted-15/NO_04_false-termination_true-no-overflow.c false(termination) 1 wit inspect 4.0 1.7 280 33 0   0   false(termination) 1 --- inspect 4.2  2.4  250 .033 0   false(termination) 1 --- inspect 7.7   4.4   310   .62 0  
termination-restricted-15/NO_13_false-termination_true-no-overflow.c out of memory 0 --- inspect 770   730   15000 8500 0   0   error (invalid witness file) 0 --- inspect .58 .35 41 0     0   error (2) 0 --- inspect .022 .023 5.6 0    0  
termination-restricted-15/NO_21_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.5 1.6 280 35 0   0   false(termination) 1 --- inspect 4.8  2.6  240 .033 0   false(termination) 1 --- inspect 7.6   4.3   310   .62 0  
termination-restricted-15/NO_22_false-termination_true-no-overflow.c out of memory 0 --- inspect 770   730   15000 7700 0   0   error (invalid witness file) 0 --- inspect .73 .45 42 0     0   error (2) 0 --- inspect .022 .022 5.6 0    0  
termination-restricted-15/NO_23_false-termination_true-no-overflow.c false(termination) 1 wit inspect 6.3 2.3 320 60 0   0   false(termination) 1 --- inspect 4.0  2.2  240 .033 0   false(termination) 1 --- inspect 12     7.1   440   .66 0  
termination-restricted-15/NO_24_false-termination_true-no-overflow.c unknown 0 --- inspect 7.3 2.5 530 62 0   0   error (invalid witness file) 0 --- inspect .61 .37 42 0     0   error (2) 0 --- inspect .022 .025 5.8 0    0  
termination-restricted-15/NarrowKonv_false-termination_true-no-overflow.c timeout 0 --- inspect 900   870   3800 8800 0   0   error (invalid witness file) 0 --- inspect .67 .42 40 0     0   error (2) 0 --- inspect .022 .024 5.7 0    0  
termination-restricted-15/Narrowing_false-termination_true-no-overflow.c timeout 0 --- inspect 900   870   1200 9400 0   0   error (invalid witness file) 0 --- inspect .61 .39 41 0     0   error (2) 0 --- inspect .021 .023 5.7 0    0  
termination-restricted-15/Sunset_false-termination_true-no-overflow.c false(termination) 1 wit inspect 7.5 2.5 390 66 0   0   false(termination) 1 --- inspect 4.2  2.3  250 .033 0   false(termination) 1 --- inspect 22     13     590   .62 0  
termination-restricted-15/Swingers_false-termination_true-no-overflow.c unknown 0 --- inspect 7.7 2.6 540 68 0   0   error (invalid witness file) 0 --- inspect .73 .45 42 0     0   error (2) 0 --- inspect .051 .052 5.5 0    0  
termination-restricted-15/TwoFloatInterv_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.6 1.6 280 37 0   0   false(termination) 1 --- inspect 4.4  2.4  240 .033 0   false(termination) 1 --- inspect 8.0   4.5   310   .62 0  
termination-restricted-15/UpAndDownIneq_false-termination_true-no-overflow.c false(termination) 1 wit inspect 310   270   3900 3900 0   0   false(termination) 1 --- inspect 5.5  3.0  250 .033 0   false(termination) 1 --- inspect 37     21     1000   .62 0  
termination-restricted-15/UpAndDown_false-termination_true-no-overflow.c false(termination) 1 wit inspect 300   260   3900 3800 0   0   false(termination) 1 --- inspect 5.1  2.7  250 .033 0   false(termination) 1 --- inspect 39     22     1100   .62 0  
termination-restricted-15/WhilePart_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.7 280 34 0   0   false(termination) 1 --- inspect 4.6  2.6  240 .033 0   false(termination) 1 --- inspect 10     6.4   360   .66 0  
termination-restricted-15/WhileSingle_false-termination_true-no-overflow.c false(termination) 1 wit inspect 3.7 1.7 270 31 0   0   false(termination) 1 --- inspect 4.2  2.3  250 .033 0   false(termination) 1 --- inspect 11     6.3   380   .66 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 320 24000 22000 290000 290000 0   0   55 38 190 100 10000 1.3 0   55 6 560   340   18000 27    0  
    correct results 180 320 2800 2000 83000 31000 0   0   38 38 170 92 9400 1.2 0   38 38 460   270   15000 24    0  
        correct true 140 280 1800 1200 61000 19000 0   0   0 0
        correct false 40 40 1000 820 22000 12000 0   0   38 38 170 92 9400 1.2 0   38 38 460   270   15000 24    0  
    incorrect results 0 0 1 -32 6.6 3.7 290 .66 0  
        incorrect true 0 0 1 -32 6.6 3.7 290 .66 0  
        incorrect false 0 0 0
score (249 tasks, max score: 443) 320 38 6
Run set cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-termination.Termination-MainControlFlow