Tool ULTIMATE Kojak f7c3ed31
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-14 07:32:15 CET [[ 2017-01-15 06:03:36 CET ]] [[ 2017-01-15 06:19:08 CET ]] [[ 2017-01-15 06:04:26 CET ]] [[ 2017-01-15 06:20:07 CET ]]
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
signedintegeroverflow-regression/AdditionIntMax_false-no-overflow.c.i 5.5 1.8 42 330 2.5 0      4.0  2.2  76   260 6.9 3.7 140 310
signedintegeroverflow-regression/AdditionIntMin_false-no-overflow.c.i 5.5 1.8 41 330 2.5 0      4.8  2.6  56   250 7.4 4.0 130 320
signedintegeroverflow-regression/Division_false-no-overflow.c.i 5.6 1.8 46 320 2.6 0      4.1  2.3  76   250 7.4 3.9 160 310
signedintegeroverflow-regression/Multiplication_false-no-overflow.c.i 5.4 1.8 43 310 2.5 0      3.7  2.1  61   240 6.8 3.7 150 300
signedintegeroverflow-regression/NoConversion_false-no-overflow.c.i 5.2 1.7 48 310 2.5 0      4.7  2.6  57   260 7.0 3.7 140 310
signedintegeroverflow-regression/PostfixDecrement_false-no-overflow.c.i 7.0 1.9 52 350 2.5 0      4.2  2.3  81   250 7.2 3.9 150 310
signedintegeroverflow-regression/PostfixIncrement_false-no-overflow.c.i 5.9 1.8 44 330 2.5 0      4.2  2.3  70   260 8.1 4.3 160 330
signedintegeroverflow-regression/PrefixDecrement_false-no-overflow.c.i 5.4 1.8 47 330 2.5 0      3.9  2.2  72   240 7.4 4.0 160 320
signedintegeroverflow-regression/PrefixIncrement_false-no-overflow.c.i 5.4 1.8 46 320 2.5 0      3.9  2.2  65   240 7.5 4.0 150 320
signedintegeroverflow-regression/UnaryMinus_false-no-overflow.c.i 5.4 1.8 39 320 2.5 0      3.9  2.2  72   260 7.5 4.0 150 320
signedintegeroverflow-regression/ConversionToSignedInt_true-no-overflow.c.i 5.5 1.7 43 320 2.5 0      3.9  2.2  48   260 6.7 3.6 130 310
signedintegeroverflow-regression/IntegerPromotion_true-no-overflow.c.i 6.1 1.9 48 320 2.5 0      3.9  2.2  63   260 7.6 4.1 140 320
signedintegeroverflow-regression/Multiplication_true-no-overflow.c.i 6.2 1.8 44 330 2.5 0      3.9  2.2  53   260 7.1 3.8 140 310
signedintegeroverflow-regression/NoNegativeIntegerConstant_true-no-overflow.c.i 6.0 1.8 44 330 2.5 0      3.8  2.1  57   260 7.0 3.7 130 310
signedintegeroverflow-regression/UsualArithmeticConversions_true-no-overflow.c.i 5.2 1.7 45 320 2.5 0      3.8  2.2  82   250 7.0 3.7 130 310
termination-crafted/2Nested_false-no-overflow.c 5.5 1.8 45 320 2.5 0      3.0  1.7  59   230 7.2 3.8 140 310
termination-crafted/4NestedWith3Variables_false-no-overflow.c 5.6 1.8 44 330 2.5 0      3.0  1.7  58   240 7.5 4.0 160 310
termination-crafted/Ackermann_false-no-overflow.c 6.2 1.8 49 350 2.5 0      3.2  1.8  64   240 7.4 4.0 140 320
termination-crafted/Bangalore_false-no-overflow.c 5.3 1.7 43 320 2.5 0      3.0  1.7  64   230 7.0 3.8 100 310
termination-crafted/Bangalore_v3_false-no-overflow.c 5.3 1.8 43 320 2.5 0      2.9  1.7  39   230 7.6 4.0 110 320
termination-crafted/Benghazi_nondet_false-no-overflow.c 5.6 1.7 47 320 2.5 0      3.3  1.8  61   240 7.5 3.9 160 310
termination-crafted/Binary_Search_false-no-overflow.c 5.8 1.9 52 320 2.5 0      3.2  1.8  74   240 8.7 4.6 160 340
termination-crafted/Cairo_nondet_false-no-overflow.c 6.0 1.9 47 320 2.5 0      3.7  2.1  51   240 7.7 4.1 160 320
termination-crafted/Collatz_unknown-termination_false-no-overflow.c 5.4 1.8 47 330 2.5 0      3.1  1.8  61   240 7.1 3.8 130 310
termination-crafted/Copenhagen_disj_false-no-overflow.c 5.7 1.8 45 320 2.5 0      3.2  1.8  60   240 7.7 4.1 160 330
termination-crafted/Gothenburg_false-no-overflow.c 5.7 1.9 45 320 2.5 0      3.2  1.8  67   240 7.5 4.0 160 320
termination-crafted/Gothenburg_v2_false-no-overflow.c 5.6 1.8 47 330 2.5 0      3.1  1.7  49   230 7.2 3.9 160 320
termination-crafted/Hanoi_2vars_false-no-overflow.c 5.4 1.7 41 320 2.5 0      3.1  1.8  69   240 7.3 3.9 150 310
termination-crafted/Hanoi_3vars_false-no-overflow.c 5.5 1.8 40 320 2.5 0      3.1  1.8  64   230 7.7 4.1 150 320
termination-crafted/Hanoi_plus_false-no-overflow.c 5.4 1.8 41 320 2.5 0      3.0  1.7  58   230 7.8 4.1 160 320
termination-crafted/Lobnya-Boolean-Reordered_false-no-overflow.c 5.9 1.9 46 330 2.5 0      3.1  1.8  50   240 7.5 4.1 160 320
termination-crafted/Mysore_false-no-overflow.c 5.6 1.8 44 320 2.5 0      3.1  1.8  67   240 7.4 3.9 150 310
termination-crafted/NestedRecursion_1a_false-no-overflow.c 6.2 1.9 48 340 2.5 0      3.5  2.0  63   250 8.1 4.3 170 330
termination-crafted/NestedRecursion_2a_false-no-overflow.c 6.9 2.0 52 340 2.5 0      3.1  1.8  73   250 7.5 4.1 150 320
termination-crafted/NonTermination1_false-no-overflow.c 5.2 1.8 42 320 2.5 0      3.3  1.8  62   230 7.2 3.9 150 310
termination-crafted/NonTermination2_false-no-overflow.c 6.0 1.9 44 330 2.5 0      3.1  1.8  65   230 7.8 4.1 150 320
termination-crafted/NonTermination4_false-no-overflow.c 290   230   4600 1800 2.5 0      3.9  2.2  55   250 9.8 5.1 170 350
termination-crafted/NonTerminationSimple2_false-no-overflow.c 5.4 1.7 39 320 2.5 0      3.1  1.8  67   230 7.0 3.8 140 310
termination-crafted/NonTerminationSimple3_false-no-overflow.c 5.5 1.8 39 320 2.5 0      2.9  1.6  55   230 7.1 3.8 150 310
termination-crafted/NonTerminationSimple4_false-no-overflow.c 900   750   13000 1900 2.3 0      .50 .33 12   40 6.5 3.4 130 310
termination-crafted/NonTerminationSimple5_false-no-overflow.c 5.3 1.7 42 320 2.5 0      3.1  1.8  65   230 6.7 3.6 130 310
termination-crafted/NonTerminationSimple6_false-no-overflow.c 5.5 1.8 45 320 2.5 0      3.1  1.8  62   240 7.2 3.9 140 310
termination-crafted/NonTerminationSimple8_false-no-overflow.c 5.6 1.8 47 320 2.5 0      4.0  2.3  39   240 7.9 4.2 150 330
termination-crafted/NonTerminationSimple9_false-no-overflow.c 5.5 1.8 38 320 2.5 0      3.5  2.0  72   250 6.5 3.5 130 300
termination-crafted/Pure2Phase_false-no-overflow.c 6.5 1.9 51 350 2.5 0      3.1  1.8  71   230 7.3 3.9 140 320
termination-crafted/Pure3Phase_false-no-overflow.c 5.4 1.8 40 320 2.5 0      3.2  1.9  73   240 7.3 3.9 150 310
termination-crafted/RecursiveMultiplication_false-no-overflow.c 6.2 1.8 48 330 2.5 0      3.2  1.8  60   250 7.5 4.0 160 320
termination-crafted/RecursiveNonterminating_false-no-overflow.c 5.3 1.7 44 320 2.5 0      3.2  1.8  63   240 8.0 4.2 140 330
termination-crafted/Rotation180_false-no-overflow.c 5.5 1.8 44 320 2.5 0      2.9  1.6  41   230 6.8 3.7 150 320
termination-crafted/Singapore_false-no-overflow.c 5.5 1.8 47 320 2.5 0      3.9  2.2  56   240 7.6 4.0 150 320
termination-crafted/Singapore_plus_false-no-overflow.c 5.7 1.8 40 330 2.5 0      3.2  1.8  67   230 6.8 3.7 150 310
termination-crafted/Singapore_v1_false-no-overflow.c 5.6 1.8 44 320 2.5 0      3.3  1.9  63   230 7.6 4.0 150 320
termination-crafted/Singapore_v2_false-no-overflow.c 5.5 1.8 50 320 2.5 0      3.2  1.8  60   230 7.6 4.1 160 320
termination-crafted/Stockholm_false-no-overflow.c 5.7 1.8 44 320 2.5 0      3.3  1.9  48   230 8.2 4.3 140 320
termination-crafted/Thun_false-no-overflow.c 5.5 1.8 42 320 2.5 0      3.0  1.7  64   240 6.9 3.7 140 320
termination-crafted/Toulouse-BranchesToLoop_false-no-overflow.c 6.4 1.9 49 350 2.5 0      3.2  1.8  69   240 7.8 4.2 160 320
termination-crafted/Toulouse-MultiBranchesToLoop_false-no-overflow.c 15   4.3 110 560 2.5 0      3.9  2.2  67   240 9.0 4.8 150 340
termination-crafted/aaron2_false-no-overflow.c 5.7 1.8 46 320 2.5 0      3.1  1.8  67   230 7.4 4.0 140 320
termination-crafted/aaron3_false-no-overflow.c 5.5 1.8 44 330 2.5 0      3.0  1.7  62   230 7.3 3.9 150 310
termination-crafted/4BitCounterPointer_true-no-overflow.c 6.1 1.9 50 320 2.5 0      4.4  2.5  71   280 7.7 4.1 150 330
termination-crafted/Arrays01-EquivalentConstantIndices_true-no-overflow.c 900   730   13000 4800 2.3 0      .53 .34 12   39 5.8 3.1 98 300
termination-crafted/Arrays02-EquivalentConstantIndices_true-no-overflow.c 5.9 1.9 41 330 2.5 0      3.7  2.2  62   290 7.1 3.9 110 320
termination-crafted/Arrays03-ValueRestictsIndex_true-no-overflow.c 8.0 2.5 59 420 2.6 0      900    850    12000   5000 8.5 4.7 160 340
termination-crafted/Bangalore_true-no-overflow.c 8.2 2.5 59 400 2.5 0      3.9  2.2  58   280 8.4 4.6 150 350
termination-crafted/Bangalore_v2_true-no-overflow.c 7.6 2.4 63 380 2.5 0      4.9  2.8  38   280 8.7 4.7 140 350
termination-crafted/Bangalore_v4_true-no-overflow.c 6.3 2.0 48 330 2.5 0      3.7  2.1  49   280 8.1 4.4 160 330
termination-crafted/Benghazi_true-no-overflow.c 900   790   13000 1200 2.3 0      .59 .39 13   42 5.7 3.0 92 300
termination-crafted/Cairo_step2_true-no-overflow.c 900   740   12000 2400 2.3 0      .51 .33 12   40 6.2 3.3 120 310
termination-crafted/Cairo_true-no-overflow.c 6.4 2.0 50 330 2.5 0      4.0  2.2  67   280 8.4 4.6 170 330
termination-crafted/Copenhagen_true-no-overflow.c 6.8 2.1 57 340 2.5 0      4.0  2.2  40   280 9.0 4.8 150 330
termination-crafted/Division_true-no-overflow.c 6.3 2.0 45 330 2.5 0      3.9  2.2  48   270 7.5 4.1 160 320
termination-crafted/LexIndexValue-Array_true-no-overflow.c 900   730   14000 4600 2.3 0      .53 .33 12   40 6.3 3.3 130 290
termination-crafted/LexIndexValue-Pointer_true-no-overflow.c 900   720   13000 5200 2.3 0      .51 .34 10   39 5.8 3.1 120 290
termination-crafted/Madrid_true-no-overflow.c 5.9 1.7 45 340 2.5 0      3.7  2.1  62   270 6.7 3.6 130 300
termination-crafted/McCarthy91_Iteration_true-no-overflow.c 900   750   13000 3400 2.3 0      .47 .30 4.6 39 5.8 3.1 120 300
termination-crafted/McCarthy91_Recursion_true-no-overflow.c 7.1 2.2 54 350 2.5 0      3.1  1.8  31   240 9.1 5.0 170 330
termination-crafted/MenloPark_true-no-overflow.c 14   5.5 140 490 2.5 0      3.8  2.1  55   270 15   8.4 210 560
termination-crafted/MutualRecursion_1a_true-no-overflow.c 900   740   13000 1200 2.3 0      .51 .33 9.9 42 5.7 3.1 110 300
termination-crafted/MutualRecursion_1b_true-no-overflow.c 900   730   13000 1300 2.3 0      .57 .38 13   43 5.8 3.1 120 300
termination-crafted/NestedRecursion_1b_true-no-overflow.c 900   570   11000 1400 2.3 0      .55 .36 11   41 6.5 3.5 110 320
termination-crafted/NestedRecursion_1c_true-no-overflow.c 900   750   12000 1700 2.3 0      .49 .32 12   39 5.6 3.0 120 290
termination-crafted/NestedRecursion_1d_true-no-overflow.c 900   760   11000 1400 2.6 0      .49 .32 8.7 40 5.9 3.1 110 300
termination-crafted/NestedRecursion_2b_true-no-overflow.c 900   670   11000 1700 2.3 0      .54 .35 12   41 6.1 3.3 120 300
termination-crafted/NestedRecursion_2c_true-no-overflow.c 900   740   12000 3000 2.3 0      .53 .34 12   41 5.8 3.1 120 300
termination-crafted/NonTermination3_true-no-overflow.c 5.4 1.7 48 310 2.5 0      4.1  2.3  69   280 7.0 3.7 130 310
termination-crafted/NonTerminationSimple7_true-no-overflow.c 7.2 2.2 54 350 2.5 0      3.8  2.2  52   270 7.9 4.2 150 320
termination-crafted/Nyala-2lex_true-no-overflow.c 6.7 2.1 55 340 2.5 0      4.3  2.4  73   280 8.1 4.3 160 320
termination-crafted/Parallel_true-no-overflow.c 6.8 2.1 59 330 2.9 0      4.1  2.3  55   280 8.2 4.4 150 320
termination-crafted/Piecewise_true-no-overflow.c 6.5 2.1 53 320 2.5 0      4.6  2.6  56   270 7.6 4.2 140 310
termination-crafted/SyntaxSupportPointer01_true-no-overflow.c 6.7 2.1 48 320 2.5 0      3.1  1.8  49   260 8.8 4.7 160 330
termination-crafted/TelAviv-Amir-Minimum_true-no-overflow.c 8.0 2.3 62 360 2.5 0      4.5  2.5  46   270 7.5 4.1 150 310
termination-crafted/Waldkirch_true-no-overflow.c 5.8 2.0 49 320 2.5 0      3.8  2.1  40   270 7.8 4.2 140 320
termination-crafted/WhileFalse_true-no-overflow.c 5.2 1.7 44 310 2.5 0      3.5  2.0  76   270 7.0 3.8 140 310
termination-crafted/WhileTrue_true-no-overflow.c 5.4 1.7 42 320 2.5 0      3.6  2.1  79   270 7.2 3.8 130 310
termination-crafted/easy1_true-no-overflow.c 6.4 2.0 52 330 2.5 0      4.0  2.2  51   280 8.5 4.5 150 330
termination-crafted/easy2_true-no-overflow.c 900   760   13000 2200 2.3 0      .55 .37 11   42 6.1 3.2 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2a_false-no-overflow.c 6.0 1.9 48 320 2.5 0      3.3  1.9  73   240 7.5 4.0 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig2b_false-no-overflow.c 6.7 1.9 51 340 2.5 0      3.3  1.9  69   240 7.7 4.1 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron2_false-no-overflow.c 5.9 1.8 44 330 2.5 0      3.2  1.8  67   240 7.3 3.9 140 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-aaron3_false-no-overflow.c 5.2 1.7 42 320 2.5 0      3.1  1.8  67   240 7.7 4.1 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-complex_false-no-overflow.c 7.3 2.2 52 340 2.5 0      3.3  1.9  73   240 8.1 4.3 170 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1a_false-no-overflow.c 5.8 1.8 45 320 2.5 0      3.4  1.9  63   240 7.3 3.9 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-counterex1b_false-no-overflow.c 7.0 2.1 49 340 2.5 0      3.3  1.9  69   240 7.9 4.2 150 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-exmini_false-no-overflow.c 6.3 2.0 47 320 2.5 0      3.2  1.8  65   230 7.8 4.1 170 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-loops_true-termination_false-no-overflow.c 78   52   960 1000 2.5 0      4.6  2.5  82   260 87   50   730 7000
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-ndecr_false-no-overflow.c 6.5 1.9 56 340 2.5 0      3.1  1.8  70   230 7.5 4.0 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-rsd_false-no-overflow.c 5.4 1.8 45 320 2.5 0      3.2  1.8  67   240 7.3 3.9 150 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedFails4_false-no-overflow.c 5.7 1.9 46 320 2.5 0      3.2  1.8  66   240 7.1 3.8 140 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-terminate_false-no-overflow.c 6.2 1.9 46 320 2.5 0      3.3  1.9  62   240 7.6 4.1 150 320
termination-crafted-lit/Ben-Amram-LMCS2010-Ex2.3_false-no-overflow.c 7.3 1.9 57 370 2.5 0      3.4  1.9  67   240 7.7 4.1 140 320
termination-crafted-lit/BradleyMannaSipma-ICALP2005-Fig1_false-no-overflow.c 5.9 1.8 46 320 2.5 0      3.3  1.8  62   240 8.6 4.5 150 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron12_false-no-overflow.c 5.5 1.9 46 320 2.5 0      4.0  2.2  39   240 7.3 3.9 160 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron1_false-no-overflow.c 5.8 2.0 43 320 2.5 0      3.9  2.2  79   230 8.2 4.3 150 340
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_false-no-overflow.c 5.9 1.8 43 330 2.5 0      3.2  1.8  67   240 7.8 4.1 150 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_false-no-overflow.c 5.8 1.8 40 330 2.5 0      3.2  1.8  70   230 7.4 3.9 150 310
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron4_false-no-overflow.c 5.6 1.8 43 320 2.5 0      3.3  1.9  69   240 7.8 4.2 140 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron6_false-no-overflow.c 5.6 1.9 44 320 2.5 0      3.3  1.9  68   240 7.7 4.1 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.01_false-no-overflow.c 6.6 1.8 50 340 2.5 0      3.2  1.8  66   240 7.7 4.1 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.02_false-no-overflow.c 6.4 1.9 48 350 2.5 0      3.1  1.8  70   240 7.4 3.9 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.03_false-no-overflow.c 5.5 1.8 43 320 2.5 0      3.4  1.9  63   230 7.5 4.0 150 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.04_false-no-overflow.c 5.4 1.7 45 320 2.5 0      3.9  2.2  55   240 6.8 3.7 150 300
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex1.05_false-no-overflow.c 5.3 1.7 38 320 2.5 0      3.2  1.9  74   230 7.2 3.8 160 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.01_false-no-overflow.c 5.8 1.8 44 330 2.5 0      3.0  1.7  63   240 7.4 3.9 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.02_false-no-overflow.c 5.7 1.8 48 320 2.5 0      3.3  1.9  68   240 7.8 4.2 170 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.03_false-no-overflow.c 5.5 1.8 38 330 2.5 0      2.9  1.7  67   240 6.9 3.7 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.04_false-no-overflow.c 5.7 1.8 48 320 2.5 0      3.6  2.1  48   240 7.2 3.8 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.05_false-no-overflow.c 5.2 1.7 41 320 2.5 0      3.2  1.8  65   230 7.4 4.0 150 330
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.06_false-no-overflow.c 5.6 1.9 40 320 2.5 0      3.3  1.9  73   240 7.0 3.8 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.07_false-no-overflow.c 6.1 1.8 47 330 2.5 0      3.1  1.8  66   240 7.2 3.8 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.08_false-no-overflow.c 6.1 1.8 48 340 2.9 0      2.9  1.7  62   230 7.1 3.8 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.09_false-no-overflow.c 6.5 2.0 46 320 2.5 0      3.0  1.7  63   230 8.8 4.7 150 340
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.10_false-no-overflow.c 6.2 2.0 52 330 2.5 0      3.1  1.8  50   240 7.3 4.0 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.11_false-no-overflow.c 5.7 1.8 44 320 2.5 0      3.2  1.8  65   240 7.1 3.8 100 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.12_false-no-overflow.c 5.4 1.7 39 320 2.5 0      3.2  1.8  71   230 7.1 3.9 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.13_false-no-overflow.c 5.4 1.8 44 320 2.5 0      3.2  1.8  72   240 7.6 4.0 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.14_false-no-overflow.c 5.4 1.7 40 320 2.5 0      3.2  1.8  66   250 7.1 3.8 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.15_false-no-overflow.c 5.8 1.8 47 320 2.5 0      2.9  1.6  61   240 7.5 4.0 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.16_false-no-overflow.c 5.7 1.8 39 330 2.6 0      3.0  1.7  39   230 8.2 4.3 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.17_false-no-overflow.c 6.0 1.9 51 320 2.5 0      2.9  1.6  61   240 7.8 4.1 170 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.18_false-no-overflow.c 6.6 1.8 48 360 2.5 0      2.9  1.6  48   240 7.6 4.0 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.19_false-no-overflow.c 5.7 1.8 45 320 2.8 0      3.1  1.8  58   240 7.7 4.1 140 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.21_false-no-overflow.c 5.7 1.8 43 330 2.5 0      3.0  1.7  60   240 7.2 3.8 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.22_false-no-overflow.c 5.5 1.8 45 320 2.5 0      3.1  1.8  48   240 7.0 3.8 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.02_false-no-overflow.c 6.0 1.8 45 330 2.5 0      2.9  1.7  62   240 7.2 3.8 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.03_false-no-overflow.c 6.6 2.0 53 340 2.5 0      3.0  1.7  58   230 7.3 3.9 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.04_false-no-overflow.c 5.6 1.8 40 320 2.5 0      3.2  1.8  61   230 7.2 3.9 150 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.05_false-no-overflow.c 5.4 1.8 49 310 2.5 0      3.3  1.8  60   240 7.2 3.9 130 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.06_false-no-overflow.c 5.6 1.8 46 320 2.5 0      3.1  1.8  67   230 7.5 4.1 160 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.07_false-no-overflow.c 5.4 1.8 40 320 2.5 0      3.1  1.8  63   240 7.7 4.1 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.08_false-no-overflow.c 5.5 1.8 46 310 2.5 0      3.0  1.7  65   240 7.7 4.1 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.09_false-no-overflow.c 6.2 1.8 47 340 2.5 0      3.1  1.7  73   230 7.1 3.8 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.10_false-no-overflow.c 5.4 1.8 43 320 2.5 0      3.2  1.8  51   240 7.9 4.2 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex4.01_false-no-overflow.c 5.4 1.8 40 320 2.5 0      3.8  2.1  56   230 6.5 3.5 96 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Fig1_false-no-overflow.c 5.2 1.8 48 320 2.9 0      3.2  1.9  48   240 7.7 4.1 170 310
termination-crafted-lit/ColonSipma-TACAS2001-Fig1_false-no-overflow.c 5.9 1.9 48 320 2.5 0      3.3  1.9  63   240 8.1 4.3 170 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1a_false-no-overflow.c 6.3 1.8 47 340 2.5 0      3.1  1.8  59   240 6.8 3.7 130 310
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1b_false-no-overflow.c 5.6 1.8 50 320 2.5 0      3.2  1.8  61   240 7.3 3.9 160 320
termination-crafted-lit/GulavaniGulwani-CAV2008-Fig1c_false-no-overflow.c 5.6 1.8 44 330 2.5 0      3.5  2.0  49   240 7.0 3.8 100 310
termination-crafted-lit/GulwaniJainKoskinen-PLDI2009-Fig1_false-no-overflow.c 6.0 1.9 50 330 2.5 0      3.2  1.8  66   240 8.1 4.2 160 330
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig2_false-no-overflow.c 12   3.3 82 480 2.5 0      3.5  2.0  75   240 7.6 4.1 160 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig2_false-no-overflow.c 5.9 1.8 41 330 2.5 0      3.2  1.8  66   240 7.5 4.0 160 330
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig7_false-no-overflow.c 6.1 1.9 47 330 2.5 0      3.1  1.7  67   230 8.2 4.4 150 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig8_false-no-overflow.c 5.6 1.8 39 320 2.5 0      3.2  1.8  63   230 7.7 4.1 140 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig9_false-no-overflow.c 5.8 1.8 46 320 2.5 0      3.1  1.7  55   240 7.0 3.7 140 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex1_false-no-overflow.c 6.3 2.0 55 330 2.5 0      3.2  1.8  67   250 8.9 4.9 170 340
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex2_false-no-overflow.c 6.4 2.0 48 320 2.5 0      3.3  1.9  69   250 7.2 3.9 140 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex3_false-no-overflow.c 6.0 1.8 43 340 2.5 0      3.4  1.9  64   250 8.1 4.3 160 320
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex6_false-no-overflow.c 5.7 1.9 45 320 2.5 0      3.2  1.8  74   260 7.5 4.0 140 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex7_false-no-overflow.c 5.6 1.8 47 320 2.5 0      3.1  1.8  66   240 8.1 4.3 150 330
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex8_false-no-overflow.c 5.5 1.8 46 320 2.5 0      3.3  1.9  68   240 7.7 4.1 160 320
termination-crafted-lit/LeikeHeizmann-TACAS2014-Fig1_false-no-overflow.c 5.6 1.8 51 320 2.5 0      3.2  1.8  64   230 7.2 3.9 150 310
termination-crafted-lit/LeikeHeizmann-WST2014-Ex5_false-no-overflow.c 5.5 1.8 46 320 2.5 0      3.0  1.7  46   240 7.4 3.9 140 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex6_false-no-overflow.c 5.6 1.7 42 320 2.5 0      3.4  1.9  64   240 7.2 3.8 100 320
termination-crafted-lit/Masse-VMCAI2014-Ex6_false-no-overflow.c 5.8 1.7 45 330 2.5 0      3.2  1.8  62   250 7.7 4.1 150 310
termination-crafted-lit/Masse-VMCAI2014-Fig1a_false-no-overflow.c 6.9 1.9 57 340 2.5 0      3.6  2.0  48   230 7.1 3.8 130 320
termination-crafted-lit/Masse-VMCAI2014-Fig1b_false-no-overflow.c 5.3 1.7 42 320 2.5 0      3.1  1.8  64   230 8.1 4.2 150 320
termination-crafted-lit/NoriSharma-FSE2013-Fig7_false-no-overflow.c 5.6 1.8 41 320 2.5 0      3.1  1.7  61   240 7.1 3.8 140 320
termination-crafted-lit/NoriSharma-FSE2013-Fig8_false-no-overflow.c 6.3 2.0 49 330 2.5 0      3.1  1.8  63   230 7.3 3.9 140 320
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1_true-termination_false-no-overflow.c 33   13   300 910 2.6 0      4.6  2.6  78   250 83   48   680 7000
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_false-no-overflow.c 7.0 2.2 59 330 2.5 0      2.9  1.7  63   230 7.5 4.0 160 310
termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig2_false-no-overflow.c 6.5 2.0 54 340 2.5 0      3.3  1.9  60   240 7.9 4.2 150 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig3_false-no-overflow.c 7.8 2.2 69 340 2.5 0      3.0  1.7  63   230 7.4 3.9 140 320
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex1_false-no-overflow.c 5.6 1.7 51 320 2.5 0      3.3  1.9  67   240 7.2 3.8 130 320
termination-crafted-lit/PodelskiRybalchenko-VMCAI2004-Ex2_false-no-overflow.c 5.5 1.8 44 320 2.7 0      3.2  1.8  68   240 7.5 4.0 150 320
termination-crafted-lit/cstrncmp_false-no-overflow.c 7.3 2.3 53 330 2.5 0      4.2  2.3  81   260 8.0 4.4 64 350
termination-crafted-lit/gcd1_false-no-overflow.c 5.6 1.8 39 320 2.5 0      3.2  1.8  56   230 7.4 3.9 150 320
termination-crafted-lit/joey_false-no-overflow.c 6.2 1.9 46 330 2.9 0      3.4  1.9  69   250 7.8 4.2 150 320
termination-crafted-lit/min_rf_false-no-overflow.c 5.5 1.8 41 340 2.5 0      3.2  1.8  74   240 7.5 4.0 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-Fig1_true-termination_true-no-overflow.c 900   740   12000 4000 2.3 .0041 .51 .33 10   40 6.3 3.3 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-cousot9_true-termination_true-no-overflow.c 11   3.7 110 480 2.5 0      4.4  2.4  66   280 13   7.4 200 410
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination_true-no-overflow.c 6.3 2.0 54 330 2.5 0      4.1  2.3  56   280 8.3 4.5 160 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination_true-no-overflow.c 900   760   12000 2300 2.3 0      .50 .32 11   39 6.3 3.3 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-nestedLoop_true-termination_true-no-overflow.c 900   770   12000 2000 2.3 0      .51 .33 11   41 5.7 3.1 120 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random1d_true-termination_true-no-overflow.c 900   770   12000 1300 2.3 0      .50 .33 8.3 40 6.3 3.3 110 310
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-random2d_true-termination_true-no-overflow.c 900   760   12000 1600 2.3 0      .52 .35 11   40 6.2 3.2 130 300
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi2_true-termination_true-no-overflow.c 8.6 2.6 62 470 2.5 0      4.4  2.5  98   280 10   5.7 180 380
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi3_true-termination_true-no-overflow.c 14   4.5 110 500 2.5 0      4.3  2.4  69   270 9.4 5.1 160 340
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-speedpldi4_true-termination_true-no-overflow.c 8.3 2.7 63 460 2.5 0      4.1  2.3  49   280 9.2 5.0 170 340
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wcet2_true-termination_true-no-overflow.c 6.9 2.1 54 350 2.5 0      900    870    9700   4800 8.2 4.4 140 320
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-while2_true-termination_true-no-overflow.c 11   3.8 91 470 2.5 0      900    860    9700   4300 14   8.0 180 470
termination-crafted-lit/AliasDarteFeautrierGonnord-SAS2010-wise_true-termination_true-no-overflow.c 13   4.9 110 490 2.5 0      4.3  2.4  54   280 11   5.8 180 340
termination-crafted-lit/Avery-FLOPS2006-Table1_true-termination_true-no-overflow.c 900   740   11000 5400 2.3 0      .53 .35 13   41 6.0 3.2 120 300
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1-modified_false-termination_true-no-overflow.c 8.8 2.9 74 470 2.5 0      4.1  2.3  68   280 14   7.6 180 400
termination-crafted-lit/BradleyMannaSipma-CAV2005-Fig1_true-termination_true-no-overflow.c 15   5.5 130 610 2.5 0      4.0  2.2  59   270 14   7.8 180 370
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig1_true-termination_true-no-overflow.c 11   3.6 90 470 2.5 0      4.3  2.4  62   280 10   5.5 150 360
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Fig9a_true-termination_true-no-overflow.c 900   810   13000 980 2.3 0      .50 .32 11   39 5.8 3.1 120 300
termination-crafted-lit/BrockschmidtCookFuhs-CAV2013-Introduction_true-termination_true-no-overflow.c 63   36   650 1200 2.5 0      3.9  2.2  61   270 23   13   270 610
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination_true-no-overflow.c 6.5 2.0 49 330 2.5 0      4.0  2.2  61   280 8.7 4.7 140 330
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination_true-no-overflow.c 900   750   13000 2800 2.3 0      .49 .31 11   39 5.4 3.0 120 290
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random1d_true-termination_true-no-overflow.c 900   770   12000 1400 2.3 0      .61 .39 9.3 43 5.9 3.1 110 300
termination-crafted-lit/ChawdharyCookGulwaniSagivYang-ESOP2008-random2d_true-termination_true-no-overflow.c 900   760   12000 1700 2.3 0      .54 .35 12   40 6.1 3.3 130 300
termination-crafted-lit/ChenCookFuhsNimkarOHearn-TACAS2014-Introduction_false-termination_true-no-overflow.c 5.3 1.6 39 330 2.5 0      3.9  2.2  66   280 7.0 3.8 140 310
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex2.20_true-termination_true-no-overflow.c 5.9 1.9 53 320 2.5 0      3.7  2.1  62   270 7.8 4.2 150 320
termination-crafted-lit/ChenFlurMukhopadhyay-SAS2012-Ex3.01_true-termination_true-no-overflow.c 6.0 1.9 51 330 2.5 0      3.7  2.1  53   270 8.2 4.4 160 340
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig1_true-termination_true-no-overflow.c 6.9 2.2 58 350 2.5 0      4.4  2.5  69   280 9.0 4.8 150 340
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7a_true-termination_true-no-overflow.c 8.8 2.7 75 480 2.5 0      4.5  2.5  65   280 8.0 4.4 150 340
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig7b_true-termination_true-no-overflow.c 9.0 2.6 75 450 2.5 0      4.9  2.7  60   270 8.2 4.4 160 320
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a-modified_true-termination_true-no-overflow.c 8.8 2.6 59 440 2.5 0      3.9  2.2  81   300 8.9 4.9 150 350
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8a_true-termination_true-no-overflow.c 6.5 2.0 48 330 2.5 0      4.9  2.7  34   270 8.2 4.5 160 310
termination-crafted-lit/CookSeeZuleger-TACAS2013-Fig8b_true-termination_true-no-overflow.c 7.3 2.3 64 370 2.5 0      3.9  2.2  59   280 8.7 4.7 140 350
termination-crafted-lit/GopanReps-CAV2006-Fig1a_true-termination_true-no-overflow.c.c 900   750   12000 1900 2.3 0      .50 .33 13   40 5.9 3.1 130 290
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig1_true-termination_true-no-overflow.c 900   760   15000 3100 2.3 0      .56 .35 9.3 40 6.5 3.4 130 300
termination-crafted-lit/HarrisLalNoriRajamani-SAS2010-Fig3_true-termination_true-no-overflow.c 7.2 2.1 53 370 2.5 0      4.3  2.4  55   270 7.9 4.3 150 320
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig1_true-termination_true-no-overflow.c 73   44   990 1200 2.5 0      3.8  2.1  52   270 22   13   310 610
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig4_true-termination_true-no-overflow.c 6.1 1.9 46 330 2.5 0      3.8  2.1  49   300 7.8 4.2 130 330
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig5_true-termination_true-no-overflow.c 11   3.8 100 490 2.5 .0082 3.6  2.0  32   270 9.6 5.2 170 350
termination-crafted-lit/HeizmannHoenickeLeikePodelski-ATVA2013-Fig6_true-termination_true-no-overflow.c 6.4 2.0 54 330 2.5 0      3.8  2.1  41   280 8.6 4.6 140 340
termination-crafted-lit/HenzingerJhalaMajumdarSutre-POPL2002-LockingExample_false-termination_true-no-overflow.c 900   740   13000 5300 2.3 0      .50 .32 11   39 6.0 3.2 120 310
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Ex_true-termination_true-no-overflow.c 6.2 1.9 46 320 2.5 0      4.3  2.4  58   280 7.5 4.0 160 320
termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1_true-termination_true-no-overflow.c 6.7 2.1 54 350 2.5 0      3.8  2.2  63   280 8.0 4.3 140 310
termination-crafted-lit/LarrazOliverasRodriguez-CarbonellRubio-FMCAD2013-Fig1_true-termination_true-no-overflow.c 900   790   14000 1200 2.3 0      .50 .33 11   40 6.5 3.4 130 310
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex4_true-termination_true-no-overflow.c 8.8 2.7 67 470 2.5 0      3.3  1.8  46   240 12   6.3 170 390
termination-crafted-lit/LeeJonesBen-Amram-POPL2001-Ex5_true-termination_true-no-overflow.c 900   750   12000 2800 2.3 0      .53 .35 11   40 5.8 3.1 120 300
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex1_true-termination_true-no-overflow.c 9.9 3.2 74 470 2.5 0      4.1  2.3  39   290 9.0 4.9 140 350
termination-crafted-lit/LeikeHeizmann-TACAS2014-Ex9_true-termination_true-no-overflow.c 7.8 2.4 66 410 2.5 0      4.6  2.6  71   280 8.0 4.3 150 320
termination-crafted-lit/LeikeHeizmann-WST2014-Ex9_true-termination_true-no-overflow.c 6.1 2.0 46 320 2.5 0      3.9  2.2  89   270 7.8 4.2 150 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig1_true-termination_true-no-overflow.c 5.5 1.8 51 320 2.5 0      3.8  2.1  63   280 7.8 4.2 160 320
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig2_true-termination_true-no-overflow.c 8.7 2.4 63 420 2.5 0      4.1  2.3  54   270 8.8 4.8 160 340
termination-crafted-lit/PodelskiRybalchenko-TACAS2011-Fig4_true-termination_true-no-overflow.c 7.5 2.1 50 350 2.5 0      4.2  2.4  63   280 7.8 4.2 150 320
termination-crafted-lit/Urban-WST2013-Fig1_false-termination_true-no-overflow.c 5.8 1.9 47 340 2.5 0      4.0  2.2  64   270 7.9 4.2 140 320
termination-crafted-lit/Urban-WST2013-Fig2-modified1000_true-termination_true-no-overflow.c 7.5 2.3 61 370 2.5 0      450    430    4700   7000 9.2 5.0 150 370
termination-crafted-lit/Urban-WST2013-Fig2_true-termination_true-no-overflow.c 7.3 2.2 55 370 2.5 0      470    450    5200   7000 9.0 4.9 160 350
termination-crafted-lit/UrbanMine-ESOP2014-Fig3_true-termination_true-no-overflow.c 9.3 2.6 81 480 2.5 0      5.5  3.0  64   290 8.3 4.5 160 350
termination-crafted-lit/Velroyen_false-termination_true-no-overflow.c 6.2 1.8 47 340 2.5 0      4.4  2.4  54   280 8.0 4.2 150 320
termination-crafted-lit/aviad_true-termination_true-no-overflow.c 900   740   13000 4200 2.3 0      .53 .35 12   40 6.3 3.4 130 290
termination-crafted-lit/cstrcmp_true-termination_true-no-overflow.c 6.7 2.1 51 330 2.5 0      5.7  3.1  66   290 7.9 4.3 150 320
termination-crafted-lit/cstrcspn_true-termination_true-no-overflow.c 7.1 2.1 60 320 2.5 0      5.1  2.9  100   320 8.5 4.6 160 330
termination-crafted-lit/cstrlen_true-termination_true-no-overflow.c 6.6 2.0 52 340 2.5 0      4.1  2.3  59   280 8.0 4.3 140 320
termination-crafted-lit/cstrpbrk_true-termination_true-no-overflow.c 6.2 2.0 48 330 2.5 0      7.1  3.9  130   320 8.1 4.4 160 330
termination-crafted-lit/cstrspn_true-termination_true-no-overflow.c 6.6 2.0 53 340 2.5 0      4.9  2.7  64   310 8.1 4.4 160 330
termination-crafted-lit/genady_true-termination_true-no-overflow.c 34   16   360 720 2.5 0      4.3  2.4  62   290 11   6.3 170 390
termination-crafted-lit/strchr_true-no-overflow.c 6.2 2.0 51 320 2.5 0      4.7  2.7  42   280 8.2 4.4 160 330
termination-numeric/Addition01_false-no-overflow.c 5.8 1.9 44 320 2.5 0      3.4  1.9  73   250 7.8 4.1 160 310
termination-numeric/Avg_true_false-no-overflow.c 5.7 1.8 40 320 2.5 0      3.3  1.9  45   250 8.2 4.4 160 340
termination-numeric/Binomial_true-termination_false-no-overflow.c 900   500   11000 1100 2.3 0      .52 .35 11   40 5.9 3.1 120 290
termination-numeric/Et1_true_false-no-overflow.c 5.6 1.9 42 330 2.5 0      3.4  1.9  68   250 7.6 4.1 150 320
termination-numeric/Et2_true_false-no-overflow.c 5.8 1.9 50 320 2.5 0      3.3  1.9  67   250 7.4 3.9 140 320
termination-numeric/Et3_true_false-no-overflow.c 5.6 1.7 42 320 2.5 0      3.4  1.9  69   250 8.2 4.3 170 340
termination-numeric/Et4_true_false-no-overflow.c 5.6 1.8 48 320 2.5 0      3.4  1.9  74   250 7.6 4.1 140 320
termination-numeric/MultCommutative_false-no-overflow.c 11   3.3 86 470 2.5 0      2.8  1.6  43   170 23   12   270 630
termination-numeric/TerminatorRec02_true-termination_false-no-overflow.c 900   670   11000 930 2.9 0      .54 .36 9.9 40 6.1 3.2 120 300
termination-numeric/Ackermann01_true-termination_true-no-overflow.c 900   640   11000 1300 2.3 0      .53 .35 12   39 6.1 3.2 120 300
termination-numeric/EvenOdd01_true-termination_true-no-overflow.c 900   740   13000 4500 2.3 0      .53 .35 12   40 6.1 3.2 130 300
termination-numeric/Fibonacci01_true-termination_true-no-overflow.c 900   680   11000 1400 2.3 0      .51 .33 11   42 5.6 3.0 100 300
termination-numeric/LeUserDefRec_true-termination_true-no-overflow.c 7.3 2.3 62 400 2.5 0      3.3  1.9  45   240 8.1 4.4 140 320
termination-numeric/LogRecursive_true-termination_true-no-overflow.c 900   780   12000 2900 2.3 0      .50 .33 10   39 5.8 3.1 120 300
termination-numeric/Parts_true-termination_true-no-overflow.c 900   600   12000 1400 2.3 0      .49 .31 9.2 39 5.6 3.0 110 300
termination-numeric/TwoWay_true-termination_true-no-overflow.c 900   740   13000 810 2.3 0      .50 .33 8.3 39 6.0 3.1 96 290
termination-numeric/gcd01_true-termination_true-no-overflow.c 8.4 2.6 74 450 2.5 0      3.4  1.9  54   250 8.1 4.4 160 320
termination-numeric/java_LogBuiltIn_true-termination_true-no-overflow.c 82   53   1200 1600 2.5 0      4.5  2.5  75   280 510   500   6000 2200
termination-numeric/recHanoi02_true-termination_true-no-overflow.c 900   780   15000 1500 2.3 0      .51 .33 11   43 5.8 3.1 110 300
termination-numeric/rec_counter1_true-termination_true-no-overflow.c 900   750   14000 4200 2.3 0      .52 .34 11   39 5.6 3.0 120 300
termination-numeric/rec_counter3_true-termination_true-no-overflow.c 900   750   14000 3000 2.3 0      .57 .35 14   42 5.6 3.0 120 290
termination-numeric/twisted_true-termination_true-no-overflow.c 900   790   12000 1100 2.3 0      .54 .36 12   41 5.8 3.1 120 300
recursive/Addition02WithOverflowBug_false-no-overflow.c 6.5 1.9 50 340 2.5 0      3.1  1.8  66   250 7.5 4.0 150 310
recursive/Addition03_false-no-overflow.c 6.3 1.9 41 330 2.5 0      3.3  1.9  67   260 7.6 4.0 160 310
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c 5.5 1.8 46 320 2.5 0      3.5  2.0  71   250 7.9 4.2 160 320
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 900   640   10000 1300 2.3 0      .51 .33 12   40 5.7 3.1 110 290
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 900   640   10000 1300 2.3 0      .55 .35 11   42 5.6 3.0 120 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 900   640   12000 1400 2.3 0      .51 .35 12   40 6.2 3.3 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 900   640   11000 1500 2.3 0      .51 .34 11   39 6.6 3.5 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 900   740   15000 4300 2.3 0      .53 .36 12   40 6.0 3.2 130 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 900   740   16000 4900 2.3 0      .53 .34 12   40 6.0 3.2 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 900   750   13000 2000 2.3 0      .51 .34 9.3 41 5.5 2.9 90 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 5.7 1.8 44 320 2.5 0      3.3  1.8  41   250 7.1 3.8 130 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 900   740   15000 4600 2.3 0      .48 .30 8.6 39 7.0 3.7 130 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 900   740   13000 3900 2.3 0      .54 .34 9.7 41 5.7 3.0 110 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 900   680   11000 1300 2.3 0      .52 .33 12   40 6.2 3.3 140 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 900   680   12000 1100 2.3 0      .51 .34 12   40 6.0 3.2 130 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 900   680   13000 1400 2.3 0      .51 .34 12   39 5.9 3.1 120 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 900   680   12000 1300 2.3 0      .53 .35 11   39 6.0 3.2 120 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 900   680   12000 1300 2.3 0      .52 .34 10   40 6.4 3.4 110 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 7.8 2.4 60 380 2.5 0      3.3  1.8  52   250 9.8 5.3 160 350
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 7.7 2.3 58 390 2.5 0      3.3  1.9  71   240 10   5.5 160 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 900   730   13000 960 2.3 0      .54 .36 13   41 6.3 3.4 130 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 900   590   12000 1300 2.5 0      .52 .33 12   41 6.0 3.2 130 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 8.9 2.7 64 460 2.5 0      3.4  1.9  47   240 8.7 4.7 160 320
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 11   3.9 100 480 2.5 0      3.6  2.0  38   240 16   9.2 220 520
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 900   730   14000 1200 2.3 0      .54 .36 12   41 6.2 3.3 120 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 900   780   13000 1600 2.3 0      .52 .33 11   41 5.7 3.1 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 900   770   14000 1800 2.3 0      .56 .36 11   43 5.8 3.1 120 290
bitvector/jain_1_false-no-overflow.i 5.5 1.8 38 320 2.5 0      3.2  1.8  62   250 7.6 4.1 150 330
bitvector/jain_2_false-no-overflow.i 5.6 1.8 45 320 2.5 0      3.2  1.8  64   240 7.6 4.0 150 320
bitvector/jain_4_false-no-overflow.i 5.5 1.8 48 320 2.5 0      3.3  1.9  62   250 7.5 4.0 160 320
bitvector/jain_5_false-no-overflow.i 900   790   13000 1200 2.3 0      .56 .35 7.5 44 6.1 3.3 110 300
bitvector/jain_6_false-no-overflow.i 5.5 1.8 50 320 2.5 0      3.4  1.9  69   250 7.8 4.2 140 310
bitvector/jain_7_false-no-overflow.i 5.7 1.8 43 320 2.5 0      3.0  1.7  61   250 7.1 3.8 160 310
bitvector/modulus_false-no-overflow.i 5.8 1.9 46 320 2.5 0      .55 .37 13   40 6.6 3.5 140 310
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i 7.4 2.2 56 350 2.6 0      10    5.5  96   450 7.5 4.1 140 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i 7.8 2.3 59 360 2.6 0      11    5.8  150   460 8.2 4.5 160 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i 8.2 2.4 63 360 2.6 0      19    9.8  260   640 8.3 4.5 110 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i 6.4 2.1 49 320 2.5 0      5.0  2.9  41   330 9.4 5.0 150 340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i 6.3 2.0 50 320 2.5 0      5.0  2.9  71   330 8.1 4.4 160 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i 6.5 2.0 50 330 2.5 0      5.2  2.9  97   300 8.3 4.4 160 320
bitvector/gcd_4_true-unreach-call_true-no-overflow.i 20   7.3 170 530 2.5 0      5.1  2.8  59   280 14   7.7 240 430
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i 5.4 1.7 43 320 2.5 0      4.9  2.7  100   290 7.4 3.9 140 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i 5.2 1.7 40 310 2.5 0      3.9  2.2  53   280 7.1 3.8 130 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i 5.1 1.7 40 320 2.5 0      4.1  2.3  53   280 6.7 3.6 130 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i 5.3 1.7 47 330 2.5 0      4.4  2.5  75   280 6.9 3.7 140 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i 5.3 1.7 40 320 2.5 0      4.1  2.3  94   280 6.8 3.6 140 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i 6.0 1.8 42 340 2.5 0      4.3  2.4  44   280 6.9 3.7 120 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i 6.0 1.8 51 330 2.5 0      4.3  2.4  63   280 6.5 3.5 130 310
bitvector/modulus_true-unreach-call_true-no-overflow.i 6.0 2.0 46 320 2.5 0      .52 .34 12   41 5.8 3.1 130 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i 5.7 1.8 47 320 2.5 0      5.0  2.8  100   280 7.3 3.9 150 330
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i 5.7 1.9 46 320 2.5 0      4.4  2.5  41   280 7.4 4.0 140 330
bitvector/parity_true-unreach-call_true-no-overflow.i 5.3 1.7 46 320 2.5 0      4.9  2.7  73   270 6.5 3.5 130 300
bitvector/sum02_false-unreach-call_true-no-overflow.i 6.0 2.0 48 320 2.5 0      4.5  2.5  56   280 6.6 3.6 140 310
bitvector/sum02_true-unreach-call_true-no-overflow.i 16   12   200 330 2.5 0      4.5  2.5  91   290 7.5 4.0 120 320
../../sv-benchmarks/c/ verifier status cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 328 59000 47000 810000 240000 820 .012  328 530 300 10000 39000   328 1400 760 26000 66000   328 4100 3700 48000 58000   328 1800 1200 29000 55000  
    correct results 263 2300 980 22000 97000 670 .0082 151 530 300 10000 38000   158 1400 740 25000 65000   89 4100 3700 47000 56000   102 1400 990 22000 37000  
        correct true 103 990 390 9200 41000 260 .0082 38 0 0 0 0   0 0 0 0 0   80 4100 3700 47000 56000   102 1400 990 22000 37000  
        correct false 160 1300 590 13000 55000 410 0      113 530 300 10000 38000   158 1400 740 25000 65000   9 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (328 tasks, max score: 491) 366
Run set [sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other]