/bat0/stac/Code/icra/WALi-OpenNWA/../icra -cra_newton_basic -cra-split-loops

Passing command-line option -cra-split-loops to duet.
<Unique State Name, 64> -> <Unique State Name, 40>	Base relation: 
{__cost := (__cost:106 + 1)
 a := param0:157
 lo := param1:160
 hi := param2:213
 a@pos := param0@pos:156
 a@width := param0@width:155
 when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1))}	
<Unique State Name, 81> -> <Unique State Name, 12>	Base relation: 
{}	
<Unique State Name, 80> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 8> -> <Unique State Name, 81>	Base relation: 
{when (i:6 <= 20 /\ 0 <= i:6 /\ len:0 <= 20 /\ 20 <= len:0)}	
<Unique State Name, 12> -> <Unique State Name, 8>	Base relation: 
{i := (i:6 + 1)
 when i:6 < len:0}	
<Unique State Name, 12> -> <Unique State Name, 77>	Base relation: 
{param0 := a:9
 param1 := len:0
 param0@pos := a@pos:8
 param1@pos := type_err:33
 param0@width := a@width:7
 param1@width := type_err:34
 when len:0 <= i:6}	
<Unique State Name, 71> -> <Unique State Name, 64 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 70> -> <Unique State Name, 29>	Base relation: 
{}	
<Unique State Name, 58> -> <Unique State Name, 64 57>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 79> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, 58>	Base relation: 
{param0 := a:193
 param1 := lo:181
 param2 := m2:198
 param0@pos := a@pos:192
 param1@pos := type_err:215
 param2@pos := type_err:217
 param0@width := a@width:191
 param1@width := type_err:216
 param2@width := type_err:218}	
<Unique State Name, 52> -> <Unique State Name, 78>	Base relation: 
{return := havoc:186
 return@pos := type_err:189
 return@width := type_err:190}	
<Unique State Name, 72> -> <Unique State Name, 71>	Base relation: 
{param0 := param0:157
 param1 := 0
 param2 := param1:160
 param0@pos := param0@pos:156
 param1@pos := type_err:165
 param2@pos := type_err:166
 param0@width := param0@width:155
 param1@width := type_err:167
 param2@width := type_err:168}	
<Unique State Name, 27> -> <Unique State Name, 8>	Base relation: 
{__cost := 0
 len := 20
 a := alloc:27
 i := 0
 a@pos := 0
 a@width := 80}	
<Unique State Name, 77> -> <Unique State Name, 72 76>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 57> -> <Unique State Name, 52>	Base relation: 
{}	
<Unique State Name, 29> -> <Unique State Name, 79>	Base relation: 
{return := havoc:138
 return@pos := type_err:141
 return@width := type_err:142}	
<Unique State Name, 76> -> <Unique State Name, 80>	Base relation: 
{return := 0
 return@pos := type_err:31
 return@width := type_err:32}	
<Unique State Name, 40> -> <Unique State Name, 52>	Base relation: 
{when (hi:182 + -lo:181) < 1}	
<Unique State Name, 40> -> <Unique State Name, 63>	Base relation: 
{m2 := ((havoc:214 + lo:181) + -1)
 param0 := a:193
 param1 := (havoc:214 + lo:181)
 param2 := hi:182
 param0@pos := a@pos:192
 param1@pos := type_err:219
 param2@pos := type_err:221
 param0@width := a@width:191
 param1@width := type_err:220
 param2@width := type_err:222
 when (1 <= (hi:182 + -lo:181) /\ 0 < havoc:214
         /\ (lo:181 + havoc:214) <= hi:182)}	
<Unique State Name, 63> -> <Unique State Name, 64 62>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 78> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{i := (i:6 + 1)
 when (i:6 <= 20 /\ 0 <= i:6 /\ len:0 <= 20 /\ 20 <= len:0 /\ i:6 < len:0)}
**** alpha hat: 
  {<Split [true
            (i':281) = (1)*(i:6) + 1
           }
          pre:
            [|len:0-20=0; -i:6+19>=0; i:6>=0|]
          post:
            [|len:0-20=0; -i':281+20>=0; i':281-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {i := i':281
   when ((!(0 <= K:287) \/ mid_i:289 = (i:6 + K:287))
           /\ ((K:287 = 0 /\ i:6 = mid_i:289)
                 \/ (1 <= K:287 /\ (-20 + len:0) = 0 /\ 0 <= (19 + -i:6)
                       /\ 0 <= i:6 /\ (-20 + len:0) = 0
                       /\ 0 <= (20 + -mid_i:289) /\ 0 <= (-1 + mid_i:289)))
           /\ K:288 = 0 /\ mid_i:289 = i':281 /\ 0 = K:288
           /\ (K:287 + K:288) = K:286 /\ 0 <= K:286)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
9  16  23  


New-style (IRE) regular expression in IREregExpMap for reID=9: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       len := 20
       a := alloc:27
       i := i':293
       param0 := alloc:27
       param1 := 20
       a@pos := 0
       param0@pos := 0
       param1@pos := type_err:295
       a@width := 80
       param0@width := 80
       param1@width := type_err:296
       when ((!(0 <= K:290) \/ mid_i:291 = K:290)
               /\ ((K:290 = 0 /\ 0 = mid_i:291)
                     \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                           /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
               /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
               /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
               /\ 0 <= i':293 /\ 20 <= i':293)}    )
    ,
    Var(16)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:31
     return@width := type_err:32}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=16: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:157
       param1 := 0
       param2 := param1:160
       param0@pos := param0@pos:156
       param1@pos := type_err:165
       param2@pos := type_err:166
       param0@width := param0@width:155
       param1@width := type_err:167
       param2@width := type_err:168}    )
    ,
    Var(23)
  )
  ,
  Weight(Base relation: 
    {return := havoc:138
     return@pos := type_err:141
     return@width := type_err:142}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=23: 
Dot(
  Plus(
    Weight(Base relation: 
      {__cost := (__cost:106 + 1)
       a := param0:157
       lo := param1:160
       hi := param2:213
       a@pos := param0@pos:156
       a@width := param0@width:155
       when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
               /\ (param2:213 + -param1:160) < 1)}    )
    ,
    Dot(
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := (__cost:106 + 1)
             m2 := ((havoc:297 + param1:160) + -1)
             a := param0:157
             lo := param1:160
             hi := param2:213
             param0 := param0:157
             param1 := (havoc:297 + param1:160)
             param2 := param2:213
             a@pos := param0@pos:156
             param0@pos := param0@pos:156
             param1@pos := type_err:298
             param2@pos := type_err:299
             a@width := param0@width:155
             param0@width := param0@width:155
             param1@width := type_err:300
             param2@width := type_err:301
             when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                     /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
                     /\ (param1:160 + havoc:297) <= param2:213)}          )
          ,
          Var(23)
        )
        ,
        Weight(Base relation: 
          {param0 := a:193
           param1 := lo:181
           param2 := m2:198
           param0@pos := a@pos:192
           param1@pos := type_err:215
           param2@pos := type_err:217
           param0@width := a@width:191
           param1@width := type_err:216
           param2@width := type_err:218}        )
      )
      ,
      Var(23)
    )
  )
  ,
  Weight(Base relation: 
    {return := havoc:186
     return@pos := type_err:189
     return@width := type_err:190}  )
)



Performing Gaussian Elimination.


  ------------------------------ 
Working on variable 9
  New-style (IRE) regular expression for 9 just before isolating it: 

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         len := 20
         a := alloc:27
         i := i':293
         param0 := alloc:27
         param1 := 20
         a@pos := 0
         param0@pos := 0
         param1@pos := type_err:295
         a@width := 80
         param0@width := 80
         param1@width := type_err:296
         when ((!(0 <= K:290) \/ mid_i:291 = K:290)
                 /\ ((K:290 = 0 /\ 0 = mid_i:291)
                       \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                             /\ 0 <= (20 + -mid_i:291)
                             /\ 0 <= (-1 + mid_i:291))) /\ K:292 = 0
                 /\ mid_i:291 = i':293 /\ 0 = K:292
                 /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
                 /\ 0 <= i':293 /\ 20 <= i':293)}      )
      ,
      Var(16)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:31
       return@width := type_err:32}    )
  )
)



  ------------------------------ 
Working on variable 16
  New-style (IRE) regular expression for 16 just before isolating it: 

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:157
         param1 := 0
         param2 := param1:160
         param0@pos := param0@pos:156
         param1@pos := type_err:165
         param2@pos := type_err:166
         param0@width := param0@width:155
         param1@width := type_err:167
         param2@width := type_err:168}      )
      ,
      Var(23)
    )
    ,
    Weight(Base relation: 
      {return := havoc:138
       return@pos := type_err:141
       return@width := type_err:142}    )
  )
)



  ------------------------------ 
Working on variable 23
  New-style (IRE) regular expression for 23 just before isolating it: 

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:106 + 1)
         a := param0:157
         lo := param1:160
         hi := param2:213
         a@pos := param0@pos:156
         a@width := param0@width:155
         when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                 /\ (param2:213 + -param1:160) < 1)}      )
      ,
      Dot(
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := (__cost:106 + 1)
               m2 := ((havoc:297 + param1:160) + -1)
               a := param0:157
               lo := param1:160
               hi := param2:213
               param0 := param0:157
               param1 := (havoc:297 + param1:160)
               param2 := param2:213
               a@pos := param0@pos:156
               param0@pos := param0@pos:156
               param1@pos := type_err:298
               param2@pos := type_err:299
               a@width := param0@width:155
               param0@width := param0@width:155
               param1@width := type_err:300
               param2@width := type_err:301
               when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                       /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
                       /\ (param1:160 + havoc:297) <= param2:213)}            )
            ,
            Var(23)
          )
          ,
          Weight(Base relation: 
            {param0 := a:193
             param1 := lo:181
             param2 := m2:198
             param0@pos := a@pos:192
             param1@pos := type_err:215
             param2@pos := type_err:217
             param0@width := a@width:191
             param1@width := type_err:216
             param2@width := type_err:218}          )
        )
        ,
        Var(23)
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:186
       return@pos := type_err:189
       return@width := type_err:190}    )
  )
)



 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=9: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         len := 20
         a := alloc:27
         i := i':293
         param0 := alloc:27
         param1 := 20
         a@pos := 0
         param0@pos := 0
         param1@pos := type_err:295
         a@width := 80
         param0@width := 80
         param1@width := type_err:296
         when ((!(0 <= K:290) \/ mid_i:291 = K:290)
                 /\ ((K:290 = 0 /\ 0 = mid_i:291)
                       \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                             /\ 0 <= (20 + -mid_i:291)
                             /\ 0 <= (-1 + mid_i:291))) /\ K:292 = 0
                 /\ mid_i:291 = i':293 /\ 0 = K:292
                 /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
                 /\ 0 <= i':293 /\ 20 <= i':293)}      )
      ,
      Project(
        Dot(
          Dot(
            Weight(Base relation: 
              {param0 := param0:157
               param1 := 0
               param2 := param1:160
               param0@pos := param0@pos:156
               param1@pos := type_err:165
               param2@pos := type_err:166
               param0@width := param0@width:155
               param1@width := type_err:167
               param2@width := type_err:168}            )
            ,
            Detensor(
              Weight(Base relation: 
                {__cost := (__cost:106 + 1)
                 return := havoc:302
                 return@pos := type_err:303
                 return@width := type_err:304
                 when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                         /\ (param2:213 + -param1:160) < 1)}              )
              ,
              KleeneT( key=1
                ProjectT(
                  Tensor(
                    Dot(
                      Dot(
                        Weight(Base relation: 
                          {__cost := (__cost:106 + 1)
                           m2 := ((havoc:297 + param1:160) + -1)
                           a := param0:157
                           lo := param1:160
                           hi := param2:213
                           param0 := param0:157
                           param1 := (havoc:297 + param1:160)
                           param2 := param2:213
                           a@pos := param0@pos:156
                           param0@pos := param0@pos:156
                           param1@pos := type_err:298
                           param2@pos := type_err:299
                           a@width := param0@width:155
                           param0@width := param0@width:155
                           param1@width := type_err:300
                           param2@width := type_err:301
                           when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                                   /\ 1 <= (param2:213 + -param1:160)
                                   /\ 0 < havoc:297
                                   /\ (param1:160 + havoc:297) <= param2:213)}                        )
                        ,
                        Var(23)
                      )
                      ,
                      Weight(Base relation: 
                        {param0 := a:193
                         param1 := lo:181
                         param2 := m2:198
                         param0@pos := a@pos:192
                         param1@pos := type_err:215
                         param2@pos := type_err:217
                         param0@width := a@width:191
                         param1@width := type_err:216
                         param2@width := type_err:218}                      )
                    )
                    ,
                    Weight(Base relation: 
                      {return := havoc:186
                       return@pos := type_err:189
                       return@width := type_err:190}                    )
                  )
                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:138
             return@pos := type_err:141
             return@width := type_err:142}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:31
       return@width := type_err:32}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=16: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:157
         param1 := 0
         param2 := param1:160
         param0@pos := param0@pos:156
         param1@pos := type_err:165
         param2@pos := type_err:166
         param0@width := param0@width:155
         param1@width := type_err:167
         param2@width := type_err:168}      )
      ,
      Detensor(
        Weight(Base relation: 
          {__cost := (__cost:106 + 1)
           return := havoc:302
           return@pos := type_err:303
           return@width := type_err:304
           when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                   /\ (param2:213 + -param1:160) < 1)}        )
        ,
        KleeneT( key=1
          ProjectT(
            Tensor(
              Dot(
                Dot(
                  Weight(Base relation: 
                    {__cost := (__cost:106 + 1)
                     m2 := ((havoc:297 + param1:160) + -1)
                     a := param0:157
                     lo := param1:160
                     hi := param2:213
                     param0 := param0:157
                     param1 := (havoc:297 + param1:160)
                     param2 := param2:213
                     a@pos := param0@pos:156
                     param0@pos := param0@pos:156
                     param1@pos := type_err:298
                     param2@pos := type_err:299
                     a@width := param0@width:155
                     param0@width := param0@width:155
                     param1@width := type_err:300
                     param2@width := type_err:301
                     when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                             /\ 1 <= (param2:213 + -param1:160)
                             /\ 0 < havoc:297
                             /\ (param1:160 + havoc:297) <= param2:213)}                  )
                  ,
                  Var(23)
                )
                ,
                Weight(Base relation: 
                  {param0 := a:193
                   param1 := lo:181
                   param2 := m2:198
                   param0@pos := a@pos:192
                   param1@pos := type_err:215
                   param2@pos := type_err:217
                   param0@width := a@width:191
                   param1@width := type_err:216
                   param2@width := type_err:218}                )
              )
              ,
              Weight(Base relation: 
                {return := havoc:186
                 return@pos := type_err:189
                 return@width := type_err:190}              )
            )
          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:138
       return@pos := type_err:141
       return@width := type_err:142}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=23: 
Detensor(
  Weight(Base relation: 
    {__cost := (__cost:106 + 1)
     return := havoc:302
     return@pos := type_err:303
     return@width := type_err:304
     when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
             /\ (param2:213 + -param1:160) < 1)}  )
  ,
  KleeneT( key=1
    ProjectT(
      Tensor(
        Dot(
          Dot(
            Weight(Base relation: 
              {__cost := (__cost:106 + 1)
               m2 := ((havoc:297 + param1:160) + -1)
               a := param0:157
               lo := param1:160
               hi := param2:213
               param0 := param0:157
               param1 := (havoc:297 + param1:160)
               param2 := param2:213
               a@pos := param0@pos:156
               param0@pos := param0@pos:156
               param1@pos := type_err:298
               param2@pos := type_err:299
               a@width := param0@width:155
               param0@width := param0@width:155
               param1@width := type_err:300
               param2@width := type_err:301
               when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
                       /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
                       /\ (param1:160 + havoc:297) <= param2:213)}            )
            ,
            Var(23)
          )
          ,
          Weight(Base relation: 
            {param0 := a:193
             param1 := lo:181
             param2 := m2:198
             param0@pos := a@pos:192
             param1@pos := type_err:215
             param2@pos := type_err:217
             param0@width := a@width:191
             param1@width := type_err:216
             param2@width := type_err:218}          )
        )
        ,
        Weight(Base relation: 
          {return := havoc:186
           return@pos := type_err:189
           return@width := type_err:190}        )
      )
    )
  )
)


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 9 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when false}
**** alpha hat: 
  {<Split [true
            }
          pre:
            bottom
          post:
            bottom
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when (K:318 = 0
           /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):320
           /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):321
           /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):322
           /\ K:319 = 0
           /\ mid_(NewtonDomain.Right return@width):320 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):321 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):322 = (NewtonDomain.Right return)':306
           /\ 0 = K:319 /\ (K:318 + K:319) = K:317 /\ 0 <= K:317)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{when false}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (__cost:106 + 1)
 return := havoc:347
 param0 := param0:157
 param1 := 0
 param2 := param1:160
 return@pos := type_err:348
 param0@pos := param0@pos:156
 param1@pos := type_err:165
 param2@pos := type_err:166
 return@width := type_err:349
 param0@width := param0@width:155
 param1@width := type_err:167
 param2@width := type_err:168
 when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1) /\ param1:160 < 1
         /\ K:335 = 0
         /\ type_err:336 = mid_(NewtonDomain.Right return@width):337
         /\ type_err:338 = mid_(NewtonDomain.Right return@pos):339
         /\ havoc:340 = mid_(NewtonDomain.Right return):341 /\ K:342 = 0
         /\ mid_(NewtonDomain.Right return@width):337 = (NewtonDomain.Right return@width)':343
         /\ mid_(NewtonDomain.Right return@pos):339 = (NewtonDomain.Right return@pos)':344
         /\ mid_(NewtonDomain.Right return):341 = (NewtonDomain.Right return)':345
         /\ 0 = K:342 /\ (K:335 + K:342) = K:346 /\ 0 <= K:346)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (__cost:106 + 1)
 return := (NewtonDomain.Right return)':333
 return@pos := (NewtonDomain.Right return@pos)':332
 return@width := (NewtonDomain.Right return@width)':331
 when (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
         /\ (param2:213 + -param1:160) < 1 /\ K:326 = 0
         /\ type_err:304 = mid_(NewtonDomain.Right return@width):327
         /\ type_err:303 = mid_(NewtonDomain.Right return@pos):328
         /\ havoc:302 = mid_(NewtonDomain.Right return):329 /\ K:330 = 0
         /\ mid_(NewtonDomain.Right return@width):327 = (NewtonDomain.Right return@width)':331
         /\ mid_(NewtonDomain.Right return@pos):328 = (NewtonDomain.Right return@pos)':332
         /\ mid_(NewtonDomain.Right return):329 = (NewtonDomain.Right return)':333
         /\ 0 = K:330 /\ (K:326 + K:330) = K:334 /\ 0 <= K:334)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> First round; nothing to compare against; continuing loop.
-------------------------------------------------------------------------------
Round 1:
Evaluating variable number 9 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:385
 (NewtonDomain.Left return) := fresh_return:390
 (NewtonDomain.Left param0) := fresh_param0:391
 (NewtonDomain.Left param1) := fresh_param1:392
 (NewtonDomain.Left param2) := fresh_param2:393
 (NewtonDomain.Left return@pos) := fresh_return@pos:395
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:396
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:397
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:398
 (NewtonDomain.Left return@width) := fresh_return@width:400
 (NewtonDomain.Left param0@width) := fresh_param0@width:401
 (NewtonDomain.Left param1@width) := fresh_param1@width:402
 (NewtonDomain.Left param2@width) := fresh_param2@width:403
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:385 /\ 0 <= (fresh___cost:385 + 1)
         /\ 1 <= (fresh_param2:393 + -fresh_param1:392) /\ 0 < havoc:297
         /\ (fresh_param1:392 + havoc:297) <= fresh_param2:393
         /\ 0 <= (fresh___cost:385 + 1) /\ 0 <= ((fresh___cost:385 + 1) + 1)
         /\ (fresh_param2:393 + -((havoc:297 + fresh_param1:392))) < 1
         /\ K:369 = 0
         /\ type_err:370 = mid_(NewtonDomain.Right return@width):371
         /\ type_err:372 = mid_(NewtonDomain.Right return@pos):373
         /\ havoc:374 = mid_(NewtonDomain.Right return):375 /\ K:376 = 0
         /\ mid_(NewtonDomain.Right return@width):371 = (NewtonDomain.Right return@width)':377
         /\ mid_(NewtonDomain.Right return@pos):373 = (NewtonDomain.Right return@pos)':378
         /\ mid_(NewtonDomain.Right return):375 = (NewtonDomain.Right return)':379
         /\ 0 = K:376 /\ (K:369 + K:376) = K:380 /\ 0 <= K:380
         /\ (NewtonDomain.Left __cost):407 = ((fresh___cost:385 + 1) + 1)
         /\ (NewtonDomain.Right m2):432 = ((havoc:297 + fresh_param1:392)
                                             + -1)
         /\ (NewtonDomain.Right a):433 = fresh_param0:391
         /\ (NewtonDomain.Right lo):434 = fresh_param1:392
         /\ (NewtonDomain.Right hi):435 = fresh_param2:393
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':379
         /\ (NewtonDomain.Left param0):413 = fresh_param0:391
         /\ (NewtonDomain.Left param1):414 = fresh_param1:392
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:392)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):436 = fresh_param0@pos:396
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':378
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:396
         /\ (NewtonDomain.Left param1@pos):419 = type_err:381
         /\ (NewtonDomain.Left param2@pos):420 = type_err:382
         /\ (NewtonDomain.Right a@width):437 = fresh_param0@width:401
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':377
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:401
         /\ (NewtonDomain.Left param1@width):424 = type_err:383
         /\ (NewtonDomain.Left param2@width):425 = type_err:384)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                 + 0
           ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param2)':442) = (1)*((NewtonDomain.Left param2):415)
                                                + 1
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           ((NewtonDomain.Left __cost)':438) = (1)*((NewtonDomain.Left __cost):407)
                                                + (-2)*1
           }
          pre:
            [|(NewtonDomain.Left __cost):407-2>=0;
              (NewtonDomain.Left param2):415-(NewtonDomain.Left param1):414>=0|]
          post:
            [|(NewtonDomain.Left __cost)':438>=0;
              (NewtonDomain.Left param2)':442-(NewtonDomain.Left param1)':441
              -1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:490)
            \/ mid_(NewtonDomain.Left param0):505 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:490)
                 \/ mid_(NewtonDomain.Left param1):504 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:490)
                 \/ mid_(NewtonDomain.Left param0@pos):501 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:490)
                 \/ mid_(NewtonDomain.Left param2):503 = ((NewtonDomain.Left param2):415
                                                            + K:490))
           /\ (!(0 <= K:490)
                 \/ mid_(NewtonDomain.Left param0@width):497 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:490)
                 \/ mid_(NewtonDomain.Left __cost):507 = ((NewtonDomain.Left __cost):407
                                                            + (-2 * K:490)))
           /\ ((K:490 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):492
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):493
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):494
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):495
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):496
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):497
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):498
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):499
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):500
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):501
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):502
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):503
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):504
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):505
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):506
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):507)
                 \/ (1 <= K:490 /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= ((NewtonDomain.Left param2):415
                                  + -(NewtonDomain.Left param1):414)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):507
                       /\ 0 <= (-1 + mid_(NewtonDomain.Left param2):503
                                  + -mid_(NewtonDomain.Left param1):504)))
           /\ K:491 = 0
           /\ mid_(NewtonDomain.Right return@width):492 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):493 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):494 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):495 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):496 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):497 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):498 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):499 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):500 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):501 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):502 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):503 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):504 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):505 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):506 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):507 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:491 /\ (K:490 + K:491) = K:489 /\ 0 <= K:489)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:610 + 1)
 return := 0
 param0 := fresh_param0:615
 param1 := fresh_param1:612
 param2 := fresh_param2:611
 return@pos := type_err:668
 param0@pos := fresh_param0@pos:618
 param1@pos := fresh_param1@pos:637
 param2@pos := fresh_param2@pos:635
 return@width := type_err:669
 param0@width := fresh_param0@width:621
 param1@width := fresh_param1@width:631
 param2@width := fresh_param2@width:629
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:610
         /\ 0 <= (fresh___cost:610 + 1)
         /\ (fresh_param2:611 + -fresh_param1:612) < 1
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left param0):614 = fresh_param0:615)
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left param1):616 = fresh_param1:612)
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left param0@pos):617 = fresh_param0@pos:618)
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left param2):619 = (fresh_param2:611
                                                          + K:613))
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left param0@width):620 = fresh_param0@width:621)
         /\ (!(0 <= K:613)
               \/ mid_(NewtonDomain.Left __cost):622 = (fresh___cost:610
                                                          + (-2 * K:613)))
         /\ ((K:613 = 0
                /\ type_err:623 = mid_(NewtonDomain.Right return@width):624
                /\ type_err:625 = mid_(NewtonDomain.Right return@pos):626
                /\ havoc:627 = mid_(NewtonDomain.Right return):628
                /\ fresh_param2@width:629 = mid_(NewtonDomain.Left param2@width):630
                /\ fresh_param1@width:631 = mid_(NewtonDomain.Left param1@width):632
                /\ fresh_param0@width:621 = mid_(NewtonDomain.Left param0@width):620
                /\ fresh_return@width:633 = mid_(NewtonDomain.Left return@width):634
                /\ fresh_param2@pos:635 = mid_(NewtonDomain.Left param2@pos):636
                /\ fresh_param1@pos:637 = mid_(NewtonDomain.Left param1@pos):638
                /\ fresh_param0@pos:618 = mid_(NewtonDomain.Left param0@pos):617
                /\ fresh_return@pos:639 = mid_(NewtonDomain.Left return@pos):640
                /\ fresh_param2:611 = mid_(NewtonDomain.Left param2):619
                /\ fresh_param1:612 = mid_(NewtonDomain.Left param1):616
                /\ fresh_param0:615 = mid_(NewtonDomain.Left param0):614
                /\ fresh_return:641 = mid_(NewtonDomain.Left return):642
                /\ fresh___cost:610 = mid_(NewtonDomain.Left __cost):622)
               \/ (1 <= K:613 /\ 0 <= (-2 + fresh___cost:610)
                     /\ 0 <= (fresh_param2:611 + -fresh_param1:612)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):622
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param2):619
                                + -mid_(NewtonDomain.Left param1):616)))
         /\ K:643 = 0
         /\ mid_(NewtonDomain.Right return@width):624 = (NewtonDomain.Right return@width)':644
         /\ mid_(NewtonDomain.Right return@pos):626 = (NewtonDomain.Right return@pos)':645
         /\ mid_(NewtonDomain.Right return):628 = (NewtonDomain.Right return)':646
         /\ mid_(NewtonDomain.Left param2@width):630 = (NewtonDomain.Left param2@width)':647
         /\ mid_(NewtonDomain.Left param1@width):632 = (NewtonDomain.Left param1@width)':648
         /\ mid_(NewtonDomain.Left param0@width):620 = (NewtonDomain.Left param0@width)':649
         /\ mid_(NewtonDomain.Left return@width):634 = (NewtonDomain.Left return@width)':650
         /\ mid_(NewtonDomain.Left param2@pos):636 = (NewtonDomain.Left param2@pos)':651
         /\ mid_(NewtonDomain.Left param1@pos):638 = (NewtonDomain.Left param1@pos)':652
         /\ mid_(NewtonDomain.Left param0@pos):617 = (NewtonDomain.Left param0@pos)':653
         /\ mid_(NewtonDomain.Left return@pos):640 = (NewtonDomain.Left return@pos)':654
         /\ mid_(NewtonDomain.Left param2):619 = (NewtonDomain.Left param2)':655
         /\ mid_(NewtonDomain.Left param1):616 = (NewtonDomain.Left param1)':656
         /\ mid_(NewtonDomain.Left param0):614 = (NewtonDomain.Left param0)':657
         /\ mid_(NewtonDomain.Left return):642 = (NewtonDomain.Left return)':658
         /\ mid_(NewtonDomain.Left __cost):622 = (NewtonDomain.Left __cost)':659
         /\ 0 = K:643 /\ (K:613 + K:643) = K:660 /\ 0 <= K:660
         /\ type_err:661 = (NewtonDomain.Left param2@width)':647
         /\ type_err:662 = (NewtonDomain.Left param1@width)':648
         /\ 80 = (NewtonDomain.Left param0@width)':649
         /\ return@width:406 = (NewtonDomain.Left return@width)':650
         /\ type_err:663 = (NewtonDomain.Left param2@pos)':651
         /\ type_err:664 = (NewtonDomain.Left param1@pos)':652
         /\ 0 = (NewtonDomain.Left param0@pos)':653
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':654
         /\ 20 = (NewtonDomain.Left param2)':655
         /\ 0 = (NewtonDomain.Left param1)':656
         /\ alloc:27 = (NewtonDomain.Left param0)':657
         /\ return:404 = (NewtonDomain.Left return)':658
         /\ 0 = (NewtonDomain.Left __cost)':659)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:556 + 1)
 return := havoc:607
 param0 := fresh_param0:561
 param1 := fresh_param1:558
 param2 := fresh_param2:557
 return@pos := type_err:608
 param0@pos := fresh_param0@pos:564
 param1@pos := fresh_param1@pos:583
 param2@pos := fresh_param2@pos:581
 return@width := type_err:609
 param0@width := fresh_param0@width:567
 param1@width := fresh_param1@width:577
 param2@width := fresh_param2@width:575
 when (0 <= fresh___cost:556 /\ 0 <= (fresh___cost:556 + 1)
         /\ (fresh_param2:557 + -fresh_param1:558) < 1
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left param0):560 = fresh_param0:561)
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left param1):562 = fresh_param1:558)
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left param0@pos):563 = fresh_param0@pos:564)
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left param2):565 = (fresh_param2:557
                                                          + K:559))
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left param0@width):566 = fresh_param0@width:567)
         /\ (!(0 <= K:559)
               \/ mid_(NewtonDomain.Left __cost):568 = (fresh___cost:556
                                                          + (-2 * K:559)))
         /\ ((K:559 = 0
                /\ type_err:569 = mid_(NewtonDomain.Right return@width):570
                /\ type_err:571 = mid_(NewtonDomain.Right return@pos):572
                /\ havoc:573 = mid_(NewtonDomain.Right return):574
                /\ fresh_param2@width:575 = mid_(NewtonDomain.Left param2@width):576
                /\ fresh_param1@width:577 = mid_(NewtonDomain.Left param1@width):578
                /\ fresh_param0@width:567 = mid_(NewtonDomain.Left param0@width):566
                /\ fresh_return@width:579 = mid_(NewtonDomain.Left return@width):580
                /\ fresh_param2@pos:581 = mid_(NewtonDomain.Left param2@pos):582
                /\ fresh_param1@pos:583 = mid_(NewtonDomain.Left param1@pos):584
                /\ fresh_param0@pos:564 = mid_(NewtonDomain.Left param0@pos):563
                /\ fresh_return@pos:585 = mid_(NewtonDomain.Left return@pos):586
                /\ fresh_param2:557 = mid_(NewtonDomain.Left param2):565
                /\ fresh_param1:558 = mid_(NewtonDomain.Left param1):562
                /\ fresh_param0:561 = mid_(NewtonDomain.Left param0):560
                /\ fresh_return:587 = mid_(NewtonDomain.Left return):588
                /\ fresh___cost:556 = mid_(NewtonDomain.Left __cost):568)
               \/ (1 <= K:559 /\ 0 <= (-2 + fresh___cost:556)
                     /\ 0 <= (fresh_param2:557 + -fresh_param1:558)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):568
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param2):565
                                + -mid_(NewtonDomain.Left param1):562)))
         /\ K:589 = 0
         /\ mid_(NewtonDomain.Right return@width):570 = (NewtonDomain.Right return@width)':590
         /\ mid_(NewtonDomain.Right return@pos):572 = (NewtonDomain.Right return@pos)':591
         /\ mid_(NewtonDomain.Right return):574 = (NewtonDomain.Right return)':592
         /\ mid_(NewtonDomain.Left param2@width):576 = (NewtonDomain.Left param2@width)':593
         /\ mid_(NewtonDomain.Left param1@width):578 = (NewtonDomain.Left param1@width)':594
         /\ mid_(NewtonDomain.Left param0@width):566 = (NewtonDomain.Left param0@width)':595
         /\ mid_(NewtonDomain.Left return@width):580 = (NewtonDomain.Left return@width)':596
         /\ mid_(NewtonDomain.Left param2@pos):582 = (NewtonDomain.Left param2@pos)':597
         /\ mid_(NewtonDomain.Left param1@pos):584 = (NewtonDomain.Left param1@pos)':598
         /\ mid_(NewtonDomain.Left param0@pos):563 = (NewtonDomain.Left param0@pos)':599
         /\ mid_(NewtonDomain.Left return@pos):586 = (NewtonDomain.Left return@pos)':600
         /\ mid_(NewtonDomain.Left param2):565 = (NewtonDomain.Left param2)':601
         /\ mid_(NewtonDomain.Left param1):562 = (NewtonDomain.Left param1)':602
         /\ mid_(NewtonDomain.Left param0):560 = (NewtonDomain.Left param0)':603
         /\ mid_(NewtonDomain.Left return):588 = (NewtonDomain.Left return)':604
         /\ mid_(NewtonDomain.Left __cost):568 = (NewtonDomain.Left __cost)':605
         /\ 0 = K:589 /\ (K:559 + K:589) = K:606 /\ 0 <= K:606
         /\ type_err:168 = (NewtonDomain.Left param2@width)':593
         /\ type_err:167 = (NewtonDomain.Left param1@width)':594
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':595
         /\ return@width:406 = (NewtonDomain.Left return@width)':596
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':597
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':598
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':599
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':600
         /\ param1:160 = (NewtonDomain.Left param2)':601
         /\ 0 = (NewtonDomain.Left param1)':602
         /\ param0:157 = (NewtonDomain.Left param0)':603
         /\ return:404 = (NewtonDomain.Left return)':604
         /\ __cost:106 = (NewtonDomain.Left __cost)':605)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:543 + 1)
 return := (NewtonDomain.Right return)':528
 param0 := fresh_param0:545
 param1 := fresh_param1:546
 param2 := fresh_param2:547
 return@pos := (NewtonDomain.Right return@pos)':527
 param0@pos := fresh_param0@pos:549
 param1@pos := fresh_param1@pos:550
 param2@pos := fresh_param2@pos:551
 return@width := (NewtonDomain.Right return@width)':526
 param0@width := fresh_param0@width:553
 param1@width := fresh_param1@width:554
 param2@width := fresh_param2@width:555
 when (0 <= fresh___cost:543 /\ 0 <= (fresh___cost:543 + 1)
         /\ (fresh_param2:547 + -fresh_param1:546) < 1
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left param0):509 = fresh_param0:545)
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left param1):510 = fresh_param1:546)
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left param0@pos):511 = fresh_param0@pos:549)
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left param2):512 = (fresh_param2:547
                                                          + K:508))
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left param0@width):513 = fresh_param0@width:553)
         /\ (!(0 <= K:508)
               \/ mid_(NewtonDomain.Left __cost):514 = (fresh___cost:543
                                                          + (-2 * K:508)))
         /\ ((K:508 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):515
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):516
                /\ havoc:302 = mid_(NewtonDomain.Right return):517
                /\ fresh_param2@width:555 = mid_(NewtonDomain.Left param2@width):518
                /\ fresh_param1@width:554 = mid_(NewtonDomain.Left param1@width):519
                /\ fresh_param0@width:553 = mid_(NewtonDomain.Left param0@width):513
                /\ fresh_return@width:552 = mid_(NewtonDomain.Left return@width):520
                /\ fresh_param2@pos:551 = mid_(NewtonDomain.Left param2@pos):521
                /\ fresh_param1@pos:550 = mid_(NewtonDomain.Left param1@pos):522
                /\ fresh_param0@pos:549 = mid_(NewtonDomain.Left param0@pos):511
                /\ fresh_return@pos:548 = mid_(NewtonDomain.Left return@pos):523
                /\ fresh_param2:547 = mid_(NewtonDomain.Left param2):512
                /\ fresh_param1:546 = mid_(NewtonDomain.Left param1):510
                /\ fresh_param0:545 = mid_(NewtonDomain.Left param0):509
                /\ fresh_return:544 = mid_(NewtonDomain.Left return):524
                /\ fresh___cost:543 = mid_(NewtonDomain.Left __cost):514)
               \/ (1 <= K:508 /\ 0 <= (-2 + fresh___cost:543)
                     /\ 0 <= (fresh_param2:547 + -fresh_param1:546)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):514
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param2):512
                                + -mid_(NewtonDomain.Left param1):510)))
         /\ K:525 = 0
         /\ mid_(NewtonDomain.Right return@width):515 = (NewtonDomain.Right return@width)':526
         /\ mid_(NewtonDomain.Right return@pos):516 = (NewtonDomain.Right return@pos)':527
         /\ mid_(NewtonDomain.Right return):517 = (NewtonDomain.Right return)':528
         /\ mid_(NewtonDomain.Left param2@width):518 = (NewtonDomain.Left param2@width)':529
         /\ mid_(NewtonDomain.Left param1@width):519 = (NewtonDomain.Left param1@width)':530
         /\ mid_(NewtonDomain.Left param0@width):513 = (NewtonDomain.Left param0@width)':531
         /\ mid_(NewtonDomain.Left return@width):520 = (NewtonDomain.Left return@width)':532
         /\ mid_(NewtonDomain.Left param2@pos):521 = (NewtonDomain.Left param2@pos)':533
         /\ mid_(NewtonDomain.Left param1@pos):522 = (NewtonDomain.Left param1@pos)':534
         /\ mid_(NewtonDomain.Left param0@pos):511 = (NewtonDomain.Left param0@pos)':535
         /\ mid_(NewtonDomain.Left return@pos):523 = (NewtonDomain.Left return@pos)':536
         /\ mid_(NewtonDomain.Left param2):512 = (NewtonDomain.Left param2)':537
         /\ mid_(NewtonDomain.Left param1):510 = (NewtonDomain.Left param1)':538
         /\ mid_(NewtonDomain.Left param0):509 = (NewtonDomain.Left param0)':539
         /\ mid_(NewtonDomain.Left return):524 = (NewtonDomain.Left return)':540
         /\ mid_(NewtonDomain.Left __cost):514 = (NewtonDomain.Left __cost)':541
         /\ 0 = K:525 /\ (K:508 + K:525) = K:542 /\ 0 <= K:542
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':529
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':530
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':531
         /\ return@width:406 = (NewtonDomain.Left return@width)':532
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':533
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':534
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':535
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':536
         /\ param2:213 = (NewtonDomain.Left param2)':537
         /\ param1:160 = (NewtonDomain.Left param1)':538
         /\ param0:157 = (NewtonDomain.Left param0)':539
         /\ return:404 = (NewtonDomain.Left return)':540
         /\ __cost:106 = (NewtonDomain.Left __cost)':541)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 2:
Evaluating variable number 9 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:725
 (NewtonDomain.Left return) := fresh_return:730
 (NewtonDomain.Left param0) := fresh_param0:731
 (NewtonDomain.Left param1) := fresh_param1:732
 (NewtonDomain.Left param2) := fresh_param2:733
 (NewtonDomain.Left return@pos) := fresh_return@pos:735
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:736
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:737
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:738
 (NewtonDomain.Left return@width) := fresh_return@width:740
 (NewtonDomain.Left param0@width) := fresh_param0@width:741
 (NewtonDomain.Left param1@width) := fresh_param1@width:742
 (NewtonDomain.Left param2@width) := fresh_param2@width:743
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:725 /\ 0 <= (fresh___cost:725 + 1)
         /\ 1 <= (fresh_param2:733 + -fresh_param1:732) /\ 0 < havoc:297
         /\ (fresh_param1:732 + havoc:297) <= fresh_param2:733
         /\ 0 <= fresh___cost:670 /\ 0 <= (fresh___cost:670 + 1)
         /\ (fresh_param2:671 + -fresh_param1:672) < 1
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left param0):674 = fresh_param0:675)
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left param1):676 = fresh_param1:672)
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left param0@pos):677 = fresh_param0@pos:678)
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left param2):679 = (fresh_param2:671
                                                          + K:673))
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left param0@width):680 = fresh_param0@width:681)
         /\ (!(0 <= K:673)
               \/ mid_(NewtonDomain.Left __cost):682 = (fresh___cost:670
                                                          + (-2 * K:673)))
         /\ ((K:673 = 0
                /\ type_err:683 = mid_(NewtonDomain.Right return@width):684
                /\ type_err:685 = mid_(NewtonDomain.Right return@pos):686
                /\ havoc:687 = mid_(NewtonDomain.Right return):688
                /\ fresh_param2@width:689 = mid_(NewtonDomain.Left param2@width):690
                /\ fresh_param1@width:691 = mid_(NewtonDomain.Left param1@width):692
                /\ fresh_param0@width:681 = mid_(NewtonDomain.Left param0@width):680
                /\ fresh_return@width:693 = mid_(NewtonDomain.Left return@width):694
                /\ fresh_param2@pos:695 = mid_(NewtonDomain.Left param2@pos):696
                /\ fresh_param1@pos:697 = mid_(NewtonDomain.Left param1@pos):698
                /\ fresh_param0@pos:678 = mid_(NewtonDomain.Left param0@pos):677
                /\ fresh_return@pos:699 = mid_(NewtonDomain.Left return@pos):700
                /\ fresh_param2:671 = mid_(NewtonDomain.Left param2):679
                /\ fresh_param1:672 = mid_(NewtonDomain.Left param1):676
                /\ fresh_param0:675 = mid_(NewtonDomain.Left param0):674
                /\ fresh_return:701 = mid_(NewtonDomain.Left return):702
                /\ fresh___cost:670 = mid_(NewtonDomain.Left __cost):682)
               \/ (1 <= K:673 /\ 0 <= (-2 + fresh___cost:670)
                     /\ 0 <= (fresh_param2:671 + -fresh_param1:672)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):682
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param2):679
                                + -mid_(NewtonDomain.Left param1):676)))
         /\ K:703 = 0
         /\ mid_(NewtonDomain.Right return@width):684 = (NewtonDomain.Right return@width)':704
         /\ mid_(NewtonDomain.Right return@pos):686 = (NewtonDomain.Right return@pos)':705
         /\ mid_(NewtonDomain.Right return):688 = (NewtonDomain.Right return)':706
         /\ mid_(NewtonDomain.Left param2@width):690 = (NewtonDomain.Left param2@width)':707
         /\ mid_(NewtonDomain.Left param1@width):692 = (NewtonDomain.Left param1@width)':708
         /\ mid_(NewtonDomain.Left param0@width):680 = (NewtonDomain.Left param0@width)':709
         /\ mid_(NewtonDomain.Left return@width):694 = (NewtonDomain.Left return@width)':710
         /\ mid_(NewtonDomain.Left param2@pos):696 = (NewtonDomain.Left param2@pos)':711
         /\ mid_(NewtonDomain.Left param1@pos):698 = (NewtonDomain.Left param1@pos)':712
         /\ mid_(NewtonDomain.Left param0@pos):677 = (NewtonDomain.Left param0@pos)':713
         /\ mid_(NewtonDomain.Left return@pos):700 = (NewtonDomain.Left return@pos)':714
         /\ mid_(NewtonDomain.Left param2):679 = (NewtonDomain.Left param2)':715
         /\ mid_(NewtonDomain.Left param1):676 = (NewtonDomain.Left param1)':716
         /\ mid_(NewtonDomain.Left param0):674 = (NewtonDomain.Left param0)':717
         /\ mid_(NewtonDomain.Left return):702 = (NewtonDomain.Left return)':718
         /\ mid_(NewtonDomain.Left __cost):682 = (NewtonDomain.Left __cost)':719
         /\ 0 = K:703 /\ (K:673 + K:703) = K:720 /\ 0 <= K:720
         /\ type_err:301 = (NewtonDomain.Left param2@width)':707
         /\ type_err:300 = (NewtonDomain.Left param1@width)':708
         /\ fresh_param0@width:741 = (NewtonDomain.Left param0@width)':709
         /\ fresh_return@width:740 = (NewtonDomain.Left return@width)':710
         /\ type_err:299 = (NewtonDomain.Left param2@pos)':711
         /\ type_err:298 = (NewtonDomain.Left param1@pos)':712
         /\ fresh_param0@pos:736 = (NewtonDomain.Left param0@pos)':713
         /\ fresh_return@pos:735 = (NewtonDomain.Left return@pos)':714
         /\ fresh_param2:733 = (NewtonDomain.Left param2)':715
         /\ (havoc:297 + fresh_param1:732) = (NewtonDomain.Left param1)':716
         /\ fresh_param0:731 = (NewtonDomain.Left param0)':717
         /\ fresh_return:730 = (NewtonDomain.Left return)':718
         /\ (fresh___cost:725 + 1) = (NewtonDomain.Left __cost)':719
         /\ (NewtonDomain.Left __cost):407 = (fresh___cost:670 + 1)
         /\ (NewtonDomain.Right m2):744 = ((havoc:297 + fresh_param1:732)
                                             + -1)
         /\ (NewtonDomain.Right a):745 = fresh_param0:731
         /\ (NewtonDomain.Right lo):746 = fresh_param1:732
         /\ (NewtonDomain.Right hi):747 = fresh_param2:733
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':706
         /\ (NewtonDomain.Left param0):413 = fresh_param0:731
         /\ (NewtonDomain.Left param1):414 = fresh_param1:732
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:732)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):748 = fresh_param0@pos:736
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':705
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:736
         /\ (NewtonDomain.Left param1@pos):419 = type_err:721
         /\ (NewtonDomain.Left param2@pos):420 = type_err:722
         /\ (NewtonDomain.Right a@width):749 = fresh_param0@width:741
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':704
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:741
         /\ (NewtonDomain.Left param1@width):424 = type_err:723
         /\ (NewtonDomain.Left param2@width):425 = type_err:724)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           (((3 * (NewtonDomain.Left __cost)':438)
               + (4 * (NewtonDomain.Left param2)':442))) <= (1)*(((3
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    4
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + (-2)*1
           (((NewtonDomain.Left __cost)':438
               + (2 * (NewtonDomain.Left param2)':442))) <= (1)*(((NewtonDomain.Left __cost):407
                                                                    + (
                                                                    2
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + 1
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:787)
            \/ mid_(NewtonDomain.Left param1):801 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:787)
                 \/ mid_(NewtonDomain.Left param0@pos):798 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:787)
                 \/ mid_(NewtonDomain.Left param0):802 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:787)
                 \/ mid_(NewtonDomain.Left param0@width):794 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:787)
                 \/ ((3 * mid_(NewtonDomain.Left __cost):804)
                       + (4 * mid_(NewtonDomain.Left param2):800)) <= (
                    ((3 * (NewtonDomain.Left __cost):407)
                       + (4 * (NewtonDomain.Left param2):415)) + (-2 * K:787)))
           /\ (!(0 <= K:787)
                 \/ (mid_(NewtonDomain.Left __cost):804
                       + (2 * mid_(NewtonDomain.Left param2):800)) <= (
                    ((NewtonDomain.Left __cost):407
                       + (2 * (NewtonDomain.Left param2):415)) + K:787))
           /\ (!(0 <= K:787)
                 \/ (-mid_(NewtonDomain.Left __cost):804
                       + (-2 * mid_(NewtonDomain.Left param2):800)) <= (
                    -(NewtonDomain.Left __cost):407
                      + (-2 * (NewtonDomain.Left param2):415)))
           /\ ((K:787 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):789
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):790
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):791
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):792
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):793
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):794
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):795
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):796
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):797
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):798
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):799
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):800
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):801
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):802
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):803
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):804)
                 \/ (1 <= K:787
                       /\ 0 <= (-(NewtonDomain.Left param1):414
                                  + (NewtonDomain.Left param2):415)
                       /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):801
                                  + mid_(NewtonDomain.Left param2):800)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):804))
           /\ K:788 = 0
           /\ mid_(NewtonDomain.Right return@width):789 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):790 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):791 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):792 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):793 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):794 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):795 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):796 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):797 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):798 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):799 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):800 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):801 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):802 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):803 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):804 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:788 /\ (K:787 + K:788) = K:786 /\ 0 <= K:786)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:907 + 1)
 return := 0
 param0 := fresh_param0:915
 param1 := fresh_param1:909
 param2 := fresh_param2:908
 return@pos := type_err:965
 param0@pos := fresh_param0@pos:913
 param1@pos := fresh_param1@pos:934
 param2@pos := fresh_param2@pos:932
 return@width := type_err:966
 param0@width := fresh_param0@width:917
 param1@width := fresh_param1@width:928
 param2@width := fresh_param2@width:926
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:907
         /\ 0 <= (fresh___cost:907 + 1)
         /\ (fresh_param2:908 + -fresh_param1:909) < 1
         /\ (!(0 <= K:910)
               \/ mid_(NewtonDomain.Left param1):911 = fresh_param1:909)
         /\ (!(0 <= K:910)
               \/ mid_(NewtonDomain.Left param0@pos):912 = fresh_param0@pos:913)
         /\ (!(0 <= K:910)
               \/ mid_(NewtonDomain.Left param0):914 = fresh_param0:915)
         /\ (!(0 <= K:910)
               \/ mid_(NewtonDomain.Left param0@width):916 = fresh_param0@width:917)
         /\ (!(0 <= K:910)
               \/ ((3 * mid_(NewtonDomain.Left __cost):918)
                     + (4 * mid_(NewtonDomain.Left param2):919)) <= (
                  ((3 * fresh___cost:907) + (4 * fresh_param2:908))
                    + (-2 * K:910)))
         /\ (!(0 <= K:910)
               \/ (mid_(NewtonDomain.Left __cost):918
                     + (2 * mid_(NewtonDomain.Left param2):919)) <= (
                  (fresh___cost:907 + (2 * fresh_param2:908)) + K:910))
         /\ (!(0 <= K:910)
               \/ (-mid_(NewtonDomain.Left __cost):918
                     + (-2 * mid_(NewtonDomain.Left param2):919)) <= (
                  -fresh___cost:907 + (-2 * fresh_param2:908)))
         /\ ((K:910 = 0
                /\ type_err:920 = mid_(NewtonDomain.Right return@width):921
                /\ type_err:922 = mid_(NewtonDomain.Right return@pos):923
                /\ havoc:924 = mid_(NewtonDomain.Right return):925
                /\ fresh_param2@width:926 = mid_(NewtonDomain.Left param2@width):927
                /\ fresh_param1@width:928 = mid_(NewtonDomain.Left param1@width):929
                /\ fresh_param0@width:917 = mid_(NewtonDomain.Left param0@width):916
                /\ fresh_return@width:930 = mid_(NewtonDomain.Left return@width):931
                /\ fresh_param2@pos:932 = mid_(NewtonDomain.Left param2@pos):933
                /\ fresh_param1@pos:934 = mid_(NewtonDomain.Left param1@pos):935
                /\ fresh_param0@pos:913 = mid_(NewtonDomain.Left param0@pos):912
                /\ fresh_return@pos:936 = mid_(NewtonDomain.Left return@pos):937
                /\ fresh_param2:908 = mid_(NewtonDomain.Left param2):919
                /\ fresh_param1:909 = mid_(NewtonDomain.Left param1):911
                /\ fresh_param0:915 = mid_(NewtonDomain.Left param0):914
                /\ fresh_return:938 = mid_(NewtonDomain.Left return):939
                /\ fresh___cost:907 = mid_(NewtonDomain.Left __cost):918)
               \/ (1 <= K:910 /\ 0 <= (-fresh_param1:909 + fresh_param2:908)
                     /\ 0 <= (-2 + fresh___cost:907)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):911
                                + mid_(NewtonDomain.Left param2):919)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):918))
         /\ K:940 = 0
         /\ mid_(NewtonDomain.Right return@width):921 = (NewtonDomain.Right return@width)':941
         /\ mid_(NewtonDomain.Right return@pos):923 = (NewtonDomain.Right return@pos)':942
         /\ mid_(NewtonDomain.Right return):925 = (NewtonDomain.Right return)':943
         /\ mid_(NewtonDomain.Left param2@width):927 = (NewtonDomain.Left param2@width)':944
         /\ mid_(NewtonDomain.Left param1@width):929 = (NewtonDomain.Left param1@width)':945
         /\ mid_(NewtonDomain.Left param0@width):916 = (NewtonDomain.Left param0@width)':946
         /\ mid_(NewtonDomain.Left return@width):931 = (NewtonDomain.Left return@width)':947
         /\ mid_(NewtonDomain.Left param2@pos):933 = (NewtonDomain.Left param2@pos)':948
         /\ mid_(NewtonDomain.Left param1@pos):935 = (NewtonDomain.Left param1@pos)':949
         /\ mid_(NewtonDomain.Left param0@pos):912 = (NewtonDomain.Left param0@pos)':950
         /\ mid_(NewtonDomain.Left return@pos):937 = (NewtonDomain.Left return@pos)':951
         /\ mid_(NewtonDomain.Left param2):919 = (NewtonDomain.Left param2)':952
         /\ mid_(NewtonDomain.Left param1):911 = (NewtonDomain.Left param1)':953
         /\ mid_(NewtonDomain.Left param0):914 = (NewtonDomain.Left param0)':954
         /\ mid_(NewtonDomain.Left return):939 = (NewtonDomain.Left return)':955
         /\ mid_(NewtonDomain.Left __cost):918 = (NewtonDomain.Left __cost)':956
         /\ 0 = K:940 /\ (K:910 + K:940) = K:957 /\ 0 <= K:957
         /\ type_err:958 = (NewtonDomain.Left param2@width)':944
         /\ type_err:959 = (NewtonDomain.Left param1@width)':945
         /\ 80 = (NewtonDomain.Left param0@width)':946
         /\ return@width:406 = (NewtonDomain.Left return@width)':947
         /\ type_err:960 = (NewtonDomain.Left param2@pos)':948
         /\ type_err:961 = (NewtonDomain.Left param1@pos)':949
         /\ 0 = (NewtonDomain.Left param0@pos)':950
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':951
         /\ 20 = (NewtonDomain.Left param2)':952
         /\ 0 = (NewtonDomain.Left param1)':953
         /\ alloc:27 = (NewtonDomain.Left param0)':954
         /\ return:404 = (NewtonDomain.Left return)':955
         /\ 0 = (NewtonDomain.Left __cost)':956)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:853 + 1)
 return := havoc:904
 param0 := fresh_param0:861
 param1 := fresh_param1:855
 param2 := fresh_param2:854
 return@pos := type_err:905
 param0@pos := fresh_param0@pos:859
 param1@pos := fresh_param1@pos:880
 param2@pos := fresh_param2@pos:878
 return@width := type_err:906
 param0@width := fresh_param0@width:863
 param1@width := fresh_param1@width:874
 param2@width := fresh_param2@width:872
 when (0 <= fresh___cost:853 /\ 0 <= (fresh___cost:853 + 1)
         /\ (fresh_param2:854 + -fresh_param1:855) < 1
         /\ (!(0 <= K:856)
               \/ mid_(NewtonDomain.Left param1):857 = fresh_param1:855)
         /\ (!(0 <= K:856)
               \/ mid_(NewtonDomain.Left param0@pos):858 = fresh_param0@pos:859)
         /\ (!(0 <= K:856)
               \/ mid_(NewtonDomain.Left param0):860 = fresh_param0:861)
         /\ (!(0 <= K:856)
               \/ mid_(NewtonDomain.Left param0@width):862 = fresh_param0@width:863)
         /\ (!(0 <= K:856)
               \/ ((3 * mid_(NewtonDomain.Left __cost):864)
                     + (4 * mid_(NewtonDomain.Left param2):865)) <= (
                  ((3 * fresh___cost:853) + (4 * fresh_param2:854))
                    + (-2 * K:856)))
         /\ (!(0 <= K:856)
               \/ (mid_(NewtonDomain.Left __cost):864
                     + (2 * mid_(NewtonDomain.Left param2):865)) <= (
                  (fresh___cost:853 + (2 * fresh_param2:854)) + K:856))
         /\ (!(0 <= K:856)
               \/ (-mid_(NewtonDomain.Left __cost):864
                     + (-2 * mid_(NewtonDomain.Left param2):865)) <= (
                  -fresh___cost:853 + (-2 * fresh_param2:854)))
         /\ ((K:856 = 0
                /\ type_err:866 = mid_(NewtonDomain.Right return@width):867
                /\ type_err:868 = mid_(NewtonDomain.Right return@pos):869
                /\ havoc:870 = mid_(NewtonDomain.Right return):871
                /\ fresh_param2@width:872 = mid_(NewtonDomain.Left param2@width):873
                /\ fresh_param1@width:874 = mid_(NewtonDomain.Left param1@width):875
                /\ fresh_param0@width:863 = mid_(NewtonDomain.Left param0@width):862
                /\ fresh_return@width:876 = mid_(NewtonDomain.Left return@width):877
                /\ fresh_param2@pos:878 = mid_(NewtonDomain.Left param2@pos):879
                /\ fresh_param1@pos:880 = mid_(NewtonDomain.Left param1@pos):881
                /\ fresh_param0@pos:859 = mid_(NewtonDomain.Left param0@pos):858
                /\ fresh_return@pos:882 = mid_(NewtonDomain.Left return@pos):883
                /\ fresh_param2:854 = mid_(NewtonDomain.Left param2):865
                /\ fresh_param1:855 = mid_(NewtonDomain.Left param1):857
                /\ fresh_param0:861 = mid_(NewtonDomain.Left param0):860
                /\ fresh_return:884 = mid_(NewtonDomain.Left return):885
                /\ fresh___cost:853 = mid_(NewtonDomain.Left __cost):864)
               \/ (1 <= K:856 /\ 0 <= (-fresh_param1:855 + fresh_param2:854)
                     /\ 0 <= (-2 + fresh___cost:853)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):857
                                + mid_(NewtonDomain.Left param2):865)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):864))
         /\ K:886 = 0
         /\ mid_(NewtonDomain.Right return@width):867 = (NewtonDomain.Right return@width)':887
         /\ mid_(NewtonDomain.Right return@pos):869 = (NewtonDomain.Right return@pos)':888
         /\ mid_(NewtonDomain.Right return):871 = (NewtonDomain.Right return)':889
         /\ mid_(NewtonDomain.Left param2@width):873 = (NewtonDomain.Left param2@width)':890
         /\ mid_(NewtonDomain.Left param1@width):875 = (NewtonDomain.Left param1@width)':891
         /\ mid_(NewtonDomain.Left param0@width):862 = (NewtonDomain.Left param0@width)':892
         /\ mid_(NewtonDomain.Left return@width):877 = (NewtonDomain.Left return@width)':893
         /\ mid_(NewtonDomain.Left param2@pos):879 = (NewtonDomain.Left param2@pos)':894
         /\ mid_(NewtonDomain.Left param1@pos):881 = (NewtonDomain.Left param1@pos)':895
         /\ mid_(NewtonDomain.Left param0@pos):858 = (NewtonDomain.Left param0@pos)':896
         /\ mid_(NewtonDomain.Left return@pos):883 = (NewtonDomain.Left return@pos)':897
         /\ mid_(NewtonDomain.Left param2):865 = (NewtonDomain.Left param2)':898
         /\ mid_(NewtonDomain.Left param1):857 = (NewtonDomain.Left param1)':899
         /\ mid_(NewtonDomain.Left param0):860 = (NewtonDomain.Left param0)':900
         /\ mid_(NewtonDomain.Left return):885 = (NewtonDomain.Left return)':901
         /\ mid_(NewtonDomain.Left __cost):864 = (NewtonDomain.Left __cost)':902
         /\ 0 = K:886 /\ (K:856 + K:886) = K:903 /\ 0 <= K:903
         /\ type_err:168 = (NewtonDomain.Left param2@width)':890
         /\ type_err:167 = (NewtonDomain.Left param1@width)':891
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':892
         /\ return@width:406 = (NewtonDomain.Left return@width)':893
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':894
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':895
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':896
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':897
         /\ param1:160 = (NewtonDomain.Left param2)':898
         /\ 0 = (NewtonDomain.Left param1)':899
         /\ param0:157 = (NewtonDomain.Left param0)':900
         /\ return:404 = (NewtonDomain.Left return)':901
         /\ __cost:106 = (NewtonDomain.Left __cost)':902)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:840 + 1)
 return := (NewtonDomain.Right return)':825
 param0 := fresh_param0:842
 param1 := fresh_param1:843
 param2 := fresh_param2:844
 return@pos := (NewtonDomain.Right return@pos)':824
 param0@pos := fresh_param0@pos:846
 param1@pos := fresh_param1@pos:847
 param2@pos := fresh_param2@pos:848
 return@width := (NewtonDomain.Right return@width)':823
 param0@width := fresh_param0@width:850
 param1@width := fresh_param1@width:851
 param2@width := fresh_param2@width:852
 when (0 <= fresh___cost:840 /\ 0 <= (fresh___cost:840 + 1)
         /\ (fresh_param2:844 + -fresh_param1:843) < 1
         /\ (!(0 <= K:805)
               \/ mid_(NewtonDomain.Left param1):806 = fresh_param1:843)
         /\ (!(0 <= K:805)
               \/ mid_(NewtonDomain.Left param0@pos):807 = fresh_param0@pos:846)
         /\ (!(0 <= K:805)
               \/ mid_(NewtonDomain.Left param0):808 = fresh_param0:842)
         /\ (!(0 <= K:805)
               \/ mid_(NewtonDomain.Left param0@width):809 = fresh_param0@width:850)
         /\ (!(0 <= K:805)
               \/ ((3 * mid_(NewtonDomain.Left __cost):810)
                     + (4 * mid_(NewtonDomain.Left param2):811)) <= (
                  ((3 * fresh___cost:840) + (4 * fresh_param2:844))
                    + (-2 * K:805)))
         /\ (!(0 <= K:805)
               \/ (mid_(NewtonDomain.Left __cost):810
                     + (2 * mid_(NewtonDomain.Left param2):811)) <= (
                  (fresh___cost:840 + (2 * fresh_param2:844)) + K:805))
         /\ (!(0 <= K:805)
               \/ (-mid_(NewtonDomain.Left __cost):810
                     + (-2 * mid_(NewtonDomain.Left param2):811)) <= (
                  -fresh___cost:840 + (-2 * fresh_param2:844)))
         /\ ((K:805 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):812
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):813
                /\ havoc:302 = mid_(NewtonDomain.Right return):814
                /\ fresh_param2@width:852 = mid_(NewtonDomain.Left param2@width):815
                /\ fresh_param1@width:851 = mid_(NewtonDomain.Left param1@width):816
                /\ fresh_param0@width:850 = mid_(NewtonDomain.Left param0@width):809
                /\ fresh_return@width:849 = mid_(NewtonDomain.Left return@width):817
                /\ fresh_param2@pos:848 = mid_(NewtonDomain.Left param2@pos):818
                /\ fresh_param1@pos:847 = mid_(NewtonDomain.Left param1@pos):819
                /\ fresh_param0@pos:846 = mid_(NewtonDomain.Left param0@pos):807
                /\ fresh_return@pos:845 = mid_(NewtonDomain.Left return@pos):820
                /\ fresh_param2:844 = mid_(NewtonDomain.Left param2):811
                /\ fresh_param1:843 = mid_(NewtonDomain.Left param1):806
                /\ fresh_param0:842 = mid_(NewtonDomain.Left param0):808
                /\ fresh_return:841 = mid_(NewtonDomain.Left return):821
                /\ fresh___cost:840 = mid_(NewtonDomain.Left __cost):810)
               \/ (1 <= K:805 /\ 0 <= (-fresh_param1:843 + fresh_param2:844)
                     /\ 0 <= (-2 + fresh___cost:840)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):806
                                + mid_(NewtonDomain.Left param2):811)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):810))
         /\ K:822 = 0
         /\ mid_(NewtonDomain.Right return@width):812 = (NewtonDomain.Right return@width)':823
         /\ mid_(NewtonDomain.Right return@pos):813 = (NewtonDomain.Right return@pos)':824
         /\ mid_(NewtonDomain.Right return):814 = (NewtonDomain.Right return)':825
         /\ mid_(NewtonDomain.Left param2@width):815 = (NewtonDomain.Left param2@width)':826
         /\ mid_(NewtonDomain.Left param1@width):816 = (NewtonDomain.Left param1@width)':827
         /\ mid_(NewtonDomain.Left param0@width):809 = (NewtonDomain.Left param0@width)':828
         /\ mid_(NewtonDomain.Left return@width):817 = (NewtonDomain.Left return@width)':829
         /\ mid_(NewtonDomain.Left param2@pos):818 = (NewtonDomain.Left param2@pos)':830
         /\ mid_(NewtonDomain.Left param1@pos):819 = (NewtonDomain.Left param1@pos)':831
         /\ mid_(NewtonDomain.Left param0@pos):807 = (NewtonDomain.Left param0@pos)':832
         /\ mid_(NewtonDomain.Left return@pos):820 = (NewtonDomain.Left return@pos)':833
         /\ mid_(NewtonDomain.Left param2):811 = (NewtonDomain.Left param2)':834
         /\ mid_(NewtonDomain.Left param1):806 = (NewtonDomain.Left param1)':835
         /\ mid_(NewtonDomain.Left param0):808 = (NewtonDomain.Left param0)':836
         /\ mid_(NewtonDomain.Left return):821 = (NewtonDomain.Left return)':837
         /\ mid_(NewtonDomain.Left __cost):810 = (NewtonDomain.Left __cost)':838
         /\ 0 = K:822 /\ (K:805 + K:822) = K:839 /\ 0 <= K:839
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':826
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':827
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':828
         /\ return@width:406 = (NewtonDomain.Left return@width)':829
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':830
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':831
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':832
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':833
         /\ param2:213 = (NewtonDomain.Left param2)':834
         /\ param1:160 = (NewtonDomain.Left param1)':835
         /\ param0:157 = (NewtonDomain.Left param0)':836
         /\ return:404 = (NewtonDomain.Left return)':837
         /\ __cost:106 = (NewtonDomain.Left __cost)':838)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 3:
Evaluating variable number 9 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:1022
 (NewtonDomain.Left return) := fresh_return:1027
 (NewtonDomain.Left param0) := fresh_param0:1028
 (NewtonDomain.Left param1) := fresh_param1:1029
 (NewtonDomain.Left param2) := fresh_param2:1030
 (NewtonDomain.Left return@pos) := fresh_return@pos:1032
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:1033
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:1034
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:1035
 (NewtonDomain.Left return@width) := fresh_return@width:1037
 (NewtonDomain.Left param0@width) := fresh_param0@width:1038
 (NewtonDomain.Left param1@width) := fresh_param1@width:1039
 (NewtonDomain.Left param2@width) := fresh_param2@width:1040
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:1022 /\ 0 <= (fresh___cost:1022 + 1)
         /\ 1 <= (fresh_param2:1030 + -fresh_param1:1029) /\ 0 < havoc:297
         /\ (fresh_param1:1029 + havoc:297) <= fresh_param2:1030
         /\ 0 <= fresh___cost:967 /\ 0 <= (fresh___cost:967 + 1)
         /\ (fresh_param2:968 + -fresh_param1:969) < 1
         /\ (!(0 <= K:970)
               \/ mid_(NewtonDomain.Left param1):971 = fresh_param1:969)
         /\ (!(0 <= K:970)
               \/ mid_(NewtonDomain.Left param0@pos):972 = fresh_param0@pos:973)
         /\ (!(0 <= K:970)
               \/ mid_(NewtonDomain.Left param0):974 = fresh_param0:975)
         /\ (!(0 <= K:970)
               \/ mid_(NewtonDomain.Left param0@width):976 = fresh_param0@width:977)
         /\ (!(0 <= K:970)
               \/ ((3 * mid_(NewtonDomain.Left __cost):978)
                     + (4 * mid_(NewtonDomain.Left param2):979)) <= (
                  ((3 * fresh___cost:967) + (4 * fresh_param2:968))
                    + (-2 * K:970)))
         /\ (!(0 <= K:970)
               \/ (mid_(NewtonDomain.Left __cost):978
                     + (2 * mid_(NewtonDomain.Left param2):979)) <= (
                  (fresh___cost:967 + (2 * fresh_param2:968)) + K:970))
         /\ (!(0 <= K:970)
               \/ (-mid_(NewtonDomain.Left __cost):978
                     + (-2 * mid_(NewtonDomain.Left param2):979)) <= (
                  -fresh___cost:967 + (-2 * fresh_param2:968)))
         /\ ((K:970 = 0
                /\ type_err:980 = mid_(NewtonDomain.Right return@width):981
                /\ type_err:982 = mid_(NewtonDomain.Right return@pos):983
                /\ havoc:984 = mid_(NewtonDomain.Right return):985
                /\ fresh_param2@width:986 = mid_(NewtonDomain.Left param2@width):987
                /\ fresh_param1@width:988 = mid_(NewtonDomain.Left param1@width):989
                /\ fresh_param0@width:977 = mid_(NewtonDomain.Left param0@width):976
                /\ fresh_return@width:990 = mid_(NewtonDomain.Left return@width):991
                /\ fresh_param2@pos:992 = mid_(NewtonDomain.Left param2@pos):993
                /\ fresh_param1@pos:994 = mid_(NewtonDomain.Left param1@pos):995
                /\ fresh_param0@pos:973 = mid_(NewtonDomain.Left param0@pos):972
                /\ fresh_return@pos:996 = mid_(NewtonDomain.Left return@pos):997
                /\ fresh_param2:968 = mid_(NewtonDomain.Left param2):979
                /\ fresh_param1:969 = mid_(NewtonDomain.Left param1):971
                /\ fresh_param0:975 = mid_(NewtonDomain.Left param0):974
                /\ fresh_return:998 = mid_(NewtonDomain.Left return):999
                /\ fresh___cost:967 = mid_(NewtonDomain.Left __cost):978)
               \/ (1 <= K:970 /\ 0 <= (-fresh_param1:969 + fresh_param2:968)
                     /\ 0 <= (-2 + fresh___cost:967)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):971
                                + mid_(NewtonDomain.Left param2):979)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):978))
         /\ K:1000 = 0
         /\ mid_(NewtonDomain.Right return@width):981 = (NewtonDomain.Right return@width)':1001
         /\ mid_(NewtonDomain.Right return@pos):983 = (NewtonDomain.Right return@pos)':1002
         /\ mid_(NewtonDomain.Right return):985 = (NewtonDomain.Right return)':1003
         /\ mid_(NewtonDomain.Left param2@width):987 = (NewtonDomain.Left param2@width)':1004
         /\ mid_(NewtonDomain.Left param1@width):989 = (NewtonDomain.Left param1@width)':1005
         /\ mid_(NewtonDomain.Left param0@width):976 = (NewtonDomain.Left param0@width)':1006
         /\ mid_(NewtonDomain.Left return@width):991 = (NewtonDomain.Left return@width)':1007
         /\ mid_(NewtonDomain.Left param2@pos):993 = (NewtonDomain.Left param2@pos)':1008
         /\ mid_(NewtonDomain.Left param1@pos):995 = (NewtonDomain.Left param1@pos)':1009
         /\ mid_(NewtonDomain.Left param0@pos):972 = (NewtonDomain.Left param0@pos)':1010
         /\ mid_(NewtonDomain.Left return@pos):997 = (NewtonDomain.Left return@pos)':1011
         /\ mid_(NewtonDomain.Left param2):979 = (NewtonDomain.Left param2)':1012
         /\ mid_(NewtonDomain.Left param1):971 = (NewtonDomain.Left param1)':1013
         /\ mid_(NewtonDomain.Left param0):974 = (NewtonDomain.Left param0)':1014
         /\ mid_(NewtonDomain.Left return):999 = (NewtonDomain.Left return)':1015
         /\ mid_(NewtonDomain.Left __cost):978 = (NewtonDomain.Left __cost)':1016
         /\ 0 = K:1000 /\ (K:970 + K:1000) = K:1017 /\ 0 <= K:1017
         /\ type_err:301 = (NewtonDomain.Left param2@width)':1004
         /\ type_err:300 = (NewtonDomain.Left param1@width)':1005
         /\ fresh_param0@width:1038 = (NewtonDomain.Left param0@width)':1006
         /\ fresh_return@width:1037 = (NewtonDomain.Left return@width)':1007
         /\ type_err:299 = (NewtonDomain.Left param2@pos)':1008
         /\ type_err:298 = (NewtonDomain.Left param1@pos)':1009
         /\ fresh_param0@pos:1033 = (NewtonDomain.Left param0@pos)':1010
         /\ fresh_return@pos:1032 = (NewtonDomain.Left return@pos)':1011
         /\ fresh_param2:1030 = (NewtonDomain.Left param2)':1012
         /\ (havoc:297 + fresh_param1:1029) = (NewtonDomain.Left param1)':1013
         /\ fresh_param0:1028 = (NewtonDomain.Left param0)':1014
         /\ fresh_return:1027 = (NewtonDomain.Left return)':1015
         /\ (fresh___cost:1022 + 1) = (NewtonDomain.Left __cost)':1016
         /\ (NewtonDomain.Left __cost):407 = (fresh___cost:967 + 1)
         /\ (NewtonDomain.Right m2):1041 = ((havoc:297 + fresh_param1:1029)
                                              + -1)
         /\ (NewtonDomain.Right a):1042 = fresh_param0:1028
         /\ (NewtonDomain.Right lo):1043 = fresh_param1:1029
         /\ (NewtonDomain.Right hi):1044 = fresh_param2:1030
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':1003
         /\ (NewtonDomain.Left param0):413 = fresh_param0:1028
         /\ (NewtonDomain.Left param1):414 = fresh_param1:1029
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:1029)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):1045 = fresh_param0@pos:1033
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':1002
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:1033
         /\ (NewtonDomain.Left param1@pos):419 = type_err:1018
         /\ (NewtonDomain.Left param2@pos):420 = type_err:1019
         /\ (NewtonDomain.Right a@width):1046 = fresh_param0@width:1038
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':1001
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:1038
         /\ (NewtonDomain.Left param1@width):424 = type_err:1020
         /\ (NewtonDomain.Left param2@width):425 = type_err:1021)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           (((7 * (NewtonDomain.Left __cost)':438)
               + (8 * (NewtonDomain.Left param2)':442))) <= (1)*(((7
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    8
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + (-6)*1
           (((5 * (NewtonDomain.Left __cost)':438)
               + (8 * (NewtonDomain.Left param2)':442))) <= (1)*(((5
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    8
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + 5*1
           (((3 * (NewtonDomain.Left __cost)':438)
               + (4 * (NewtonDomain.Left param2)':442))) <= (1)*(((3
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    4
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + (-1)*1
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:1084)
            \/ mid_(NewtonDomain.Left param1):1098 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:1084)
                 \/ mid_(NewtonDomain.Left param0@pos):1095 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:1084)
                 \/ mid_(NewtonDomain.Left param0):1099 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:1084)
                 \/ mid_(NewtonDomain.Left param0@width):1091 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:1084)
                 \/ ((7 * mid_(NewtonDomain.Left __cost):1101)
                       + (8 * mid_(NewtonDomain.Left param2):1097)) <= (
                    ((7 * (NewtonDomain.Left __cost):407)
                       + (8 * (NewtonDomain.Left param2):415))
                      + (-6 * K:1084)))
           /\ (!(0 <= K:1084)
                 \/ ((5 * mid_(NewtonDomain.Left __cost):1101)
                       + (8 * mid_(NewtonDomain.Left param2):1097)) <= (
                    ((5 * (NewtonDomain.Left __cost):407)
                       + (8 * (NewtonDomain.Left param2):415)) + (5 * K:1084)))
           /\ (!(0 <= K:1084)
                 \/ ((3 * mid_(NewtonDomain.Left __cost):1101)
                       + (4 * mid_(NewtonDomain.Left param2):1097)) <= (
                    ((3 * (NewtonDomain.Left __cost):407)
                       + (4 * (NewtonDomain.Left param2):415)) + -K:1084))
           /\ (!(0 <= K:1084)
                 \/ (-mid_(NewtonDomain.Left __cost):1101
                       + (-2 * mid_(NewtonDomain.Left param2):1097)) <= (
                    -(NewtonDomain.Left __cost):407
                      + (-2 * (NewtonDomain.Left param2):415)))
           /\ ((K:1084 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):1086
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):1087
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):1088
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):1089
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):1090
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):1091
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):1092
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):1093
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):1094
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):1095
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):1096
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):1097
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):1098
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):1099
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):1100
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):1101)
                 \/ (1 <= K:1084
                       /\ 0 <= (-(NewtonDomain.Left param1):414
                                  + (NewtonDomain.Left param2):415)
                       /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1098
                                  + mid_(NewtonDomain.Left param2):1097)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):1101))
           /\ K:1085 = 0
           /\ mid_(NewtonDomain.Right return@width):1086 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):1087 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):1088 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):1089 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):1090 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):1091 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):1092 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):1093 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):1094 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):1095 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):1096 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):1097 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):1098 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):1099 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):1100 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):1101 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:1085 /\ (K:1084 + K:1085) = K:1083 /\ 0 <= K:1083)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1204 + 1)
 return := 0
 param0 := fresh_param0:1212
 param1 := fresh_param1:1206
 param2 := fresh_param2:1205
 return@pos := type_err:1262
 param0@pos := fresh_param0@pos:1210
 param1@pos := fresh_param1@pos:1231
 param2@pos := fresh_param2@pos:1229
 return@width := type_err:1263
 param0@width := fresh_param0@width:1214
 param1@width := fresh_param1@width:1225
 param2@width := fresh_param2@width:1223
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:1204
         /\ 0 <= (fresh___cost:1204 + 1)
         /\ (fresh_param2:1205 + -fresh_param1:1206) < 1
         /\ (!(0 <= K:1207)
               \/ mid_(NewtonDomain.Left param1):1208 = fresh_param1:1206)
         /\ (!(0 <= K:1207)
               \/ mid_(NewtonDomain.Left param0@pos):1209 = fresh_param0@pos:1210)
         /\ (!(0 <= K:1207)
               \/ mid_(NewtonDomain.Left param0):1211 = fresh_param0:1212)
         /\ (!(0 <= K:1207)
               \/ mid_(NewtonDomain.Left param0@width):1213 = fresh_param0@width:1214)
         /\ (!(0 <= K:1207)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1215)
                     + (8 * mid_(NewtonDomain.Left param2):1216)) <= (
                  ((7 * fresh___cost:1204) + (8 * fresh_param2:1205))
                    + (-6 * K:1207)))
         /\ (!(0 <= K:1207)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1215)
                     + (8 * mid_(NewtonDomain.Left param2):1216)) <= (
                  ((5 * fresh___cost:1204) + (8 * fresh_param2:1205))
                    + (5 * K:1207)))
         /\ (!(0 <= K:1207)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1215)
                     + (4 * mid_(NewtonDomain.Left param2):1216)) <= (
                  ((3 * fresh___cost:1204) + (4 * fresh_param2:1205))
                    + -K:1207))
         /\ (!(0 <= K:1207)
               \/ (-mid_(NewtonDomain.Left __cost):1215
                     + (-2 * mid_(NewtonDomain.Left param2):1216)) <= (
                  -fresh___cost:1204 + (-2 * fresh_param2:1205)))
         /\ ((K:1207 = 0
                /\ type_err:1217 = mid_(NewtonDomain.Right return@width):1218
                /\ type_err:1219 = mid_(NewtonDomain.Right return@pos):1220
                /\ havoc:1221 = mid_(NewtonDomain.Right return):1222
                /\ fresh_param2@width:1223 = mid_(NewtonDomain.Left param2@width):1224
                /\ fresh_param1@width:1225 = mid_(NewtonDomain.Left param1@width):1226
                /\ fresh_param0@width:1214 = mid_(NewtonDomain.Left param0@width):1213
                /\ fresh_return@width:1227 = mid_(NewtonDomain.Left return@width):1228
                /\ fresh_param2@pos:1229 = mid_(NewtonDomain.Left param2@pos):1230
                /\ fresh_param1@pos:1231 = mid_(NewtonDomain.Left param1@pos):1232
                /\ fresh_param0@pos:1210 = mid_(NewtonDomain.Left param0@pos):1209
                /\ fresh_return@pos:1233 = mid_(NewtonDomain.Left return@pos):1234
                /\ fresh_param2:1205 = mid_(NewtonDomain.Left param2):1216
                /\ fresh_param1:1206 = mid_(NewtonDomain.Left param1):1208
                /\ fresh_param0:1212 = mid_(NewtonDomain.Left param0):1211
                /\ fresh_return:1235 = mid_(NewtonDomain.Left return):1236
                /\ fresh___cost:1204 = mid_(NewtonDomain.Left __cost):1215)
               \/ (1 <= K:1207
                     /\ 0 <= (-fresh_param1:1206 + fresh_param2:1205)
                     /\ 0 <= (-2 + fresh___cost:1204)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1208
                                + mid_(NewtonDomain.Left param2):1216)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1215))
         /\ K:1237 = 0
         /\ mid_(NewtonDomain.Right return@width):1218 = (NewtonDomain.Right return@width)':1238
         /\ mid_(NewtonDomain.Right return@pos):1220 = (NewtonDomain.Right return@pos)':1239
         /\ mid_(NewtonDomain.Right return):1222 = (NewtonDomain.Right return)':1240
         /\ mid_(NewtonDomain.Left param2@width):1224 = (NewtonDomain.Left param2@width)':1241
         /\ mid_(NewtonDomain.Left param1@width):1226 = (NewtonDomain.Left param1@width)':1242
         /\ mid_(NewtonDomain.Left param0@width):1213 = (NewtonDomain.Left param0@width)':1243
         /\ mid_(NewtonDomain.Left return@width):1228 = (NewtonDomain.Left return@width)':1244
         /\ mid_(NewtonDomain.Left param2@pos):1230 = (NewtonDomain.Left param2@pos)':1245
         /\ mid_(NewtonDomain.Left param1@pos):1232 = (NewtonDomain.Left param1@pos)':1246
         /\ mid_(NewtonDomain.Left param0@pos):1209 = (NewtonDomain.Left param0@pos)':1247
         /\ mid_(NewtonDomain.Left return@pos):1234 = (NewtonDomain.Left return@pos)':1248
         /\ mid_(NewtonDomain.Left param2):1216 = (NewtonDomain.Left param2)':1249
         /\ mid_(NewtonDomain.Left param1):1208 = (NewtonDomain.Left param1)':1250
         /\ mid_(NewtonDomain.Left param0):1211 = (NewtonDomain.Left param0)':1251
         /\ mid_(NewtonDomain.Left return):1236 = (NewtonDomain.Left return)':1252
         /\ mid_(NewtonDomain.Left __cost):1215 = (NewtonDomain.Left __cost)':1253
         /\ 0 = K:1237 /\ (K:1207 + K:1237) = K:1254 /\ 0 <= K:1254
         /\ type_err:1255 = (NewtonDomain.Left param2@width)':1241
         /\ type_err:1256 = (NewtonDomain.Left param1@width)':1242
         /\ 80 = (NewtonDomain.Left param0@width)':1243
         /\ return@width:406 = (NewtonDomain.Left return@width)':1244
         /\ type_err:1257 = (NewtonDomain.Left param2@pos)':1245
         /\ type_err:1258 = (NewtonDomain.Left param1@pos)':1246
         /\ 0 = (NewtonDomain.Left param0@pos)':1247
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1248
         /\ 20 = (NewtonDomain.Left param2)':1249
         /\ 0 = (NewtonDomain.Left param1)':1250
         /\ alloc:27 = (NewtonDomain.Left param0)':1251
         /\ return:404 = (NewtonDomain.Left return)':1252
         /\ 0 = (NewtonDomain.Left __cost)':1253)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1150 + 1)
 return := havoc:1201
 param0 := fresh_param0:1158
 param1 := fresh_param1:1152
 param2 := fresh_param2:1151
 return@pos := type_err:1202
 param0@pos := fresh_param0@pos:1156
 param1@pos := fresh_param1@pos:1177
 param2@pos := fresh_param2@pos:1175
 return@width := type_err:1203
 param0@width := fresh_param0@width:1160
 param1@width := fresh_param1@width:1171
 param2@width := fresh_param2@width:1169
 when (0 <= fresh___cost:1150 /\ 0 <= (fresh___cost:1150 + 1)
         /\ (fresh_param2:1151 + -fresh_param1:1152) < 1
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param1):1154 = fresh_param1:1152)
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param0@pos):1155 = fresh_param0@pos:1156)
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param0):1157 = fresh_param0:1158)
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param0@width):1159 = fresh_param0@width:1160)
         /\ (!(0 <= K:1153)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1161)
                     + (8 * mid_(NewtonDomain.Left param2):1162)) <= (
                  ((7 * fresh___cost:1150) + (8 * fresh_param2:1151))
                    + (-6 * K:1153)))
         /\ (!(0 <= K:1153)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1161)
                     + (8 * mid_(NewtonDomain.Left param2):1162)) <= (
                  ((5 * fresh___cost:1150) + (8 * fresh_param2:1151))
                    + (5 * K:1153)))
         /\ (!(0 <= K:1153)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1161)
                     + (4 * mid_(NewtonDomain.Left param2):1162)) <= (
                  ((3 * fresh___cost:1150) + (4 * fresh_param2:1151))
                    + -K:1153))
         /\ (!(0 <= K:1153)
               \/ (-mid_(NewtonDomain.Left __cost):1161
                     + (-2 * mid_(NewtonDomain.Left param2):1162)) <= (
                  -fresh___cost:1150 + (-2 * fresh_param2:1151)))
         /\ ((K:1153 = 0
                /\ type_err:1163 = mid_(NewtonDomain.Right return@width):1164
                /\ type_err:1165 = mid_(NewtonDomain.Right return@pos):1166
                /\ havoc:1167 = mid_(NewtonDomain.Right return):1168
                /\ fresh_param2@width:1169 = mid_(NewtonDomain.Left param2@width):1170
                /\ fresh_param1@width:1171 = mid_(NewtonDomain.Left param1@width):1172
                /\ fresh_param0@width:1160 = mid_(NewtonDomain.Left param0@width):1159
                /\ fresh_return@width:1173 = mid_(NewtonDomain.Left return@width):1174
                /\ fresh_param2@pos:1175 = mid_(NewtonDomain.Left param2@pos):1176
                /\ fresh_param1@pos:1177 = mid_(NewtonDomain.Left param1@pos):1178
                /\ fresh_param0@pos:1156 = mid_(NewtonDomain.Left param0@pos):1155
                /\ fresh_return@pos:1179 = mid_(NewtonDomain.Left return@pos):1180
                /\ fresh_param2:1151 = mid_(NewtonDomain.Left param2):1162
                /\ fresh_param1:1152 = mid_(NewtonDomain.Left param1):1154
                /\ fresh_param0:1158 = mid_(NewtonDomain.Left param0):1157
                /\ fresh_return:1181 = mid_(NewtonDomain.Left return):1182
                /\ fresh___cost:1150 = mid_(NewtonDomain.Left __cost):1161)
               \/ (1 <= K:1153
                     /\ 0 <= (-fresh_param1:1152 + fresh_param2:1151)
                     /\ 0 <= (-2 + fresh___cost:1150)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1154
                                + mid_(NewtonDomain.Left param2):1162)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1161))
         /\ K:1183 = 0
         /\ mid_(NewtonDomain.Right return@width):1164 = (NewtonDomain.Right return@width)':1184
         /\ mid_(NewtonDomain.Right return@pos):1166 = (NewtonDomain.Right return@pos)':1185
         /\ mid_(NewtonDomain.Right return):1168 = (NewtonDomain.Right return)':1186
         /\ mid_(NewtonDomain.Left param2@width):1170 = (NewtonDomain.Left param2@width)':1187
         /\ mid_(NewtonDomain.Left param1@width):1172 = (NewtonDomain.Left param1@width)':1188
         /\ mid_(NewtonDomain.Left param0@width):1159 = (NewtonDomain.Left param0@width)':1189
         /\ mid_(NewtonDomain.Left return@width):1174 = (NewtonDomain.Left return@width)':1190
         /\ mid_(NewtonDomain.Left param2@pos):1176 = (NewtonDomain.Left param2@pos)':1191
         /\ mid_(NewtonDomain.Left param1@pos):1178 = (NewtonDomain.Left param1@pos)':1192
         /\ mid_(NewtonDomain.Left param0@pos):1155 = (NewtonDomain.Left param0@pos)':1193
         /\ mid_(NewtonDomain.Left return@pos):1180 = (NewtonDomain.Left return@pos)':1194
         /\ mid_(NewtonDomain.Left param2):1162 = (NewtonDomain.Left param2)':1195
         /\ mid_(NewtonDomain.Left param1):1154 = (NewtonDomain.Left param1)':1196
         /\ mid_(NewtonDomain.Left param0):1157 = (NewtonDomain.Left param0)':1197
         /\ mid_(NewtonDomain.Left return):1182 = (NewtonDomain.Left return)':1198
         /\ mid_(NewtonDomain.Left __cost):1161 = (NewtonDomain.Left __cost)':1199
         /\ 0 = K:1183 /\ (K:1153 + K:1183) = K:1200 /\ 0 <= K:1200
         /\ type_err:168 = (NewtonDomain.Left param2@width)':1187
         /\ type_err:167 = (NewtonDomain.Left param1@width)':1188
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1189
         /\ return@width:406 = (NewtonDomain.Left return@width)':1190
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':1191
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':1192
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1193
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1194
         /\ param1:160 = (NewtonDomain.Left param2)':1195
         /\ 0 = (NewtonDomain.Left param1)':1196
         /\ param0:157 = (NewtonDomain.Left param0)':1197
         /\ return:404 = (NewtonDomain.Left return)':1198
         /\ __cost:106 = (NewtonDomain.Left __cost)':1199)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1137 + 1)
 return := (NewtonDomain.Right return)':1122
 param0 := fresh_param0:1139
 param1 := fresh_param1:1140
 param2 := fresh_param2:1141
 return@pos := (NewtonDomain.Right return@pos)':1121
 param0@pos := fresh_param0@pos:1143
 param1@pos := fresh_param1@pos:1144
 param2@pos := fresh_param2@pos:1145
 return@width := (NewtonDomain.Right return@width)':1120
 param0@width := fresh_param0@width:1147
 param1@width := fresh_param1@width:1148
 param2@width := fresh_param2@width:1149
 when (0 <= fresh___cost:1137 /\ 0 <= (fresh___cost:1137 + 1)
         /\ (fresh_param2:1141 + -fresh_param1:1140) < 1
         /\ (!(0 <= K:1102)
               \/ mid_(NewtonDomain.Left param1):1103 = fresh_param1:1140)
         /\ (!(0 <= K:1102)
               \/ mid_(NewtonDomain.Left param0@pos):1104 = fresh_param0@pos:1143)
         /\ (!(0 <= K:1102)
               \/ mid_(NewtonDomain.Left param0):1105 = fresh_param0:1139)
         /\ (!(0 <= K:1102)
               \/ mid_(NewtonDomain.Left param0@width):1106 = fresh_param0@width:1147)
         /\ (!(0 <= K:1102)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1107)
                     + (8 * mid_(NewtonDomain.Left param2):1108)) <= (
                  ((7 * fresh___cost:1137) + (8 * fresh_param2:1141))
                    + (-6 * K:1102)))
         /\ (!(0 <= K:1102)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1107)
                     + (8 * mid_(NewtonDomain.Left param2):1108)) <= (
                  ((5 * fresh___cost:1137) + (8 * fresh_param2:1141))
                    + (5 * K:1102)))
         /\ (!(0 <= K:1102)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1107)
                     + (4 * mid_(NewtonDomain.Left param2):1108)) <= (
                  ((3 * fresh___cost:1137) + (4 * fresh_param2:1141))
                    + -K:1102))
         /\ (!(0 <= K:1102)
               \/ (-mid_(NewtonDomain.Left __cost):1107
                     + (-2 * mid_(NewtonDomain.Left param2):1108)) <= (
                  -fresh___cost:1137 + (-2 * fresh_param2:1141)))
         /\ ((K:1102 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):1109
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):1110
                /\ havoc:302 = mid_(NewtonDomain.Right return):1111
                /\ fresh_param2@width:1149 = mid_(NewtonDomain.Left param2@width):1112
                /\ fresh_param1@width:1148 = mid_(NewtonDomain.Left param1@width):1113
                /\ fresh_param0@width:1147 = mid_(NewtonDomain.Left param0@width):1106
                /\ fresh_return@width:1146 = mid_(NewtonDomain.Left return@width):1114
                /\ fresh_param2@pos:1145 = mid_(NewtonDomain.Left param2@pos):1115
                /\ fresh_param1@pos:1144 = mid_(NewtonDomain.Left param1@pos):1116
                /\ fresh_param0@pos:1143 = mid_(NewtonDomain.Left param0@pos):1104
                /\ fresh_return@pos:1142 = mid_(NewtonDomain.Left return@pos):1117
                /\ fresh_param2:1141 = mid_(NewtonDomain.Left param2):1108
                /\ fresh_param1:1140 = mid_(NewtonDomain.Left param1):1103
                /\ fresh_param0:1139 = mid_(NewtonDomain.Left param0):1105
                /\ fresh_return:1138 = mid_(NewtonDomain.Left return):1118
                /\ fresh___cost:1137 = mid_(NewtonDomain.Left __cost):1107)
               \/ (1 <= K:1102
                     /\ 0 <= (-fresh_param1:1140 + fresh_param2:1141)
                     /\ 0 <= (-2 + fresh___cost:1137)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1103
                                + mid_(NewtonDomain.Left param2):1108)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1107))
         /\ K:1119 = 0
         /\ mid_(NewtonDomain.Right return@width):1109 = (NewtonDomain.Right return@width)':1120
         /\ mid_(NewtonDomain.Right return@pos):1110 = (NewtonDomain.Right return@pos)':1121
         /\ mid_(NewtonDomain.Right return):1111 = (NewtonDomain.Right return)':1122
         /\ mid_(NewtonDomain.Left param2@width):1112 = (NewtonDomain.Left param2@width)':1123
         /\ mid_(NewtonDomain.Left param1@width):1113 = (NewtonDomain.Left param1@width)':1124
         /\ mid_(NewtonDomain.Left param0@width):1106 = (NewtonDomain.Left param0@width)':1125
         /\ mid_(NewtonDomain.Left return@width):1114 = (NewtonDomain.Left return@width)':1126
         /\ mid_(NewtonDomain.Left param2@pos):1115 = (NewtonDomain.Left param2@pos)':1127
         /\ mid_(NewtonDomain.Left param1@pos):1116 = (NewtonDomain.Left param1@pos)':1128
         /\ mid_(NewtonDomain.Left param0@pos):1104 = (NewtonDomain.Left param0@pos)':1129
         /\ mid_(NewtonDomain.Left return@pos):1117 = (NewtonDomain.Left return@pos)':1130
         /\ mid_(NewtonDomain.Left param2):1108 = (NewtonDomain.Left param2)':1131
         /\ mid_(NewtonDomain.Left param1):1103 = (NewtonDomain.Left param1)':1132
         /\ mid_(NewtonDomain.Left param0):1105 = (NewtonDomain.Left param0)':1133
         /\ mid_(NewtonDomain.Left return):1118 = (NewtonDomain.Left return)':1134
         /\ mid_(NewtonDomain.Left __cost):1107 = (NewtonDomain.Left __cost)':1135
         /\ 0 = K:1119 /\ (K:1102 + K:1119) = K:1136 /\ 0 <= K:1136
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':1123
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':1124
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1125
         /\ return@width:406 = (NewtonDomain.Left return@width)':1126
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':1127
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':1128
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1129
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1130
         /\ param2:213 = (NewtonDomain.Left param2)':1131
         /\ param1:160 = (NewtonDomain.Left param1)':1132
         /\ param0:157 = (NewtonDomain.Left param0)':1133
         /\ return:404 = (NewtonDomain.Left return)':1134
         /\ __cost:106 = (NewtonDomain.Left __cost)':1135)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 4:
Evaluating variable number 9 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:1319
 (NewtonDomain.Left return) := fresh_return:1324
 (NewtonDomain.Left param0) := fresh_param0:1325
 (NewtonDomain.Left param1) := fresh_param1:1326
 (NewtonDomain.Left param2) := fresh_param2:1327
 (NewtonDomain.Left return@pos) := fresh_return@pos:1329
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:1330
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:1331
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:1332
 (NewtonDomain.Left return@width) := fresh_return@width:1334
 (NewtonDomain.Left param0@width) := fresh_param0@width:1335
 (NewtonDomain.Left param1@width) := fresh_param1@width:1336
 (NewtonDomain.Left param2@width) := fresh_param2@width:1337
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:1319 /\ 0 <= (fresh___cost:1319 + 1)
         /\ 1 <= (fresh_param2:1327 + -fresh_param1:1326) /\ 0 < havoc:297
         /\ (fresh_param1:1326 + havoc:297) <= fresh_param2:1327
         /\ 0 <= fresh___cost:1264 /\ 0 <= (fresh___cost:1264 + 1)
         /\ (fresh_param2:1265 + -fresh_param1:1266) < 1
         /\ (!(0 <= K:1267)
               \/ mid_(NewtonDomain.Left param1):1268 = fresh_param1:1266)
         /\ (!(0 <= K:1267)
               \/ mid_(NewtonDomain.Left param0@pos):1269 = fresh_param0@pos:1270)
         /\ (!(0 <= K:1267)
               \/ mid_(NewtonDomain.Left param0):1271 = fresh_param0:1272)
         /\ (!(0 <= K:1267)
               \/ mid_(NewtonDomain.Left param0@width):1273 = fresh_param0@width:1274)
         /\ (!(0 <= K:1267)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1275)
                     + (8 * mid_(NewtonDomain.Left param2):1276)) <= (
                  ((7 * fresh___cost:1264) + (8 * fresh_param2:1265))
                    + (-6 * K:1267)))
         /\ (!(0 <= K:1267)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1275)
                     + (8 * mid_(NewtonDomain.Left param2):1276)) <= (
                  ((5 * fresh___cost:1264) + (8 * fresh_param2:1265))
                    + (5 * K:1267)))
         /\ (!(0 <= K:1267)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1275)
                     + (4 * mid_(NewtonDomain.Left param2):1276)) <= (
                  ((3 * fresh___cost:1264) + (4 * fresh_param2:1265))
                    + -K:1267))
         /\ (!(0 <= K:1267)
               \/ (-mid_(NewtonDomain.Left __cost):1275
                     + (-2 * mid_(NewtonDomain.Left param2):1276)) <= (
                  -fresh___cost:1264 + (-2 * fresh_param2:1265)))
         /\ ((K:1267 = 0
                /\ type_err:1277 = mid_(NewtonDomain.Right return@width):1278
                /\ type_err:1279 = mid_(NewtonDomain.Right return@pos):1280
                /\ havoc:1281 = mid_(NewtonDomain.Right return):1282
                /\ fresh_param2@width:1283 = mid_(NewtonDomain.Left param2@width):1284
                /\ fresh_param1@width:1285 = mid_(NewtonDomain.Left param1@width):1286
                /\ fresh_param0@width:1274 = mid_(NewtonDomain.Left param0@width):1273
                /\ fresh_return@width:1287 = mid_(NewtonDomain.Left return@width):1288
                /\ fresh_param2@pos:1289 = mid_(NewtonDomain.Left param2@pos):1290
                /\ fresh_param1@pos:1291 = mid_(NewtonDomain.Left param1@pos):1292
                /\ fresh_param0@pos:1270 = mid_(NewtonDomain.Left param0@pos):1269
                /\ fresh_return@pos:1293 = mid_(NewtonDomain.Left return@pos):1294
                /\ fresh_param2:1265 = mid_(NewtonDomain.Left param2):1276
                /\ fresh_param1:1266 = mid_(NewtonDomain.Left param1):1268
                /\ fresh_param0:1272 = mid_(NewtonDomain.Left param0):1271
                /\ fresh_return:1295 = mid_(NewtonDomain.Left return):1296
                /\ fresh___cost:1264 = mid_(NewtonDomain.Left __cost):1275)
               \/ (1 <= K:1267
                     /\ 0 <= (-fresh_param1:1266 + fresh_param2:1265)
                     /\ 0 <= (-2 + fresh___cost:1264)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1268
                                + mid_(NewtonDomain.Left param2):1276)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1275))
         /\ K:1297 = 0
         /\ mid_(NewtonDomain.Right return@width):1278 = (NewtonDomain.Right return@width)':1298
         /\ mid_(NewtonDomain.Right return@pos):1280 = (NewtonDomain.Right return@pos)':1299
         /\ mid_(NewtonDomain.Right return):1282 = (NewtonDomain.Right return)':1300
         /\ mid_(NewtonDomain.Left param2@width):1284 = (NewtonDomain.Left param2@width)':1301
         /\ mid_(NewtonDomain.Left param1@width):1286 = (NewtonDomain.Left param1@width)':1302
         /\ mid_(NewtonDomain.Left param0@width):1273 = (NewtonDomain.Left param0@width)':1303
         /\ mid_(NewtonDomain.Left return@width):1288 = (NewtonDomain.Left return@width)':1304
         /\ mid_(NewtonDomain.Left param2@pos):1290 = (NewtonDomain.Left param2@pos)':1305
         /\ mid_(NewtonDomain.Left param1@pos):1292 = (NewtonDomain.Left param1@pos)':1306
         /\ mid_(NewtonDomain.Left param0@pos):1269 = (NewtonDomain.Left param0@pos)':1307
         /\ mid_(NewtonDomain.Left return@pos):1294 = (NewtonDomain.Left return@pos)':1308
         /\ mid_(NewtonDomain.Left param2):1276 = (NewtonDomain.Left param2)':1309
         /\ mid_(NewtonDomain.Left param1):1268 = (NewtonDomain.Left param1)':1310
         /\ mid_(NewtonDomain.Left param0):1271 = (NewtonDomain.Left param0)':1311
         /\ mid_(NewtonDomain.Left return):1296 = (NewtonDomain.Left return)':1312
         /\ mid_(NewtonDomain.Left __cost):1275 = (NewtonDomain.Left __cost)':1313
         /\ 0 = K:1297 /\ (K:1267 + K:1297) = K:1314 /\ 0 <= K:1314
         /\ type_err:301 = (NewtonDomain.Left param2@width)':1301
         /\ type_err:300 = (NewtonDomain.Left param1@width)':1302
         /\ fresh_param0@width:1335 = (NewtonDomain.Left param0@width)':1303
         /\ fresh_return@width:1334 = (NewtonDomain.Left return@width)':1304
         /\ type_err:299 = (NewtonDomain.Left param2@pos)':1305
         /\ type_err:298 = (NewtonDomain.Left param1@pos)':1306
         /\ fresh_param0@pos:1330 = (NewtonDomain.Left param0@pos)':1307
         /\ fresh_return@pos:1329 = (NewtonDomain.Left return@pos)':1308
         /\ fresh_param2:1327 = (NewtonDomain.Left param2)':1309
         /\ (havoc:297 + fresh_param1:1326) = (NewtonDomain.Left param1)':1310
         /\ fresh_param0:1325 = (NewtonDomain.Left param0)':1311
         /\ fresh_return:1324 = (NewtonDomain.Left return)':1312
         /\ (fresh___cost:1319 + 1) = (NewtonDomain.Left __cost)':1313
         /\ (NewtonDomain.Left __cost):407 = (fresh___cost:1264 + 1)
         /\ (NewtonDomain.Right m2):1338 = ((havoc:297 + fresh_param1:1326)
                                              + -1)
         /\ (NewtonDomain.Right a):1339 = fresh_param0:1325
         /\ (NewtonDomain.Right lo):1340 = fresh_param1:1326
         /\ (NewtonDomain.Right hi):1341 = fresh_param2:1327
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':1300
         /\ (NewtonDomain.Left param0):413 = fresh_param0:1325
         /\ (NewtonDomain.Left param1):414 = fresh_param1:1326
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:1326)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):1342 = fresh_param0@pos:1330
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':1299
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:1330
         /\ (NewtonDomain.Left param1@pos):419 = type_err:1315
         /\ (NewtonDomain.Left param2@pos):420 = type_err:1316
         /\ (NewtonDomain.Right a@width):1343 = fresh_param0@width:1335
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':1298
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:1335
         /\ (NewtonDomain.Left param1@width):424 = type_err:1317
         /\ (NewtonDomain.Left param2@width):425 = type_err:1318)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           (((15 * (NewtonDomain.Left __cost)':438)
               + (16 * (NewtonDomain.Left param2)':442))) <= (1)*(((15
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    16
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + (-14)*1
           (((7 * (NewtonDomain.Left __cost)':438)
               + (8 * (NewtonDomain.Left param2)':442))) <= (1)*(((7
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    8
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + (-5)*1
           (((5 * (NewtonDomain.Left __cost)':438)
               + (7 * (NewtonDomain.Left param2)':442))) <= (1)*(((5
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    7
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + 3*1
           (((3 * (NewtonDomain.Left __cost)':438)
               + (4 * (NewtonDomain.Left param2)':442))) <= (1)*(((3
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    4
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + 0
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:1381)
            \/ mid_(NewtonDomain.Left param1):1395 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:1381)
                 \/ mid_(NewtonDomain.Left param0@pos):1392 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:1381)
                 \/ mid_(NewtonDomain.Left param0):1396 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:1381)
                 \/ mid_(NewtonDomain.Left param0@width):1388 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:1381)
                 \/ ((15 * mid_(NewtonDomain.Left __cost):1398)
                       + (16 * mid_(NewtonDomain.Left param2):1394)) <= (
                    ((15 * (NewtonDomain.Left __cost):407)
                       + (16 * (NewtonDomain.Left param2):415))
                      + (-14 * K:1381)))
           /\ (!(0 <= K:1381)
                 \/ ((7 * mid_(NewtonDomain.Left __cost):1398)
                       + (8 * mid_(NewtonDomain.Left param2):1394)) <= (
                    ((7 * (NewtonDomain.Left __cost):407)
                       + (8 * (NewtonDomain.Left param2):415))
                      + (-5 * K:1381)))
           /\ (!(0 <= K:1381)
                 \/ ((5 * mid_(NewtonDomain.Left __cost):1398)
                       + (7 * mid_(NewtonDomain.Left param2):1394)) <= (
                    ((5 * (NewtonDomain.Left __cost):407)
                       + (7 * (NewtonDomain.Left param2):415)) + (3 * K:1381)))
           /\ (!(0 <= K:1381)
                 \/ ((3 * mid_(NewtonDomain.Left __cost):1398)
                       + (4 * mid_(NewtonDomain.Left param2):1394)) <= (
                    (3 * (NewtonDomain.Left __cost):407)
                      + (4 * (NewtonDomain.Left param2):415)))
           /\ (!(0 <= K:1381)
                 \/ (-mid_(NewtonDomain.Left __cost):1398
                       + (-2 * mid_(NewtonDomain.Left param2):1394)) <= (
                    -(NewtonDomain.Left __cost):407
                      + (-2 * (NewtonDomain.Left param2):415)))
           /\ ((K:1381 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):1383
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):1384
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):1385
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):1386
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):1387
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):1388
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):1389
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):1390
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):1391
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):1392
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):1393
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):1394
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):1395
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):1396
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):1397
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):1398)
                 \/ (1 <= K:1381
                       /\ 0 <= (-(NewtonDomain.Left param1):414
                                  + (NewtonDomain.Left param2):415)
                       /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1395
                                  + mid_(NewtonDomain.Left param2):1394)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):1398))
           /\ K:1382 = 0
           /\ mid_(NewtonDomain.Right return@width):1383 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):1384 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):1385 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):1386 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):1387 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):1388 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):1389 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):1390 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):1391 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):1392 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):1393 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):1394 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):1395 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):1396 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):1397 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):1398 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:1382 /\ (K:1381 + K:1382) = K:1380 /\ 0 <= K:1380)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1501 + 1)
 return := 0
 param0 := fresh_param0:1509
 param1 := fresh_param1:1503
 param2 := fresh_param2:1502
 return@pos := type_err:1559
 param0@pos := fresh_param0@pos:1507
 param1@pos := fresh_param1@pos:1528
 param2@pos := fresh_param2@pos:1526
 return@width := type_err:1560
 param0@width := fresh_param0@width:1511
 param1@width := fresh_param1@width:1522
 param2@width := fresh_param2@width:1520
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:1501
         /\ 0 <= (fresh___cost:1501 + 1)
         /\ (fresh_param2:1502 + -fresh_param1:1503) < 1
         /\ (!(0 <= K:1504)
               \/ mid_(NewtonDomain.Left param1):1505 = fresh_param1:1503)
         /\ (!(0 <= K:1504)
               \/ mid_(NewtonDomain.Left param0@pos):1506 = fresh_param0@pos:1507)
         /\ (!(0 <= K:1504)
               \/ mid_(NewtonDomain.Left param0):1508 = fresh_param0:1509)
         /\ (!(0 <= K:1504)
               \/ mid_(NewtonDomain.Left param0@width):1510 = fresh_param0@width:1511)
         /\ (!(0 <= K:1504)
               \/ ((15 * mid_(NewtonDomain.Left __cost):1512)
                     + (16 * mid_(NewtonDomain.Left param2):1513)) <= (
                  ((15 * fresh___cost:1501) + (16 * fresh_param2:1502))
                    + (-14 * K:1504)))
         /\ (!(0 <= K:1504)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1512)
                     + (8 * mid_(NewtonDomain.Left param2):1513)) <= (
                  ((7 * fresh___cost:1501) + (8 * fresh_param2:1502))
                    + (-5 * K:1504)))
         /\ (!(0 <= K:1504)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1512)
                     + (7 * mid_(NewtonDomain.Left param2):1513)) <= (
                  ((5 * fresh___cost:1501) + (7 * fresh_param2:1502))
                    + (3 * K:1504)))
         /\ (!(0 <= K:1504)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1512)
                     + (4 * mid_(NewtonDomain.Left param2):1513)) <= (
                  (3 * fresh___cost:1501) + (4 * fresh_param2:1502)))
         /\ (!(0 <= K:1504)
               \/ (-mid_(NewtonDomain.Left __cost):1512
                     + (-2 * mid_(NewtonDomain.Left param2):1513)) <= (
                  -fresh___cost:1501 + (-2 * fresh_param2:1502)))
         /\ ((K:1504 = 0
                /\ type_err:1514 = mid_(NewtonDomain.Right return@width):1515
                /\ type_err:1516 = mid_(NewtonDomain.Right return@pos):1517
                /\ havoc:1518 = mid_(NewtonDomain.Right return):1519
                /\ fresh_param2@width:1520 = mid_(NewtonDomain.Left param2@width):1521
                /\ fresh_param1@width:1522 = mid_(NewtonDomain.Left param1@width):1523
                /\ fresh_param0@width:1511 = mid_(NewtonDomain.Left param0@width):1510
                /\ fresh_return@width:1524 = mid_(NewtonDomain.Left return@width):1525
                /\ fresh_param2@pos:1526 = mid_(NewtonDomain.Left param2@pos):1527
                /\ fresh_param1@pos:1528 = mid_(NewtonDomain.Left param1@pos):1529
                /\ fresh_param0@pos:1507 = mid_(NewtonDomain.Left param0@pos):1506
                /\ fresh_return@pos:1530 = mid_(NewtonDomain.Left return@pos):1531
                /\ fresh_param2:1502 = mid_(NewtonDomain.Left param2):1513
                /\ fresh_param1:1503 = mid_(NewtonDomain.Left param1):1505
                /\ fresh_param0:1509 = mid_(NewtonDomain.Left param0):1508
                /\ fresh_return:1532 = mid_(NewtonDomain.Left return):1533
                /\ fresh___cost:1501 = mid_(NewtonDomain.Left __cost):1512)
               \/ (1 <= K:1504
                     /\ 0 <= (-fresh_param1:1503 + fresh_param2:1502)
                     /\ 0 <= (-2 + fresh___cost:1501)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1505
                                + mid_(NewtonDomain.Left param2):1513)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1512))
         /\ K:1534 = 0
         /\ mid_(NewtonDomain.Right return@width):1515 = (NewtonDomain.Right return@width)':1535
         /\ mid_(NewtonDomain.Right return@pos):1517 = (NewtonDomain.Right return@pos)':1536
         /\ mid_(NewtonDomain.Right return):1519 = (NewtonDomain.Right return)':1537
         /\ mid_(NewtonDomain.Left param2@width):1521 = (NewtonDomain.Left param2@width)':1538
         /\ mid_(NewtonDomain.Left param1@width):1523 = (NewtonDomain.Left param1@width)':1539
         /\ mid_(NewtonDomain.Left param0@width):1510 = (NewtonDomain.Left param0@width)':1540
         /\ mid_(NewtonDomain.Left return@width):1525 = (NewtonDomain.Left return@width)':1541
         /\ mid_(NewtonDomain.Left param2@pos):1527 = (NewtonDomain.Left param2@pos)':1542
         /\ mid_(NewtonDomain.Left param1@pos):1529 = (NewtonDomain.Left param1@pos)':1543
         /\ mid_(NewtonDomain.Left param0@pos):1506 = (NewtonDomain.Left param0@pos)':1544
         /\ mid_(NewtonDomain.Left return@pos):1531 = (NewtonDomain.Left return@pos)':1545
         /\ mid_(NewtonDomain.Left param2):1513 = (NewtonDomain.Left param2)':1546
         /\ mid_(NewtonDomain.Left param1):1505 = (NewtonDomain.Left param1)':1547
         /\ mid_(NewtonDomain.Left param0):1508 = (NewtonDomain.Left param0)':1548
         /\ mid_(NewtonDomain.Left return):1533 = (NewtonDomain.Left return)':1549
         /\ mid_(NewtonDomain.Left __cost):1512 = (NewtonDomain.Left __cost)':1550
         /\ 0 = K:1534 /\ (K:1504 + K:1534) = K:1551 /\ 0 <= K:1551
         /\ type_err:1552 = (NewtonDomain.Left param2@width)':1538
         /\ type_err:1553 = (NewtonDomain.Left param1@width)':1539
         /\ 80 = (NewtonDomain.Left param0@width)':1540
         /\ return@width:406 = (NewtonDomain.Left return@width)':1541
         /\ type_err:1554 = (NewtonDomain.Left param2@pos)':1542
         /\ type_err:1555 = (NewtonDomain.Left param1@pos)':1543
         /\ 0 = (NewtonDomain.Left param0@pos)':1544
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1545
         /\ 20 = (NewtonDomain.Left param2)':1546
         /\ 0 = (NewtonDomain.Left param1)':1547
         /\ alloc:27 = (NewtonDomain.Left param0)':1548
         /\ return:404 = (NewtonDomain.Left return)':1549
         /\ 0 = (NewtonDomain.Left __cost)':1550)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1447 + 1)
 return := havoc:1498
 param0 := fresh_param0:1455
 param1 := fresh_param1:1449
 param2 := fresh_param2:1448
 return@pos := type_err:1499
 param0@pos := fresh_param0@pos:1453
 param1@pos := fresh_param1@pos:1474
 param2@pos := fresh_param2@pos:1472
 return@width := type_err:1500
 param0@width := fresh_param0@width:1457
 param1@width := fresh_param1@width:1468
 param2@width := fresh_param2@width:1466
 when (0 <= fresh___cost:1447 /\ 0 <= (fresh___cost:1447 + 1)
         /\ (fresh_param2:1448 + -fresh_param1:1449) < 1
         /\ (!(0 <= K:1450)
               \/ mid_(NewtonDomain.Left param1):1451 = fresh_param1:1449)
         /\ (!(0 <= K:1450)
               \/ mid_(NewtonDomain.Left param0@pos):1452 = fresh_param0@pos:1453)
         /\ (!(0 <= K:1450)
               \/ mid_(NewtonDomain.Left param0):1454 = fresh_param0:1455)
         /\ (!(0 <= K:1450)
               \/ mid_(NewtonDomain.Left param0@width):1456 = fresh_param0@width:1457)
         /\ (!(0 <= K:1450)
               \/ ((15 * mid_(NewtonDomain.Left __cost):1458)
                     + (16 * mid_(NewtonDomain.Left param2):1459)) <= (
                  ((15 * fresh___cost:1447) + (16 * fresh_param2:1448))
                    + (-14 * K:1450)))
         /\ (!(0 <= K:1450)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1458)
                     + (8 * mid_(NewtonDomain.Left param2):1459)) <= (
                  ((7 * fresh___cost:1447) + (8 * fresh_param2:1448))
                    + (-5 * K:1450)))
         /\ (!(0 <= K:1450)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1458)
                     + (7 * mid_(NewtonDomain.Left param2):1459)) <= (
                  ((5 * fresh___cost:1447) + (7 * fresh_param2:1448))
                    + (3 * K:1450)))
         /\ (!(0 <= K:1450)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1458)
                     + (4 * mid_(NewtonDomain.Left param2):1459)) <= (
                  (3 * fresh___cost:1447) + (4 * fresh_param2:1448)))
         /\ (!(0 <= K:1450)
               \/ (-mid_(NewtonDomain.Left __cost):1458
                     + (-2 * mid_(NewtonDomain.Left param2):1459)) <= (
                  -fresh___cost:1447 + (-2 * fresh_param2:1448)))
         /\ ((K:1450 = 0
                /\ type_err:1460 = mid_(NewtonDomain.Right return@width):1461
                /\ type_err:1462 = mid_(NewtonDomain.Right return@pos):1463
                /\ havoc:1464 = mid_(NewtonDomain.Right return):1465
                /\ fresh_param2@width:1466 = mid_(NewtonDomain.Left param2@width):1467
                /\ fresh_param1@width:1468 = mid_(NewtonDomain.Left param1@width):1469
                /\ fresh_param0@width:1457 = mid_(NewtonDomain.Left param0@width):1456
                /\ fresh_return@width:1470 = mid_(NewtonDomain.Left return@width):1471
                /\ fresh_param2@pos:1472 = mid_(NewtonDomain.Left param2@pos):1473
                /\ fresh_param1@pos:1474 = mid_(NewtonDomain.Left param1@pos):1475
                /\ fresh_param0@pos:1453 = mid_(NewtonDomain.Left param0@pos):1452
                /\ fresh_return@pos:1476 = mid_(NewtonDomain.Left return@pos):1477
                /\ fresh_param2:1448 = mid_(NewtonDomain.Left param2):1459
                /\ fresh_param1:1449 = mid_(NewtonDomain.Left param1):1451
                /\ fresh_param0:1455 = mid_(NewtonDomain.Left param0):1454
                /\ fresh_return:1478 = mid_(NewtonDomain.Left return):1479
                /\ fresh___cost:1447 = mid_(NewtonDomain.Left __cost):1458)
               \/ (1 <= K:1450
                     /\ 0 <= (-fresh_param1:1449 + fresh_param2:1448)
                     /\ 0 <= (-2 + fresh___cost:1447)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1451
                                + mid_(NewtonDomain.Left param2):1459)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1458))
         /\ K:1480 = 0
         /\ mid_(NewtonDomain.Right return@width):1461 = (NewtonDomain.Right return@width)':1481
         /\ mid_(NewtonDomain.Right return@pos):1463 = (NewtonDomain.Right return@pos)':1482
         /\ mid_(NewtonDomain.Right return):1465 = (NewtonDomain.Right return)':1483
         /\ mid_(NewtonDomain.Left param2@width):1467 = (NewtonDomain.Left param2@width)':1484
         /\ mid_(NewtonDomain.Left param1@width):1469 = (NewtonDomain.Left param1@width)':1485
         /\ mid_(NewtonDomain.Left param0@width):1456 = (NewtonDomain.Left param0@width)':1486
         /\ mid_(NewtonDomain.Left return@width):1471 = (NewtonDomain.Left return@width)':1487
         /\ mid_(NewtonDomain.Left param2@pos):1473 = (NewtonDomain.Left param2@pos)':1488
         /\ mid_(NewtonDomain.Left param1@pos):1475 = (NewtonDomain.Left param1@pos)':1489
         /\ mid_(NewtonDomain.Left param0@pos):1452 = (NewtonDomain.Left param0@pos)':1490
         /\ mid_(NewtonDomain.Left return@pos):1477 = (NewtonDomain.Left return@pos)':1491
         /\ mid_(NewtonDomain.Left param2):1459 = (NewtonDomain.Left param2)':1492
         /\ mid_(NewtonDomain.Left param1):1451 = (NewtonDomain.Left param1)':1493
         /\ mid_(NewtonDomain.Left param0):1454 = (NewtonDomain.Left param0)':1494
         /\ mid_(NewtonDomain.Left return):1479 = (NewtonDomain.Left return)':1495
         /\ mid_(NewtonDomain.Left __cost):1458 = (NewtonDomain.Left __cost)':1496
         /\ 0 = K:1480 /\ (K:1450 + K:1480) = K:1497 /\ 0 <= K:1497
         /\ type_err:168 = (NewtonDomain.Left param2@width)':1484
         /\ type_err:167 = (NewtonDomain.Left param1@width)':1485
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1486
         /\ return@width:406 = (NewtonDomain.Left return@width)':1487
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':1488
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':1489
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1490
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1491
         /\ param1:160 = (NewtonDomain.Left param2)':1492
         /\ 0 = (NewtonDomain.Left param1)':1493
         /\ param0:157 = (NewtonDomain.Left param0)':1494
         /\ return:404 = (NewtonDomain.Left return)':1495
         /\ __cost:106 = (NewtonDomain.Left __cost)':1496)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1434 + 1)
 return := (NewtonDomain.Right return)':1419
 param0 := fresh_param0:1436
 param1 := fresh_param1:1437
 param2 := fresh_param2:1438
 return@pos := (NewtonDomain.Right return@pos)':1418
 param0@pos := fresh_param0@pos:1440
 param1@pos := fresh_param1@pos:1441
 param2@pos := fresh_param2@pos:1442
 return@width := (NewtonDomain.Right return@width)':1417
 param0@width := fresh_param0@width:1444
 param1@width := fresh_param1@width:1445
 param2@width := fresh_param2@width:1446
 when (0 <= fresh___cost:1434 /\ 0 <= (fresh___cost:1434 + 1)
         /\ (fresh_param2:1438 + -fresh_param1:1437) < 1
         /\ (!(0 <= K:1399)
               \/ mid_(NewtonDomain.Left param1):1400 = fresh_param1:1437)
         /\ (!(0 <= K:1399)
               \/ mid_(NewtonDomain.Left param0@pos):1401 = fresh_param0@pos:1440)
         /\ (!(0 <= K:1399)
               \/ mid_(NewtonDomain.Left param0):1402 = fresh_param0:1436)
         /\ (!(0 <= K:1399)
               \/ mid_(NewtonDomain.Left param0@width):1403 = fresh_param0@width:1444)
         /\ (!(0 <= K:1399)
               \/ ((15 * mid_(NewtonDomain.Left __cost):1404)
                     + (16 * mid_(NewtonDomain.Left param2):1405)) <= (
                  ((15 * fresh___cost:1434) + (16 * fresh_param2:1438))
                    + (-14 * K:1399)))
         /\ (!(0 <= K:1399)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1404)
                     + (8 * mid_(NewtonDomain.Left param2):1405)) <= (
                  ((7 * fresh___cost:1434) + (8 * fresh_param2:1438))
                    + (-5 * K:1399)))
         /\ (!(0 <= K:1399)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1404)
                     + (7 * mid_(NewtonDomain.Left param2):1405)) <= (
                  ((5 * fresh___cost:1434) + (7 * fresh_param2:1438))
                    + (3 * K:1399)))
         /\ (!(0 <= K:1399)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1404)
                     + (4 * mid_(NewtonDomain.Left param2):1405)) <= (
                  (3 * fresh___cost:1434) + (4 * fresh_param2:1438)))
         /\ (!(0 <= K:1399)
               \/ (-mid_(NewtonDomain.Left __cost):1404
                     + (-2 * mid_(NewtonDomain.Left param2):1405)) <= (
                  -fresh___cost:1434 + (-2 * fresh_param2:1438)))
         /\ ((K:1399 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):1406
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):1407
                /\ havoc:302 = mid_(NewtonDomain.Right return):1408
                /\ fresh_param2@width:1446 = mid_(NewtonDomain.Left param2@width):1409
                /\ fresh_param1@width:1445 = mid_(NewtonDomain.Left param1@width):1410
                /\ fresh_param0@width:1444 = mid_(NewtonDomain.Left param0@width):1403
                /\ fresh_return@width:1443 = mid_(NewtonDomain.Left return@width):1411
                /\ fresh_param2@pos:1442 = mid_(NewtonDomain.Left param2@pos):1412
                /\ fresh_param1@pos:1441 = mid_(NewtonDomain.Left param1@pos):1413
                /\ fresh_param0@pos:1440 = mid_(NewtonDomain.Left param0@pos):1401
                /\ fresh_return@pos:1439 = mid_(NewtonDomain.Left return@pos):1414
                /\ fresh_param2:1438 = mid_(NewtonDomain.Left param2):1405
                /\ fresh_param1:1437 = mid_(NewtonDomain.Left param1):1400
                /\ fresh_param0:1436 = mid_(NewtonDomain.Left param0):1402
                /\ fresh_return:1435 = mid_(NewtonDomain.Left return):1415
                /\ fresh___cost:1434 = mid_(NewtonDomain.Left __cost):1404)
               \/ (1 <= K:1399
                     /\ 0 <= (-fresh_param1:1437 + fresh_param2:1438)
                     /\ 0 <= (-2 + fresh___cost:1434)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1400
                                + mid_(NewtonDomain.Left param2):1405)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1404))
         /\ K:1416 = 0
         /\ mid_(NewtonDomain.Right return@width):1406 = (NewtonDomain.Right return@width)':1417
         /\ mid_(NewtonDomain.Right return@pos):1407 = (NewtonDomain.Right return@pos)':1418
         /\ mid_(NewtonDomain.Right return):1408 = (NewtonDomain.Right return)':1419
         /\ mid_(NewtonDomain.Left param2@width):1409 = (NewtonDomain.Left param2@width)':1420
         /\ mid_(NewtonDomain.Left param1@width):1410 = (NewtonDomain.Left param1@width)':1421
         /\ mid_(NewtonDomain.Left param0@width):1403 = (NewtonDomain.Left param0@width)':1422
         /\ mid_(NewtonDomain.Left return@width):1411 = (NewtonDomain.Left return@width)':1423
         /\ mid_(NewtonDomain.Left param2@pos):1412 = (NewtonDomain.Left param2@pos)':1424
         /\ mid_(NewtonDomain.Left param1@pos):1413 = (NewtonDomain.Left param1@pos)':1425
         /\ mid_(NewtonDomain.Left param0@pos):1401 = (NewtonDomain.Left param0@pos)':1426
         /\ mid_(NewtonDomain.Left return@pos):1414 = (NewtonDomain.Left return@pos)':1427
         /\ mid_(NewtonDomain.Left param2):1405 = (NewtonDomain.Left param2)':1428
         /\ mid_(NewtonDomain.Left param1):1400 = (NewtonDomain.Left param1)':1429
         /\ mid_(NewtonDomain.Left param0):1402 = (NewtonDomain.Left param0)':1430
         /\ mid_(NewtonDomain.Left return):1415 = (NewtonDomain.Left return)':1431
         /\ mid_(NewtonDomain.Left __cost):1404 = (NewtonDomain.Left __cost)':1432
         /\ 0 = K:1416 /\ (K:1399 + K:1416) = K:1433 /\ 0 <= K:1433
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':1420
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':1421
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1422
         /\ return@width:406 = (NewtonDomain.Left return@width)':1423
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':1424
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':1425
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1426
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1427
         /\ param2:213 = (NewtonDomain.Left param2)':1428
         /\ param1:160 = (NewtonDomain.Left param1)':1429
         /\ param0:157 = (NewtonDomain.Left param0)':1430
         /\ return:404 = (NewtonDomain.Left return)':1431
         /\ __cost:106 = (NewtonDomain.Left __cost)':1432)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 5:
Widening will be applied on this round.
Evaluating variable number 9 (using IRE) 
(Performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:1616
 (NewtonDomain.Left return) := fresh_return:1621
 (NewtonDomain.Left param0) := fresh_param0:1622
 (NewtonDomain.Left param1) := fresh_param1:1623
 (NewtonDomain.Left param2) := fresh_param2:1624
 (NewtonDomain.Left return@pos) := fresh_return@pos:1626
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:1627
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:1628
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:1629
 (NewtonDomain.Left return@width) := fresh_return@width:1631
 (NewtonDomain.Left param0@width) := fresh_param0@width:1632
 (NewtonDomain.Left param1@width) := fresh_param1@width:1633
 (NewtonDomain.Left param2@width) := fresh_param2@width:1634
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:1616 /\ 0 <= (fresh___cost:1616 + 1)
         /\ 1 <= (fresh_param2:1624 + -fresh_param1:1623) /\ 0 < havoc:297
         /\ (fresh_param1:1623 + havoc:297) <= fresh_param2:1624
         /\ 0 <= fresh___cost:1561 /\ 0 <= (fresh___cost:1561 + 1)
         /\ (fresh_param2:1562 + -fresh_param1:1563) < 1
         /\ (!(0 <= K:1564)
               \/ mid_(NewtonDomain.Left param1):1565 = fresh_param1:1563)
         /\ (!(0 <= K:1564)
               \/ mid_(NewtonDomain.Left param0@pos):1566 = fresh_param0@pos:1567)
         /\ (!(0 <= K:1564)
               \/ mid_(NewtonDomain.Left param0):1568 = fresh_param0:1569)
         /\ (!(0 <= K:1564)
               \/ mid_(NewtonDomain.Left param0@width):1570 = fresh_param0@width:1571)
         /\ (!(0 <= K:1564)
               \/ ((15 * mid_(NewtonDomain.Left __cost):1572)
                     + (16 * mid_(NewtonDomain.Left param2):1573)) <= (
                  ((15 * fresh___cost:1561) + (16 * fresh_param2:1562))
                    + (-14 * K:1564)))
         /\ (!(0 <= K:1564)
               \/ ((7 * mid_(NewtonDomain.Left __cost):1572)
                     + (8 * mid_(NewtonDomain.Left param2):1573)) <= (
                  ((7 * fresh___cost:1561) + (8 * fresh_param2:1562))
                    + (-5 * K:1564)))
         /\ (!(0 <= K:1564)
               \/ ((5 * mid_(NewtonDomain.Left __cost):1572)
                     + (7 * mid_(NewtonDomain.Left param2):1573)) <= (
                  ((5 * fresh___cost:1561) + (7 * fresh_param2:1562))
                    + (3 * K:1564)))
         /\ (!(0 <= K:1564)
               \/ ((3 * mid_(NewtonDomain.Left __cost):1572)
                     + (4 * mid_(NewtonDomain.Left param2):1573)) <= (
                  (3 * fresh___cost:1561) + (4 * fresh_param2:1562)))
         /\ (!(0 <= K:1564)
               \/ (-mid_(NewtonDomain.Left __cost):1572
                     + (-2 * mid_(NewtonDomain.Left param2):1573)) <= (
                  -fresh___cost:1561 + (-2 * fresh_param2:1562)))
         /\ ((K:1564 = 0
                /\ type_err:1574 = mid_(NewtonDomain.Right return@width):1575
                /\ type_err:1576 = mid_(NewtonDomain.Right return@pos):1577
                /\ havoc:1578 = mid_(NewtonDomain.Right return):1579
                /\ fresh_param2@width:1580 = mid_(NewtonDomain.Left param2@width):1581
                /\ fresh_param1@width:1582 = mid_(NewtonDomain.Left param1@width):1583
                /\ fresh_param0@width:1571 = mid_(NewtonDomain.Left param0@width):1570
                /\ fresh_return@width:1584 = mid_(NewtonDomain.Left return@width):1585
                /\ fresh_param2@pos:1586 = mid_(NewtonDomain.Left param2@pos):1587
                /\ fresh_param1@pos:1588 = mid_(NewtonDomain.Left param1@pos):1589
                /\ fresh_param0@pos:1567 = mid_(NewtonDomain.Left param0@pos):1566
                /\ fresh_return@pos:1590 = mid_(NewtonDomain.Left return@pos):1591
                /\ fresh_param2:1562 = mid_(NewtonDomain.Left param2):1573
                /\ fresh_param1:1563 = mid_(NewtonDomain.Left param1):1565
                /\ fresh_param0:1569 = mid_(NewtonDomain.Left param0):1568
                /\ fresh_return:1592 = mid_(NewtonDomain.Left return):1593
                /\ fresh___cost:1561 = mid_(NewtonDomain.Left __cost):1572)
               \/ (1 <= K:1564
                     /\ 0 <= (-fresh_param1:1563 + fresh_param2:1562)
                     /\ 0 <= (-2 + fresh___cost:1561)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1565
                                + mid_(NewtonDomain.Left param2):1573)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1572))
         /\ K:1594 = 0
         /\ mid_(NewtonDomain.Right return@width):1575 = (NewtonDomain.Right return@width)':1595
         /\ mid_(NewtonDomain.Right return@pos):1577 = (NewtonDomain.Right return@pos)':1596
         /\ mid_(NewtonDomain.Right return):1579 = (NewtonDomain.Right return)':1597
         /\ mid_(NewtonDomain.Left param2@width):1581 = (NewtonDomain.Left param2@width)':1598
         /\ mid_(NewtonDomain.Left param1@width):1583 = (NewtonDomain.Left param1@width)':1599
         /\ mid_(NewtonDomain.Left param0@width):1570 = (NewtonDomain.Left param0@width)':1600
         /\ mid_(NewtonDomain.Left return@width):1585 = (NewtonDomain.Left return@width)':1601
         /\ mid_(NewtonDomain.Left param2@pos):1587 = (NewtonDomain.Left param2@pos)':1602
         /\ mid_(NewtonDomain.Left param1@pos):1589 = (NewtonDomain.Left param1@pos)':1603
         /\ mid_(NewtonDomain.Left param0@pos):1566 = (NewtonDomain.Left param0@pos)':1604
         /\ mid_(NewtonDomain.Left return@pos):1591 = (NewtonDomain.Left return@pos)':1605
         /\ mid_(NewtonDomain.Left param2):1573 = (NewtonDomain.Left param2)':1606
         /\ mid_(NewtonDomain.Left param1):1565 = (NewtonDomain.Left param1)':1607
         /\ mid_(NewtonDomain.Left param0):1568 = (NewtonDomain.Left param0)':1608
         /\ mid_(NewtonDomain.Left return):1593 = (NewtonDomain.Left return)':1609
         /\ mid_(NewtonDomain.Left __cost):1572 = (NewtonDomain.Left __cost)':1610
         /\ 0 = K:1594 /\ (K:1564 + K:1594) = K:1611 /\ 0 <= K:1611
         /\ type_err:301 = (NewtonDomain.Left param2@width)':1598
         /\ type_err:300 = (NewtonDomain.Left param1@width)':1599
         /\ fresh_param0@width:1632 = (NewtonDomain.Left param0@width)':1600
         /\ fresh_return@width:1631 = (NewtonDomain.Left return@width)':1601
         /\ type_err:299 = (NewtonDomain.Left param2@pos)':1602
         /\ type_err:298 = (NewtonDomain.Left param1@pos)':1603
         /\ fresh_param0@pos:1627 = (NewtonDomain.Left param0@pos)':1604
         /\ fresh_return@pos:1626 = (NewtonDomain.Left return@pos)':1605
         /\ fresh_param2:1624 = (NewtonDomain.Left param2)':1606
         /\ (havoc:297 + fresh_param1:1623) = (NewtonDomain.Left param1)':1607
         /\ fresh_param0:1622 = (NewtonDomain.Left param0)':1608
         /\ fresh_return:1621 = (NewtonDomain.Left return)':1609
         /\ (fresh___cost:1616 + 1) = (NewtonDomain.Left __cost)':1610
         /\ (NewtonDomain.Left __cost):407 = (fresh___cost:1561 + 1)
         /\ (NewtonDomain.Right m2):1635 = ((havoc:297 + fresh_param1:1623)
                                              + -1)
         /\ (NewtonDomain.Right a):1636 = fresh_param0:1622
         /\ (NewtonDomain.Right lo):1637 = fresh_param1:1623
         /\ (NewtonDomain.Right hi):1638 = fresh_param2:1624
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':1597
         /\ (NewtonDomain.Left param0):413 = fresh_param0:1622
         /\ (NewtonDomain.Left param1):414 = fresh_param1:1623
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:1623)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):1639 = fresh_param0@pos:1627
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':1596
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:1627
         /\ (NewtonDomain.Left param1@pos):419 = type_err:1612
         /\ (NewtonDomain.Left param2@pos):420 = type_err:1613
         /\ (NewtonDomain.Right a@width):1640 = fresh_param0@width:1632
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':1595
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:1632
         /\ (NewtonDomain.Left param1@width):424 = type_err:1614
         /\ (NewtonDomain.Left param2@width):425 = type_err:1615)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           (((31 * (NewtonDomain.Left __cost)':438)
               + (32 * (NewtonDomain.Left param2)':442))) <= (1)*(((31
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    32
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + (-30)*1
           (((15 * (NewtonDomain.Left __cost)':438)
               + (16 * (NewtonDomain.Left param2)':442))) <= (1)*(((15
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    16
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + (-13)*1
           (((7 * (NewtonDomain.Left __cost)':438)
               + (8 * (NewtonDomain.Left param2)':442))) <= (1)*(((7
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    8
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + (-4)*1
           (((3 * (NewtonDomain.Left __cost)':438)
               + (4 * (NewtonDomain.Left param2)':442))) <= (1)*(((3
                                                                    * (NewtonDomain.Left __cost):407)
                                                                    + (
                                                                    4
                                                                    * (NewtonDomain.Left param2):415)))
                                                             + 1
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** result of widening: 
  {<Split [true
            ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:1714)
            \/ mid_(NewtonDomain.Left param0):1729 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:1714)
                 \/ mid_(NewtonDomain.Left param0@pos):1725 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:1714)
                 \/ mid_(NewtonDomain.Left param1):1728 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:1714)
                 \/ mid_(NewtonDomain.Left param0@width):1721 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:1714)
                 \/ (-mid_(NewtonDomain.Left __cost):1731
                       + (-2 * mid_(NewtonDomain.Left param2):1727)) <= (
                    -(NewtonDomain.Left __cost):407
                      + (-2 * (NewtonDomain.Left param2):415)))
           /\ ((K:1714 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):1716
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):1717
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):1718
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):1719
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):1720
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):1721
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):1722
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):1723
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):1724
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):1725
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):1726
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):1727
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):1728
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):1729
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):1730
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):1731)
                 \/ (1 <= K:1714
                       /\ 0 <= (-(NewtonDomain.Left param1):414
                                  + (NewtonDomain.Left param2):415)
                       /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1728
                                  + mid_(NewtonDomain.Left param2):1727)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):1731))
           /\ K:1715 = 0
           /\ mid_(NewtonDomain.Right return@width):1716 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):1717 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):1718 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):1719 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):1720 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):1721 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):1722 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):1723 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):1724 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):1725 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):1726 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):1727 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):1728 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):1729 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):1730 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):1731 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:1715 /\ (K:1714 + K:1715) = K:1713 /\ 0 <= K:1713)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1834 + 1)
 return := 0
 param0 := fresh_param0:1839
 param1 := fresh_param1:1836
 param2 := fresh_param2:1835
 return@pos := type_err:1892
 param0@pos := fresh_param0@pos:1841
 param1@pos := fresh_param1@pos:1861
 param2@pos := fresh_param2@pos:1859
 return@width := type_err:1893
 param0@width := fresh_param0@width:1844
 param1@width := fresh_param1@width:1855
 param2@width := fresh_param2@width:1853
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:1834
         /\ 0 <= (fresh___cost:1834 + 1)
         /\ (fresh_param2:1835 + -fresh_param1:1836) < 1
         /\ (!(0 <= K:1837)
               \/ mid_(NewtonDomain.Left param0):1838 = fresh_param0:1839)
         /\ (!(0 <= K:1837)
               \/ mid_(NewtonDomain.Left param0@pos):1840 = fresh_param0@pos:1841)
         /\ (!(0 <= K:1837)
               \/ mid_(NewtonDomain.Left param1):1842 = fresh_param1:1836)
         /\ (!(0 <= K:1837)
               \/ mid_(NewtonDomain.Left param0@width):1843 = fresh_param0@width:1844)
         /\ (!(0 <= K:1837)
               \/ (-mid_(NewtonDomain.Left __cost):1845
                     + (-2 * mid_(NewtonDomain.Left param2):1846)) <= (
                  -fresh___cost:1834 + (-2 * fresh_param2:1835)))
         /\ ((K:1837 = 0
                /\ type_err:1847 = mid_(NewtonDomain.Right return@width):1848
                /\ type_err:1849 = mid_(NewtonDomain.Right return@pos):1850
                /\ havoc:1851 = mid_(NewtonDomain.Right return):1852
                /\ fresh_param2@width:1853 = mid_(NewtonDomain.Left param2@width):1854
                /\ fresh_param1@width:1855 = mid_(NewtonDomain.Left param1@width):1856
                /\ fresh_param0@width:1844 = mid_(NewtonDomain.Left param0@width):1843
                /\ fresh_return@width:1857 = mid_(NewtonDomain.Left return@width):1858
                /\ fresh_param2@pos:1859 = mid_(NewtonDomain.Left param2@pos):1860
                /\ fresh_param1@pos:1861 = mid_(NewtonDomain.Left param1@pos):1862
                /\ fresh_param0@pos:1841 = mid_(NewtonDomain.Left param0@pos):1840
                /\ fresh_return@pos:1863 = mid_(NewtonDomain.Left return@pos):1864
                /\ fresh_param2:1835 = mid_(NewtonDomain.Left param2):1846
                /\ fresh_param1:1836 = mid_(NewtonDomain.Left param1):1842
                /\ fresh_param0:1839 = mid_(NewtonDomain.Left param0):1838
                /\ fresh_return:1865 = mid_(NewtonDomain.Left return):1866
                /\ fresh___cost:1834 = mid_(NewtonDomain.Left __cost):1845)
               \/ (1 <= K:1837
                     /\ 0 <= (-fresh_param1:1836 + fresh_param2:1835)
                     /\ 0 <= (-2 + fresh___cost:1834)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1842
                                + mid_(NewtonDomain.Left param2):1846)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1845))
         /\ K:1867 = 0
         /\ mid_(NewtonDomain.Right return@width):1848 = (NewtonDomain.Right return@width)':1868
         /\ mid_(NewtonDomain.Right return@pos):1850 = (NewtonDomain.Right return@pos)':1869
         /\ mid_(NewtonDomain.Right return):1852 = (NewtonDomain.Right return)':1870
         /\ mid_(NewtonDomain.Left param2@width):1854 = (NewtonDomain.Left param2@width)':1871
         /\ mid_(NewtonDomain.Left param1@width):1856 = (NewtonDomain.Left param1@width)':1872
         /\ mid_(NewtonDomain.Left param0@width):1843 = (NewtonDomain.Left param0@width)':1873
         /\ mid_(NewtonDomain.Left return@width):1858 = (NewtonDomain.Left return@width)':1874
         /\ mid_(NewtonDomain.Left param2@pos):1860 = (NewtonDomain.Left param2@pos)':1875
         /\ mid_(NewtonDomain.Left param1@pos):1862 = (NewtonDomain.Left param1@pos)':1876
         /\ mid_(NewtonDomain.Left param0@pos):1840 = (NewtonDomain.Left param0@pos)':1877
         /\ mid_(NewtonDomain.Left return@pos):1864 = (NewtonDomain.Left return@pos)':1878
         /\ mid_(NewtonDomain.Left param2):1846 = (NewtonDomain.Left param2)':1879
         /\ mid_(NewtonDomain.Left param1):1842 = (NewtonDomain.Left param1)':1880
         /\ mid_(NewtonDomain.Left param0):1838 = (NewtonDomain.Left param0)':1881
         /\ mid_(NewtonDomain.Left return):1866 = (NewtonDomain.Left return)':1882
         /\ mid_(NewtonDomain.Left __cost):1845 = (NewtonDomain.Left __cost)':1883
         /\ 0 = K:1867 /\ (K:1837 + K:1867) = K:1884 /\ 0 <= K:1884
         /\ type_err:1885 = (NewtonDomain.Left param2@width)':1871
         /\ type_err:1886 = (NewtonDomain.Left param1@width)':1872
         /\ 80 = (NewtonDomain.Left param0@width)':1873
         /\ return@width:406 = (NewtonDomain.Left return@width)':1874
         /\ type_err:1887 = (NewtonDomain.Left param2@pos)':1875
         /\ type_err:1888 = (NewtonDomain.Left param1@pos)':1876
         /\ 0 = (NewtonDomain.Left param0@pos)':1877
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1878
         /\ 20 = (NewtonDomain.Left param2)':1879
         /\ 0 = (NewtonDomain.Left param1)':1880
         /\ alloc:27 = (NewtonDomain.Left param0)':1881
         /\ return:404 = (NewtonDomain.Left return)':1882
         /\ 0 = (NewtonDomain.Left __cost)':1883)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1780 + 1)
 return := havoc:1831
 param0 := fresh_param0:1785
 param1 := fresh_param1:1782
 param2 := fresh_param2:1781
 return@pos := type_err:1832
 param0@pos := fresh_param0@pos:1787
 param1@pos := fresh_param1@pos:1807
 param2@pos := fresh_param2@pos:1805
 return@width := type_err:1833
 param0@width := fresh_param0@width:1790
 param1@width := fresh_param1@width:1801
 param2@width := fresh_param2@width:1799
 when (0 <= fresh___cost:1780 /\ 0 <= (fresh___cost:1780 + 1)
         /\ (fresh_param2:1781 + -fresh_param1:1782) < 1
         /\ (!(0 <= K:1783)
               \/ mid_(NewtonDomain.Left param0):1784 = fresh_param0:1785)
         /\ (!(0 <= K:1783)
               \/ mid_(NewtonDomain.Left param0@pos):1786 = fresh_param0@pos:1787)
         /\ (!(0 <= K:1783)
               \/ mid_(NewtonDomain.Left param1):1788 = fresh_param1:1782)
         /\ (!(0 <= K:1783)
               \/ mid_(NewtonDomain.Left param0@width):1789 = fresh_param0@width:1790)
         /\ (!(0 <= K:1783)
               \/ (-mid_(NewtonDomain.Left __cost):1791
                     + (-2 * mid_(NewtonDomain.Left param2):1792)) <= (
                  -fresh___cost:1780 + (-2 * fresh_param2:1781)))
         /\ ((K:1783 = 0
                /\ type_err:1793 = mid_(NewtonDomain.Right return@width):1794
                /\ type_err:1795 = mid_(NewtonDomain.Right return@pos):1796
                /\ havoc:1797 = mid_(NewtonDomain.Right return):1798
                /\ fresh_param2@width:1799 = mid_(NewtonDomain.Left param2@width):1800
                /\ fresh_param1@width:1801 = mid_(NewtonDomain.Left param1@width):1802
                /\ fresh_param0@width:1790 = mid_(NewtonDomain.Left param0@width):1789
                /\ fresh_return@width:1803 = mid_(NewtonDomain.Left return@width):1804
                /\ fresh_param2@pos:1805 = mid_(NewtonDomain.Left param2@pos):1806
                /\ fresh_param1@pos:1807 = mid_(NewtonDomain.Left param1@pos):1808
                /\ fresh_param0@pos:1787 = mid_(NewtonDomain.Left param0@pos):1786
                /\ fresh_return@pos:1809 = mid_(NewtonDomain.Left return@pos):1810
                /\ fresh_param2:1781 = mid_(NewtonDomain.Left param2):1792
                /\ fresh_param1:1782 = mid_(NewtonDomain.Left param1):1788
                /\ fresh_param0:1785 = mid_(NewtonDomain.Left param0):1784
                /\ fresh_return:1811 = mid_(NewtonDomain.Left return):1812
                /\ fresh___cost:1780 = mid_(NewtonDomain.Left __cost):1791)
               \/ (1 <= K:1783
                     /\ 0 <= (-fresh_param1:1782 + fresh_param2:1781)
                     /\ 0 <= (-2 + fresh___cost:1780)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1788
                                + mid_(NewtonDomain.Left param2):1792)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1791))
         /\ K:1813 = 0
         /\ mid_(NewtonDomain.Right return@width):1794 = (NewtonDomain.Right return@width)':1814
         /\ mid_(NewtonDomain.Right return@pos):1796 = (NewtonDomain.Right return@pos)':1815
         /\ mid_(NewtonDomain.Right return):1798 = (NewtonDomain.Right return)':1816
         /\ mid_(NewtonDomain.Left param2@width):1800 = (NewtonDomain.Left param2@width)':1817
         /\ mid_(NewtonDomain.Left param1@width):1802 = (NewtonDomain.Left param1@width)':1818
         /\ mid_(NewtonDomain.Left param0@width):1789 = (NewtonDomain.Left param0@width)':1819
         /\ mid_(NewtonDomain.Left return@width):1804 = (NewtonDomain.Left return@width)':1820
         /\ mid_(NewtonDomain.Left param2@pos):1806 = (NewtonDomain.Left param2@pos)':1821
         /\ mid_(NewtonDomain.Left param1@pos):1808 = (NewtonDomain.Left param1@pos)':1822
         /\ mid_(NewtonDomain.Left param0@pos):1786 = (NewtonDomain.Left param0@pos)':1823
         /\ mid_(NewtonDomain.Left return@pos):1810 = (NewtonDomain.Left return@pos)':1824
         /\ mid_(NewtonDomain.Left param2):1792 = (NewtonDomain.Left param2)':1825
         /\ mid_(NewtonDomain.Left param1):1788 = (NewtonDomain.Left param1)':1826
         /\ mid_(NewtonDomain.Left param0):1784 = (NewtonDomain.Left param0)':1827
         /\ mid_(NewtonDomain.Left return):1812 = (NewtonDomain.Left return)':1828
         /\ mid_(NewtonDomain.Left __cost):1791 = (NewtonDomain.Left __cost)':1829
         /\ 0 = K:1813 /\ (K:1783 + K:1813) = K:1830 /\ 0 <= K:1830
         /\ type_err:168 = (NewtonDomain.Left param2@width)':1817
         /\ type_err:167 = (NewtonDomain.Left param1@width)':1818
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1819
         /\ return@width:406 = (NewtonDomain.Left return@width)':1820
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':1821
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':1822
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1823
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1824
         /\ param1:160 = (NewtonDomain.Left param2)':1825
         /\ 0 = (NewtonDomain.Left param1)':1826
         /\ param0:157 = (NewtonDomain.Left param0)':1827
         /\ return:404 = (NewtonDomain.Left return)':1828
         /\ __cost:106 = (NewtonDomain.Left __cost)':1829)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:1767 + 1)
 return := (NewtonDomain.Right return)':1752
 param0 := fresh_param0:1769
 param1 := fresh_param1:1770
 param2 := fresh_param2:1771
 return@pos := (NewtonDomain.Right return@pos)':1751
 param0@pos := fresh_param0@pos:1773
 param1@pos := fresh_param1@pos:1774
 param2@pos := fresh_param2@pos:1775
 return@width := (NewtonDomain.Right return@width)':1750
 param0@width := fresh_param0@width:1777
 param1@width := fresh_param1@width:1778
 param2@width := fresh_param2@width:1779
 when (0 <= fresh___cost:1767 /\ 0 <= (fresh___cost:1767 + 1)
         /\ (fresh_param2:1771 + -fresh_param1:1770) < 1
         /\ (!(0 <= K:1732)
               \/ mid_(NewtonDomain.Left param0):1733 = fresh_param0:1769)
         /\ (!(0 <= K:1732)
               \/ mid_(NewtonDomain.Left param0@pos):1734 = fresh_param0@pos:1773)
         /\ (!(0 <= K:1732)
               \/ mid_(NewtonDomain.Left param1):1735 = fresh_param1:1770)
         /\ (!(0 <= K:1732)
               \/ mid_(NewtonDomain.Left param0@width):1736 = fresh_param0@width:1777)
         /\ (!(0 <= K:1732)
               \/ (-mid_(NewtonDomain.Left __cost):1737
                     + (-2 * mid_(NewtonDomain.Left param2):1738)) <= (
                  -fresh___cost:1767 + (-2 * fresh_param2:1771)))
         /\ ((K:1732 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):1739
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):1740
                /\ havoc:302 = mid_(NewtonDomain.Right return):1741
                /\ fresh_param2@width:1779 = mid_(NewtonDomain.Left param2@width):1742
                /\ fresh_param1@width:1778 = mid_(NewtonDomain.Left param1@width):1743
                /\ fresh_param0@width:1777 = mid_(NewtonDomain.Left param0@width):1736
                /\ fresh_return@width:1776 = mid_(NewtonDomain.Left return@width):1744
                /\ fresh_param2@pos:1775 = mid_(NewtonDomain.Left param2@pos):1745
                /\ fresh_param1@pos:1774 = mid_(NewtonDomain.Left param1@pos):1746
                /\ fresh_param0@pos:1773 = mid_(NewtonDomain.Left param0@pos):1734
                /\ fresh_return@pos:1772 = mid_(NewtonDomain.Left return@pos):1747
                /\ fresh_param2:1771 = mid_(NewtonDomain.Left param2):1738
                /\ fresh_param1:1770 = mid_(NewtonDomain.Left param1):1735
                /\ fresh_param0:1769 = mid_(NewtonDomain.Left param0):1733
                /\ fresh_return:1768 = mid_(NewtonDomain.Left return):1748
                /\ fresh___cost:1767 = mid_(NewtonDomain.Left __cost):1737)
               \/ (1 <= K:1732
                     /\ 0 <= (-fresh_param1:1770 + fresh_param2:1771)
                     /\ 0 <= (-2 + fresh___cost:1767)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1735
                                + mid_(NewtonDomain.Left param2):1738)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1737))
         /\ K:1749 = 0
         /\ mid_(NewtonDomain.Right return@width):1739 = (NewtonDomain.Right return@width)':1750
         /\ mid_(NewtonDomain.Right return@pos):1740 = (NewtonDomain.Right return@pos)':1751
         /\ mid_(NewtonDomain.Right return):1741 = (NewtonDomain.Right return)':1752
         /\ mid_(NewtonDomain.Left param2@width):1742 = (NewtonDomain.Left param2@width)':1753
         /\ mid_(NewtonDomain.Left param1@width):1743 = (NewtonDomain.Left param1@width)':1754
         /\ mid_(NewtonDomain.Left param0@width):1736 = (NewtonDomain.Left param0@width)':1755
         /\ mid_(NewtonDomain.Left return@width):1744 = (NewtonDomain.Left return@width)':1756
         /\ mid_(NewtonDomain.Left param2@pos):1745 = (NewtonDomain.Left param2@pos)':1757
         /\ mid_(NewtonDomain.Left param1@pos):1746 = (NewtonDomain.Left param1@pos)':1758
         /\ mid_(NewtonDomain.Left param0@pos):1734 = (NewtonDomain.Left param0@pos)':1759
         /\ mid_(NewtonDomain.Left return@pos):1747 = (NewtonDomain.Left return@pos)':1760
         /\ mid_(NewtonDomain.Left param2):1738 = (NewtonDomain.Left param2)':1761
         /\ mid_(NewtonDomain.Left param1):1735 = (NewtonDomain.Left param1)':1762
         /\ mid_(NewtonDomain.Left param0):1733 = (NewtonDomain.Left param0)':1763
         /\ mid_(NewtonDomain.Left return):1748 = (NewtonDomain.Left return)':1764
         /\ mid_(NewtonDomain.Left __cost):1737 = (NewtonDomain.Left __cost)':1765
         /\ 0 = K:1749 /\ (K:1732 + K:1749) = K:1766 /\ 0 <= K:1766
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':1753
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':1754
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':1755
         /\ return@width:406 = (NewtonDomain.Left return@width)':1756
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':1757
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':1758
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1759
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':1760
         /\ param2:213 = (NewtonDomain.Left param2)':1761
         /\ param1:160 = (NewtonDomain.Left param1)':1762
         /\ param0:157 = (NewtonDomain.Left param0)':1763
         /\ return:404 = (NewtonDomain.Left return)':1764
         /\ __cost:106 = (NewtonDomain.Left __cost)':1765)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 6:
Widening will be applied on this round.
Evaluating variable number 9 (using IRE) 
(Performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:1949
 (NewtonDomain.Left return) := fresh_return:1954
 (NewtonDomain.Left param0) := fresh_param0:1955
 (NewtonDomain.Left param1) := fresh_param1:1956
 (NewtonDomain.Left param2) := fresh_param2:1957
 (NewtonDomain.Left return@pos) := fresh_return@pos:1959
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:1960
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:1961
 (NewtonDomain.Left param2@pos) := fresh_param2@pos:1962
 (NewtonDomain.Left return@width) := fresh_return@width:1964
 (NewtonDomain.Left param0@width) := fresh_param0@width:1965
 (NewtonDomain.Left param1@width) := fresh_param1@width:1966
 (NewtonDomain.Left param2@width) := fresh_param2@width:1967
 (NewtonDomain.Right return) := havoc:186
 (NewtonDomain.Right return@pos) := type_err:189
 (NewtonDomain.Right return@width) := type_err:190
 when (0 <= fresh___cost:1949 /\ 0 <= (fresh___cost:1949 + 1)
         /\ 1 <= (fresh_param2:1957 + -fresh_param1:1956) /\ 0 < havoc:297
         /\ (fresh_param1:1956 + havoc:297) <= fresh_param2:1957
         /\ 0 <= fresh___cost:1894 /\ 0 <= (fresh___cost:1894 + 1)
         /\ (fresh_param2:1895 + -fresh_param1:1896) < 1
         /\ (!(0 <= K:1897)
               \/ mid_(NewtonDomain.Left param0):1898 = fresh_param0:1899)
         /\ (!(0 <= K:1897)
               \/ mid_(NewtonDomain.Left param0@pos):1900 = fresh_param0@pos:1901)
         /\ (!(0 <= K:1897)
               \/ mid_(NewtonDomain.Left param1):1902 = fresh_param1:1896)
         /\ (!(0 <= K:1897)
               \/ mid_(NewtonDomain.Left param0@width):1903 = fresh_param0@width:1904)
         /\ (!(0 <= K:1897)
               \/ (-mid_(NewtonDomain.Left __cost):1905
                     + (-2 * mid_(NewtonDomain.Left param2):1906)) <= (
                  -fresh___cost:1894 + (-2 * fresh_param2:1895)))
         /\ ((K:1897 = 0
                /\ type_err:1907 = mid_(NewtonDomain.Right return@width):1908
                /\ type_err:1909 = mid_(NewtonDomain.Right return@pos):1910
                /\ havoc:1911 = mid_(NewtonDomain.Right return):1912
                /\ fresh_param2@width:1913 = mid_(NewtonDomain.Left param2@width):1914
                /\ fresh_param1@width:1915 = mid_(NewtonDomain.Left param1@width):1916
                /\ fresh_param0@width:1904 = mid_(NewtonDomain.Left param0@width):1903
                /\ fresh_return@width:1917 = mid_(NewtonDomain.Left return@width):1918
                /\ fresh_param2@pos:1919 = mid_(NewtonDomain.Left param2@pos):1920
                /\ fresh_param1@pos:1921 = mid_(NewtonDomain.Left param1@pos):1922
                /\ fresh_param0@pos:1901 = mid_(NewtonDomain.Left param0@pos):1900
                /\ fresh_return@pos:1923 = mid_(NewtonDomain.Left return@pos):1924
                /\ fresh_param2:1895 = mid_(NewtonDomain.Left param2):1906
                /\ fresh_param1:1896 = mid_(NewtonDomain.Left param1):1902
                /\ fresh_param0:1899 = mid_(NewtonDomain.Left param0):1898
                /\ fresh_return:1925 = mid_(NewtonDomain.Left return):1926
                /\ fresh___cost:1894 = mid_(NewtonDomain.Left __cost):1905)
               \/ (1 <= K:1897
                     /\ 0 <= (-fresh_param1:1896 + fresh_param2:1895)
                     /\ 0 <= (-2 + fresh___cost:1894)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1902
                                + mid_(NewtonDomain.Left param2):1906)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1905))
         /\ K:1927 = 0
         /\ mid_(NewtonDomain.Right return@width):1908 = (NewtonDomain.Right return@width)':1928
         /\ mid_(NewtonDomain.Right return@pos):1910 = (NewtonDomain.Right return@pos)':1929
         /\ mid_(NewtonDomain.Right return):1912 = (NewtonDomain.Right return)':1930
         /\ mid_(NewtonDomain.Left param2@width):1914 = (NewtonDomain.Left param2@width)':1931
         /\ mid_(NewtonDomain.Left param1@width):1916 = (NewtonDomain.Left param1@width)':1932
         /\ mid_(NewtonDomain.Left param0@width):1903 = (NewtonDomain.Left param0@width)':1933
         /\ mid_(NewtonDomain.Left return@width):1918 = (NewtonDomain.Left return@width)':1934
         /\ mid_(NewtonDomain.Left param2@pos):1920 = (NewtonDomain.Left param2@pos)':1935
         /\ mid_(NewtonDomain.Left param1@pos):1922 = (NewtonDomain.Left param1@pos)':1936
         /\ mid_(NewtonDomain.Left param0@pos):1900 = (NewtonDomain.Left param0@pos)':1937
         /\ mid_(NewtonDomain.Left return@pos):1924 = (NewtonDomain.Left return@pos)':1938
         /\ mid_(NewtonDomain.Left param2):1906 = (NewtonDomain.Left param2)':1939
         /\ mid_(NewtonDomain.Left param1):1902 = (NewtonDomain.Left param1)':1940
         /\ mid_(NewtonDomain.Left param0):1898 = (NewtonDomain.Left param0)':1941
         /\ mid_(NewtonDomain.Left return):1926 = (NewtonDomain.Left return)':1942
         /\ mid_(NewtonDomain.Left __cost):1905 = (NewtonDomain.Left __cost)':1943
         /\ 0 = K:1927 /\ (K:1897 + K:1927) = K:1944 /\ 0 <= K:1944
         /\ type_err:301 = (NewtonDomain.Left param2@width)':1931
         /\ type_err:300 = (NewtonDomain.Left param1@width)':1932
         /\ fresh_param0@width:1965 = (NewtonDomain.Left param0@width)':1933
         /\ fresh_return@width:1964 = (NewtonDomain.Left return@width)':1934
         /\ type_err:299 = (NewtonDomain.Left param2@pos)':1935
         /\ type_err:298 = (NewtonDomain.Left param1@pos)':1936
         /\ fresh_param0@pos:1960 = (NewtonDomain.Left param0@pos)':1937
         /\ fresh_return@pos:1959 = (NewtonDomain.Left return@pos)':1938
         /\ fresh_param2:1957 = (NewtonDomain.Left param2)':1939
         /\ (havoc:297 + fresh_param1:1956) = (NewtonDomain.Left param1)':1940
         /\ fresh_param0:1955 = (NewtonDomain.Left param0)':1941
         /\ fresh_return:1954 = (NewtonDomain.Left return)':1942
         /\ (fresh___cost:1949 + 1) = (NewtonDomain.Left __cost)':1943
         /\ (NewtonDomain.Left __cost):407 = (fresh___cost:1894 + 1)
         /\ (NewtonDomain.Right m2):1968 = ((havoc:297 + fresh_param1:1956)
                                              + -1)
         /\ (NewtonDomain.Right a):1969 = fresh_param0:1955
         /\ (NewtonDomain.Right lo):1970 = fresh_param1:1956
         /\ (NewtonDomain.Right hi):1971 = fresh_param2:1957
         /\ (NewtonDomain.Left return):412 = (NewtonDomain.Right return)':1930
         /\ (NewtonDomain.Left param0):413 = fresh_param0:1955
         /\ (NewtonDomain.Left param1):414 = fresh_param1:1956
         /\ (NewtonDomain.Left param2):415 = ((havoc:297 + fresh_param1:1956)
                                                + -1)
         /\ (NewtonDomain.Right a@pos):1972 = fresh_param0@pos:1960
         /\ (NewtonDomain.Left return@pos):417 = (NewtonDomain.Right return@pos)':1929
         /\ (NewtonDomain.Left param0@pos):418 = fresh_param0@pos:1960
         /\ (NewtonDomain.Left param1@pos):419 = type_err:1945
         /\ (NewtonDomain.Left param2@pos):420 = type_err:1946
         /\ (NewtonDomain.Right a@width):1973 = fresh_param0@width:1965
         /\ (NewtonDomain.Left return@width):422 = (NewtonDomain.Right return@width)':1928
         /\ (NewtonDomain.Left param0@width):423 = fresh_param0@width:1965
         /\ (NewtonDomain.Left param1@width):424 = type_err:1947
         /\ (NewtonDomain.Left param2@width):425 = type_err:1948)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           (-(NewtonDomain.Left param2)':442) <= (1)*(-(NewtonDomain.Left param2):415)
                                                  + (-1)*1
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** result of widening: 
  {<Split [true
            ((NewtonDomain.Left param1)':441) = (1)*((NewtonDomain.Left param1):414)
                                                 + 0
           ((NewtonDomain.Left param0@pos)':444) = (1)*((NewtonDomain.Left param0@pos):418)
                                                    + 0
           ((NewtonDomain.Left param0)':440) = (1)*((NewtonDomain.Left param0):413)
                                                + 0
           ((NewtonDomain.Left param0@width)':448) = (1)*((NewtonDomain.Left param0@width):423)
                                                      + 0
           ((-(NewtonDomain.Left __cost)':438
               + (-2 * (NewtonDomain.Left param2)':442))) <= (1)*((-(NewtonDomain.Left __cost):407
                                                                    + (
                                                                    -2
                                                                    * (NewtonDomain.Left param2):415)))
                                                              + 0
           }
          pre:
            [|-(NewtonDomain.Left param1):414+(NewtonDomain.Left param2):415>=0;
              (NewtonDomain.Left __cost):407-2>=0|]
          post:
            [|-(NewtonDomain.Left param1)':441
              +(NewtonDomain.Left param2)':442-1>=0;
              (NewtonDomain.Left __cost)':438>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':438
   (NewtonDomain.Left return) := (NewtonDomain.Left return)':439
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':440
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':441
   (NewtonDomain.Left param2) := (NewtonDomain.Left param2)':442
   (NewtonDomain.Left return@pos) := (NewtonDomain.Left return@pos)':443
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':444
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':445
   (NewtonDomain.Left param2@pos) := (NewtonDomain.Left param2@pos)':446
   (NewtonDomain.Left return@width) := (NewtonDomain.Left return@width)':447
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':448
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':449
   (NewtonDomain.Left param2@width) := (NewtonDomain.Left param2@width)':450
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':306
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':308
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':310
   when ((!(0 <= K:2047)
            \/ mid_(NewtonDomain.Left param1):2061 = (NewtonDomain.Left param1):414)
           /\ (!(0 <= K:2047)
                 \/ mid_(NewtonDomain.Left param0@pos):2058 = (NewtonDomain.Left param0@pos):418)
           /\ (!(0 <= K:2047)
                 \/ mid_(NewtonDomain.Left param0):2062 = (NewtonDomain.Left param0):413)
           /\ (!(0 <= K:2047)
                 \/ mid_(NewtonDomain.Left param0@width):2054 = (NewtonDomain.Left param0@width):423)
           /\ (!(0 <= K:2047)
                 \/ (-mid_(NewtonDomain.Left __cost):2064
                       + (-2 * mid_(NewtonDomain.Left param2):2060)) <= (
                    -(NewtonDomain.Left __cost):407
                      + (-2 * (NewtonDomain.Left param2):415)))
           /\ ((K:2047 = 0
                  /\ (NewtonDomain.Right return@width):309 = mid_(NewtonDomain.Right return@width):2049
                  /\ (NewtonDomain.Right return@pos):307 = mid_(NewtonDomain.Right return@pos):2050
                  /\ (NewtonDomain.Right return):305 = mid_(NewtonDomain.Right return):2051
                  /\ (NewtonDomain.Left param2@width):425 = mid_(NewtonDomain.Left param2@width):2052
                  /\ (NewtonDomain.Left param1@width):424 = mid_(NewtonDomain.Left param1@width):2053
                  /\ (NewtonDomain.Left param0@width):423 = mid_(NewtonDomain.Left param0@width):2054
                  /\ (NewtonDomain.Left return@width):422 = mid_(NewtonDomain.Left return@width):2055
                  /\ (NewtonDomain.Left param2@pos):420 = mid_(NewtonDomain.Left param2@pos):2056
                  /\ (NewtonDomain.Left param1@pos):419 = mid_(NewtonDomain.Left param1@pos):2057
                  /\ (NewtonDomain.Left param0@pos):418 = mid_(NewtonDomain.Left param0@pos):2058
                  /\ (NewtonDomain.Left return@pos):417 = mid_(NewtonDomain.Left return@pos):2059
                  /\ (NewtonDomain.Left param2):415 = mid_(NewtonDomain.Left param2):2060
                  /\ (NewtonDomain.Left param1):414 = mid_(NewtonDomain.Left param1):2061
                  /\ (NewtonDomain.Left param0):413 = mid_(NewtonDomain.Left param0):2062
                  /\ (NewtonDomain.Left return):412 = mid_(NewtonDomain.Left return):2063
                  /\ (NewtonDomain.Left __cost):407 = mid_(NewtonDomain.Left __cost):2064)
                 \/ (1 <= K:2047
                       /\ 0 <= (-(NewtonDomain.Left param1):414
                                  + (NewtonDomain.Left param2):415)
                       /\ 0 <= (-2 + (NewtonDomain.Left __cost):407)
                       /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2061
                                  + mid_(NewtonDomain.Left param2):2060)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):2064))
           /\ K:2048 = 0
           /\ mid_(NewtonDomain.Right return@width):2049 = (NewtonDomain.Right return@width)':310
           /\ mid_(NewtonDomain.Right return@pos):2050 = (NewtonDomain.Right return@pos)':308
           /\ mid_(NewtonDomain.Right return):2051 = (NewtonDomain.Right return)':306
           /\ mid_(NewtonDomain.Left param2@width):2052 = (NewtonDomain.Left param2@width)':450
           /\ mid_(NewtonDomain.Left param1@width):2053 = (NewtonDomain.Left param1@width)':449
           /\ mid_(NewtonDomain.Left param0@width):2054 = (NewtonDomain.Left param0@width)':448
           /\ mid_(NewtonDomain.Left return@width):2055 = (NewtonDomain.Left return@width)':447
           /\ mid_(NewtonDomain.Left param2@pos):2056 = (NewtonDomain.Left param2@pos)':446
           /\ mid_(NewtonDomain.Left param1@pos):2057 = (NewtonDomain.Left param1@pos)':445
           /\ mid_(NewtonDomain.Left param0@pos):2058 = (NewtonDomain.Left param0@pos)':444
           /\ mid_(NewtonDomain.Left return@pos):2059 = (NewtonDomain.Left return@pos)':443
           /\ mid_(NewtonDomain.Left param2):2060 = (NewtonDomain.Left param2)':442
           /\ mid_(NewtonDomain.Left param1):2061 = (NewtonDomain.Left param1)':441
           /\ mid_(NewtonDomain.Left param0):2062 = (NewtonDomain.Left param0)':440
           /\ mid_(NewtonDomain.Left return):2063 = (NewtonDomain.Left return)':439
           /\ mid_(NewtonDomain.Left __cost):2064 = (NewtonDomain.Left __cost)':438
           /\ 0 = K:2048 /\ (K:2047 + K:2048) = K:2046 /\ 0 <= K:2046)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:2167 + 1)
 return := 0
 param0 := fresh_param0:2175
 param1 := fresh_param1:2169
 param2 := fresh_param2:2168
 return@pos := type_err:2225
 param0@pos := fresh_param0@pos:2173
 param1@pos := fresh_param1@pos:2194
 param2@pos := fresh_param2@pos:2192
 return@width := type_err:2226
 param0@width := fresh_param0@width:2177
 param1@width := fresh_param1@width:2188
 param2@width := fresh_param2@width:2186
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:2167
         /\ 0 <= (fresh___cost:2167 + 1)
         /\ (fresh_param2:2168 + -fresh_param1:2169) < 1
         /\ (!(0 <= K:2170)
               \/ mid_(NewtonDomain.Left param1):2171 = fresh_param1:2169)
         /\ (!(0 <= K:2170)
               \/ mid_(NewtonDomain.Left param0@pos):2172 = fresh_param0@pos:2173)
         /\ (!(0 <= K:2170)
               \/ mid_(NewtonDomain.Left param0):2174 = fresh_param0:2175)
         /\ (!(0 <= K:2170)
               \/ mid_(NewtonDomain.Left param0@width):2176 = fresh_param0@width:2177)
         /\ (!(0 <= K:2170)
               \/ (-mid_(NewtonDomain.Left __cost):2178
                     + (-2 * mid_(NewtonDomain.Left param2):2179)) <= (
                  -fresh___cost:2167 + (-2 * fresh_param2:2168)))
         /\ ((K:2170 = 0
                /\ type_err:2180 = mid_(NewtonDomain.Right return@width):2181
                /\ type_err:2182 = mid_(NewtonDomain.Right return@pos):2183
                /\ havoc:2184 = mid_(NewtonDomain.Right return):2185
                /\ fresh_param2@width:2186 = mid_(NewtonDomain.Left param2@width):2187
                /\ fresh_param1@width:2188 = mid_(NewtonDomain.Left param1@width):2189
                /\ fresh_param0@width:2177 = mid_(NewtonDomain.Left param0@width):2176
                /\ fresh_return@width:2190 = mid_(NewtonDomain.Left return@width):2191
                /\ fresh_param2@pos:2192 = mid_(NewtonDomain.Left param2@pos):2193
                /\ fresh_param1@pos:2194 = mid_(NewtonDomain.Left param1@pos):2195
                /\ fresh_param0@pos:2173 = mid_(NewtonDomain.Left param0@pos):2172
                /\ fresh_return@pos:2196 = mid_(NewtonDomain.Left return@pos):2197
                /\ fresh_param2:2168 = mid_(NewtonDomain.Left param2):2179
                /\ fresh_param1:2169 = mid_(NewtonDomain.Left param1):2171
                /\ fresh_param0:2175 = mid_(NewtonDomain.Left param0):2174
                /\ fresh_return:2198 = mid_(NewtonDomain.Left return):2199
                /\ fresh___cost:2167 = mid_(NewtonDomain.Left __cost):2178)
               \/ (1 <= K:2170
                     /\ 0 <= (-fresh_param1:2169 + fresh_param2:2168)
                     /\ 0 <= (-2 + fresh___cost:2167)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2171
                                + mid_(NewtonDomain.Left param2):2179)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):2178))
         /\ K:2200 = 0
         /\ mid_(NewtonDomain.Right return@width):2181 = (NewtonDomain.Right return@width)':2201
         /\ mid_(NewtonDomain.Right return@pos):2183 = (NewtonDomain.Right return@pos)':2202
         /\ mid_(NewtonDomain.Right return):2185 = (NewtonDomain.Right return)':2203
         /\ mid_(NewtonDomain.Left param2@width):2187 = (NewtonDomain.Left param2@width)':2204
         /\ mid_(NewtonDomain.Left param1@width):2189 = (NewtonDomain.Left param1@width)':2205
         /\ mid_(NewtonDomain.Left param0@width):2176 = (NewtonDomain.Left param0@width)':2206
         /\ mid_(NewtonDomain.Left return@width):2191 = (NewtonDomain.Left return@width)':2207
         /\ mid_(NewtonDomain.Left param2@pos):2193 = (NewtonDomain.Left param2@pos)':2208
         /\ mid_(NewtonDomain.Left param1@pos):2195 = (NewtonDomain.Left param1@pos)':2209
         /\ mid_(NewtonDomain.Left param0@pos):2172 = (NewtonDomain.Left param0@pos)':2210
         /\ mid_(NewtonDomain.Left return@pos):2197 = (NewtonDomain.Left return@pos)':2211
         /\ mid_(NewtonDomain.Left param2):2179 = (NewtonDomain.Left param2)':2212
         /\ mid_(NewtonDomain.Left param1):2171 = (NewtonDomain.Left param1)':2213
         /\ mid_(NewtonDomain.Left param0):2174 = (NewtonDomain.Left param0)':2214
         /\ mid_(NewtonDomain.Left return):2199 = (NewtonDomain.Left return)':2215
         /\ mid_(NewtonDomain.Left __cost):2178 = (NewtonDomain.Left __cost)':2216
         /\ 0 = K:2200 /\ (K:2170 + K:2200) = K:2217 /\ 0 <= K:2217
         /\ type_err:2218 = (NewtonDomain.Left param2@width)':2204
         /\ type_err:2219 = (NewtonDomain.Left param1@width)':2205
         /\ 80 = (NewtonDomain.Left param0@width)':2206
         /\ return@width:406 = (NewtonDomain.Left return@width)':2207
         /\ type_err:2220 = (NewtonDomain.Left param2@pos)':2208
         /\ type_err:2221 = (NewtonDomain.Left param1@pos)':2209
         /\ 0 = (NewtonDomain.Left param0@pos)':2210
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':2211
         /\ 20 = (NewtonDomain.Left param2)':2212
         /\ 0 = (NewtonDomain.Left param1)':2213
         /\ alloc:27 = (NewtonDomain.Left param0)':2214
         /\ return:404 = (NewtonDomain.Left return)':2215
         /\ 0 = (NewtonDomain.Left __cost)':2216)}

Evaluating variable number 16 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:2113 + 1)
 return := havoc:2164
 param0 := fresh_param0:2121
 param1 := fresh_param1:2115
 param2 := fresh_param2:2114
 return@pos := type_err:2165
 param0@pos := fresh_param0@pos:2119
 param1@pos := fresh_param1@pos:2140
 param2@pos := fresh_param2@pos:2138
 return@width := type_err:2166
 param0@width := fresh_param0@width:2123
 param1@width := fresh_param1@width:2134
 param2@width := fresh_param2@width:2132
 when (0 <= fresh___cost:2113 /\ 0 <= (fresh___cost:2113 + 1)
         /\ (fresh_param2:2114 + -fresh_param1:2115) < 1
         /\ (!(0 <= K:2116)
               \/ mid_(NewtonDomain.Left param1):2117 = fresh_param1:2115)
         /\ (!(0 <= K:2116)
               \/ mid_(NewtonDomain.Left param0@pos):2118 = fresh_param0@pos:2119)
         /\ (!(0 <= K:2116)
               \/ mid_(NewtonDomain.Left param0):2120 = fresh_param0:2121)
         /\ (!(0 <= K:2116)
               \/ mid_(NewtonDomain.Left param0@width):2122 = fresh_param0@width:2123)
         /\ (!(0 <= K:2116)
               \/ (-mid_(NewtonDomain.Left __cost):2124
                     + (-2 * mid_(NewtonDomain.Left param2):2125)) <= (
                  -fresh___cost:2113 + (-2 * fresh_param2:2114)))
         /\ ((K:2116 = 0
                /\ type_err:2126 = mid_(NewtonDomain.Right return@width):2127
                /\ type_err:2128 = mid_(NewtonDomain.Right return@pos):2129
                /\ havoc:2130 = mid_(NewtonDomain.Right return):2131
                /\ fresh_param2@width:2132 = mid_(NewtonDomain.Left param2@width):2133
                /\ fresh_param1@width:2134 = mid_(NewtonDomain.Left param1@width):2135
                /\ fresh_param0@width:2123 = mid_(NewtonDomain.Left param0@width):2122
                /\ fresh_return@width:2136 = mid_(NewtonDomain.Left return@width):2137
                /\ fresh_param2@pos:2138 = mid_(NewtonDomain.Left param2@pos):2139
                /\ fresh_param1@pos:2140 = mid_(NewtonDomain.Left param1@pos):2141
                /\ fresh_param0@pos:2119 = mid_(NewtonDomain.Left param0@pos):2118
                /\ fresh_return@pos:2142 = mid_(NewtonDomain.Left return@pos):2143
                /\ fresh_param2:2114 = mid_(NewtonDomain.Left param2):2125
                /\ fresh_param1:2115 = mid_(NewtonDomain.Left param1):2117
                /\ fresh_param0:2121 = mid_(NewtonDomain.Left param0):2120
                /\ fresh_return:2144 = mid_(NewtonDomain.Left return):2145
                /\ fresh___cost:2113 = mid_(NewtonDomain.Left __cost):2124)
               \/ (1 <= K:2116
                     /\ 0 <= (-fresh_param1:2115 + fresh_param2:2114)
                     /\ 0 <= (-2 + fresh___cost:2113)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2117
                                + mid_(NewtonDomain.Left param2):2125)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):2124))
         /\ K:2146 = 0
         /\ mid_(NewtonDomain.Right return@width):2127 = (NewtonDomain.Right return@width)':2147
         /\ mid_(NewtonDomain.Right return@pos):2129 = (NewtonDomain.Right return@pos)':2148
         /\ mid_(NewtonDomain.Right return):2131 = (NewtonDomain.Right return)':2149
         /\ mid_(NewtonDomain.Left param2@width):2133 = (NewtonDomain.Left param2@width)':2150
         /\ mid_(NewtonDomain.Left param1@width):2135 = (NewtonDomain.Left param1@width)':2151
         /\ mid_(NewtonDomain.Left param0@width):2122 = (NewtonDomain.Left param0@width)':2152
         /\ mid_(NewtonDomain.Left return@width):2137 = (NewtonDomain.Left return@width)':2153
         /\ mid_(NewtonDomain.Left param2@pos):2139 = (NewtonDomain.Left param2@pos)':2154
         /\ mid_(NewtonDomain.Left param1@pos):2141 = (NewtonDomain.Left param1@pos)':2155
         /\ mid_(NewtonDomain.Left param0@pos):2118 = (NewtonDomain.Left param0@pos)':2156
         /\ mid_(NewtonDomain.Left return@pos):2143 = (NewtonDomain.Left return@pos)':2157
         /\ mid_(NewtonDomain.Left param2):2125 = (NewtonDomain.Left param2)':2158
         /\ mid_(NewtonDomain.Left param1):2117 = (NewtonDomain.Left param1)':2159
         /\ mid_(NewtonDomain.Left param0):2120 = (NewtonDomain.Left param0)':2160
         /\ mid_(NewtonDomain.Left return):2145 = (NewtonDomain.Left return)':2161
         /\ mid_(NewtonDomain.Left __cost):2124 = (NewtonDomain.Left __cost)':2162
         /\ 0 = K:2146 /\ (K:2116 + K:2146) = K:2163 /\ 0 <= K:2163
         /\ type_err:168 = (NewtonDomain.Left param2@width)':2150
         /\ type_err:167 = (NewtonDomain.Left param1@width)':2151
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':2152
         /\ return@width:406 = (NewtonDomain.Left return@width)':2153
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':2154
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':2155
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':2156
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':2157
         /\ param1:160 = (NewtonDomain.Left param2)':2158
         /\ 0 = (NewtonDomain.Left param1)':2159
         /\ param0:157 = (NewtonDomain.Left param0)':2160
         /\ return:404 = (NewtonDomain.Left return)':2161
         /\ __cost:106 = (NewtonDomain.Left __cost)':2162)}

Evaluating variable number 23 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:2100 + 1)
 return := (NewtonDomain.Right return)':2085
 param0 := fresh_param0:2102
 param1 := fresh_param1:2103
 param2 := fresh_param2:2104
 return@pos := (NewtonDomain.Right return@pos)':2084
 param0@pos := fresh_param0@pos:2106
 param1@pos := fresh_param1@pos:2107
 param2@pos := fresh_param2@pos:2108
 return@width := (NewtonDomain.Right return@width)':2083
 param0@width := fresh_param0@width:2110
 param1@width := fresh_param1@width:2111
 param2@width := fresh_param2@width:2112
 when (0 <= fresh___cost:2100 /\ 0 <= (fresh___cost:2100 + 1)
         /\ (fresh_param2:2104 + -fresh_param1:2103) < 1
         /\ (!(0 <= K:2065)
               \/ mid_(NewtonDomain.Left param1):2066 = fresh_param1:2103)
         /\ (!(0 <= K:2065)
               \/ mid_(NewtonDomain.Left param0@pos):2067 = fresh_param0@pos:2106)
         /\ (!(0 <= K:2065)
               \/ mid_(NewtonDomain.Left param0):2068 = fresh_param0:2102)
         /\ (!(0 <= K:2065)
               \/ mid_(NewtonDomain.Left param0@width):2069 = fresh_param0@width:2110)
         /\ (!(0 <= K:2065)
               \/ (-mid_(NewtonDomain.Left __cost):2070
                     + (-2 * mid_(NewtonDomain.Left param2):2071)) <= (
                  -fresh___cost:2100 + (-2 * fresh_param2:2104)))
         /\ ((K:2065 = 0
                /\ type_err:304 = mid_(NewtonDomain.Right return@width):2072
                /\ type_err:303 = mid_(NewtonDomain.Right return@pos):2073
                /\ havoc:302 = mid_(NewtonDomain.Right return):2074
                /\ fresh_param2@width:2112 = mid_(NewtonDomain.Left param2@width):2075
                /\ fresh_param1@width:2111 = mid_(NewtonDomain.Left param1@width):2076
                /\ fresh_param0@width:2110 = mid_(NewtonDomain.Left param0@width):2069
                /\ fresh_return@width:2109 = mid_(NewtonDomain.Left return@width):2077
                /\ fresh_param2@pos:2108 = mid_(NewtonDomain.Left param2@pos):2078
                /\ fresh_param1@pos:2107 = mid_(NewtonDomain.Left param1@pos):2079
                /\ fresh_param0@pos:2106 = mid_(NewtonDomain.Left param0@pos):2067
                /\ fresh_return@pos:2105 = mid_(NewtonDomain.Left return@pos):2080
                /\ fresh_param2:2104 = mid_(NewtonDomain.Left param2):2071
                /\ fresh_param1:2103 = mid_(NewtonDomain.Left param1):2066
                /\ fresh_param0:2102 = mid_(NewtonDomain.Left param0):2068
                /\ fresh_return:2101 = mid_(NewtonDomain.Left return):2081
                /\ fresh___cost:2100 = mid_(NewtonDomain.Left __cost):2070)
               \/ (1 <= K:2065
                     /\ 0 <= (-fresh_param1:2103 + fresh_param2:2104)
                     /\ 0 <= (-2 + fresh___cost:2100)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2066
                                + mid_(NewtonDomain.Left param2):2071)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):2070))
         /\ K:2082 = 0
         /\ mid_(NewtonDomain.Right return@width):2072 = (NewtonDomain.Right return@width)':2083
         /\ mid_(NewtonDomain.Right return@pos):2073 = (NewtonDomain.Right return@pos)':2084
         /\ mid_(NewtonDomain.Right return):2074 = (NewtonDomain.Right return)':2085
         /\ mid_(NewtonDomain.Left param2@width):2075 = (NewtonDomain.Left param2@width)':2086
         /\ mid_(NewtonDomain.Left param1@width):2076 = (NewtonDomain.Left param1@width)':2087
         /\ mid_(NewtonDomain.Left param0@width):2069 = (NewtonDomain.Left param0@width)':2088
         /\ mid_(NewtonDomain.Left return@width):2077 = (NewtonDomain.Left return@width)':2089
         /\ mid_(NewtonDomain.Left param2@pos):2078 = (NewtonDomain.Left param2@pos)':2090
         /\ mid_(NewtonDomain.Left param1@pos):2079 = (NewtonDomain.Left param1@pos)':2091
         /\ mid_(NewtonDomain.Left param0@pos):2067 = (NewtonDomain.Left param0@pos)':2092
         /\ mid_(NewtonDomain.Left return@pos):2080 = (NewtonDomain.Left return@pos)':2093
         /\ mid_(NewtonDomain.Left param2):2071 = (NewtonDomain.Left param2)':2094
         /\ mid_(NewtonDomain.Left param1):2066 = (NewtonDomain.Left param1)':2095
         /\ mid_(NewtonDomain.Left param0):2068 = (NewtonDomain.Left param0)':2096
         /\ mid_(NewtonDomain.Left return):2081 = (NewtonDomain.Left return)':2097
         /\ mid_(NewtonDomain.Left __cost):2070 = (NewtonDomain.Left __cost)':2098
         /\ 0 = K:2082 /\ (K:2065 + K:2082) = K:2099 /\ 0 <= K:2099
         /\ param2@width:211 = (NewtonDomain.Left param2@width)':2086
         /\ param1@width:158 = (NewtonDomain.Left param1@width)':2087
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':2088
         /\ return@width:406 = (NewtonDomain.Left return@width)':2089
         /\ param2@pos:212 = (NewtonDomain.Left param2@pos)':2090
         /\ param1@pos:159 = (NewtonDomain.Left param1@pos)':2091
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':2092
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':2093
         /\ param2:213 = (NewtonDomain.Left param2)':2094
         /\ param1:160 = (NewtonDomain.Left param1)':2095
         /\ param0:157 = (NewtonDomain.Left param0)':2096
         /\ return:404 = (NewtonDomain.Left return)':2097
         /\ __cost:106 = (NewtonDomain.Left __cost)':2098)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Equivalent star body.
    (IRE-tc)     >> All star bodies equivalent.

NumRnds: 7

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,72)_g1> -> <__pstate, (Unique State Name,64)_g1>	Base relation: 
{param0 := param0:157
 param1 := 0
 param2 := param1:160
 param0@pos := param0@pos:156
 param1@pos := type_err:165
 param2@pos := type_err:166
 param0@width := param0@width:155
 param1@width := type_err:167
 param2@width := type_err:168}	
<__pstate, accept> -> <__pstate, (Unique State Name,72)_g1>	Base relation: 
{__cost := 0
 len := 20
 a := alloc:27
 i := i':293
 param0 := alloc:27
 param1 := 20
 a@pos := 0
 param0@pos := 0
 param1@pos := type_err:295
 a@width := 80
 param0@width := 80
 param1@width := type_err:296
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293)}	
<__pstate, (Unique State Name,64)_g1> -> <__pstate, (Unique State Name,64)_g1>	Base relation: 
{__cost := phi___cost:2418
 m2 := ((havoc:297 + param1:160) + -1)
 a := param0:157
 lo := param1:160
 hi := param2:213
 return := phi_return:2417
 param0 := param0:157
 param1 := phi_param1:2416
 param2 := phi_param2:2415
 a@pos := param0@pos:156
 return@pos := phi_return@pos:2414
 param0@pos := param0@pos:156
 param1@pos := phi_param1@pos:2413
 param2@pos := phi_param2@pos:2412
 a@width := param0@width:155
 return@width := phi_return@width:2411
 param0@width := param0@width:155
 param1@width := phi_param1@width:2410
 param2@width := phi_param2@width:2409
 when ((0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
          /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
          /\ (param1:160 + havoc:297) <= param2:213 /\ 0 <= fresh___cost:1894
          /\ 0 <= (fresh___cost:1894 + 1)
          /\ (fresh_param2:1895 + -fresh_param1:1896) < 1
          /\ (!(0 <= K:1897)
                \/ mid_(NewtonDomain.Left param0):1898 = fresh_param0:1899)
          /\ (!(0 <= K:1897)
                \/ mid_(NewtonDomain.Left param0@pos):1900 = fresh_param0@pos:1901)
          /\ (!(0 <= K:1897)
                \/ mid_(NewtonDomain.Left param1):1902 = fresh_param1:1896)
          /\ (!(0 <= K:1897)
                \/ mid_(NewtonDomain.Left param0@width):1903 = fresh_param0@width:1904)
          /\ (!(0 <= K:1897)
                \/ (-mid_(NewtonDomain.Left __cost):1905
                      + (-2 * mid_(NewtonDomain.Left param2):1906)) <= (
                   -fresh___cost:1894 + (-2 * fresh_param2:1895)))
          /\ ((K:1897 = 0
                 /\ type_err:1907 = mid_(NewtonDomain.Right return@width):1908
                 /\ type_err:1909 = mid_(NewtonDomain.Right return@pos):1910
                 /\ havoc:1911 = mid_(NewtonDomain.Right return):1912
                 /\ fresh_param2@width:1913 = mid_(NewtonDomain.Left param2@width):1914
                 /\ fresh_param1@width:1915 = mid_(NewtonDomain.Left param1@width):1916
                 /\ fresh_param0@width:1904 = mid_(NewtonDomain.Left param0@width):1903
                 /\ fresh_return@width:1917 = mid_(NewtonDomain.Left return@width):1918
                 /\ fresh_param2@pos:1919 = mid_(NewtonDomain.Left param2@pos):1920
                 /\ fresh_param1@pos:1921 = mid_(NewtonDomain.Left param1@pos):1922
                 /\ fresh_param0@pos:1901 = mid_(NewtonDomain.Left param0@pos):1900
                 /\ fresh_return@pos:1923 = mid_(NewtonDomain.Left return@pos):1924
                 /\ fresh_param2:1895 = mid_(NewtonDomain.Left param2):1906
                 /\ fresh_param1:1896 = mid_(NewtonDomain.Left param1):1902
                 /\ fresh_param0:1899 = mid_(NewtonDomain.Left param0):1898
                 /\ fresh_return:1925 = mid_(NewtonDomain.Left return):1926
                 /\ fresh___cost:1894 = mid_(NewtonDomain.Left __cost):1905)
                \/ (1 <= K:1897
                      /\ 0 <= (-fresh_param1:1896 + fresh_param2:1895)
                      /\ 0 <= (-2 + fresh___cost:1894)
                      /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1902
                                 + mid_(NewtonDomain.Left param2):1906)
                      /\ 0 <= mid_(NewtonDomain.Left __cost):1905))
          /\ K:1927 = 0
          /\ mid_(NewtonDomain.Right return@width):1908 = (NewtonDomain.Right return@width)':1928
          /\ mid_(NewtonDomain.Right return@pos):1910 = (NewtonDomain.Right return@pos)':1929
          /\ mid_(NewtonDomain.Right return):1912 = (NewtonDomain.Right return)':1930
          /\ mid_(NewtonDomain.Left param2@width):1914 = (NewtonDomain.Left param2@width)':1931
          /\ mid_(NewtonDomain.Left param1@width):1916 = (NewtonDomain.Left param1@width)':1932
          /\ mid_(NewtonDomain.Left param0@width):1903 = (NewtonDomain.Left param0@width)':1933
          /\ mid_(NewtonDomain.Left return@width):1918 = (NewtonDomain.Left return@width)':1934
          /\ mid_(NewtonDomain.Left param2@pos):1920 = (NewtonDomain.Left param2@pos)':1935
          /\ mid_(NewtonDomain.Left param1@pos):1922 = (NewtonDomain.Left param1@pos)':1936
          /\ mid_(NewtonDomain.Left param0@pos):1900 = (NewtonDomain.Left param0@pos)':1937
          /\ mid_(NewtonDomain.Left return@pos):1924 = (NewtonDomain.Left return@pos)':1938
          /\ mid_(NewtonDomain.Left param2):1906 = (NewtonDomain.Left param2)':1939
          /\ mid_(NewtonDomain.Left param1):1902 = (NewtonDomain.Left param1)':1940
          /\ mid_(NewtonDomain.Left param0):1898 = (NewtonDomain.Left param0)':1941
          /\ mid_(NewtonDomain.Left return):1926 = (NewtonDomain.Left return)':1942
          /\ mid_(NewtonDomain.Left __cost):1905 = (NewtonDomain.Left __cost)':1943
          /\ 0 = K:1927 /\ (K:1897 + K:1927) = K:1944 /\ 0 <= K:1944
          /\ type_err:301 = (NewtonDomain.Left param2@width)':1931
          /\ type_err:300 = (NewtonDomain.Left param1@width)':1932
          /\ param0@width:155 = (NewtonDomain.Left param0@width)':1933
          /\ return@width:406 = (NewtonDomain.Left return@width)':1934
          /\ type_err:299 = (NewtonDomain.Left param2@pos)':1935
          /\ type_err:298 = (NewtonDomain.Left param1@pos)':1936
          /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1937
          /\ return@pos:405 = (NewtonDomain.Left return@pos)':1938
          /\ param2:213 = (NewtonDomain.Left param2)':1939
          /\ (havoc:297 + param1:160) = (NewtonDomain.Left param1)':1940
          /\ param0:157 = (NewtonDomain.Left param0)':1941
          /\ return:404 = (NewtonDomain.Left return)':1942
          /\ (__cost:106 + 1) = (NewtonDomain.Left __cost)':1943
          /\ (fresh___cost:1894 + 1) = phi___cost:2418
          /\ (NewtonDomain.Right return)':1930 = phi_return:2417
          /\ param1:160 = phi_param1:2416
          /\ ((havoc:297 + param1:160) + -1) = phi_param2:2415
          /\ (NewtonDomain.Right return@pos)':1929 = phi_return@pos:2414
          /\ type_err:1945 = phi_param1@pos:2413
          /\ type_err:1946 = phi_param2@pos:2412
          /\ (NewtonDomain.Right return@width)':1928 = phi_return@width:2411
          /\ type_err:1947 = phi_param1@width:2410
          /\ type_err:1948 = phi_param2@width:2409)
         \/ (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
               /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
               /\ (param1:160 + havoc:297) <= param2:213
               /\ (__cost:106 + 1) = phi___cost:2418
               /\ return:404 = phi_return:2417
               /\ (havoc:297 + param1:160) = phi_param1:2416
               /\ param2:213 = phi_param2:2415
               /\ return@pos:405 = phi_return@pos:2414
               /\ type_err:298 = phi_param1@pos:2413
               /\ type_err:299 = phi_param2@pos:2412
               /\ return@width:406 = phi_return@width:2411
               /\ type_err:300 = phi_param1@width:2410
               /\ type_err:301 = phi_param2@width:2409))}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x9b64fe0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x9b65090: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,64)_g1 , __done )	Base relation: 
{__cost := __cost':2547
 len := 20
 a := alloc:27
 i := i':293
 m2 := m2':2546
 a := a':2545
 lo := lo':2544
 hi := hi':2543
 return := return':2542
 param0 := param0':2541
 param1 := param1':2540
 param2 := param2':2539
 a@pos := 0
 a@pos := a@pos':2538
 return@pos := return@pos':2537
 param0@pos := param0@pos':2536
 param1@pos := param1@pos':2535
 param2@pos := param2@pos':2534
 a@width := 80
 a@width := a@width':2533
 return@width := return@width':2532
 param0@width := param0@width':2531
 param1@width := param1@width':2530
 param2@width := param2@width':2529
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293
         /\ (!(0 <= K:2508) \/ mid_param0@width:2509 = 80)
         /\ (!((0 <= K:2508 /\ K:2508 <= 0))
               \/ mid_a@width:2510 = a@width:191)
         /\ (!(1 <= K:2508) \/ mid_a@width:2510 = 80)
         /\ (!(0 <= K:2508) \/ mid_param0:2511 = alloc:27)
         /\ (!(0 <= K:2508) \/ mid_param0@pos:2512 = 0)
         /\ (!((0 <= K:2508 /\ K:2508 <= 0)) \/ mid_a@pos:2513 = a@pos:192)
         /\ (!(1 <= K:2508) \/ mid_a@pos:2513 = 0)
         /\ (!((0 <= K:2508 /\ K:2508 <= 0)) \/ mid_a:2514 = a:193)
         /\ (!(1 <= K:2508) \/ mid_a:2514 = alloc:27)
         /\ (!(0 <= K:2508)
               \/ (mid___cost:2515 + (2 * mid_param2:2516)) <= (40 + K:2508))
         /\ (!(0 <= K:2508)
               \/ (mid___cost:2515 + -mid_param1:2517 + (2 * mid_param2:2516)) <= 40)
         /\ (!(0 <= K:2508) \/ mid_param2:2516 <= 20)
         /\ (!(0 <= K:2508)
               \/ (-mid_param1:2517 + mid_param2:2516) <= (20 + -K:2508))
         /\ (!(0 <= K:2508) \/ -mid_param1:2517 <= 0)
         /\ ((K:2508 = 0 /\ type_err:2422 = mid_param2@width:2518
                /\ type_err:2421 = mid_param1@width:2519
                /\ 80 = mid_param0@width:2509
                /\ return@width:406 = mid_return@width:2520
                /\ a@width:191 = mid_a@width:2510
                /\ type_err:2420 = mid_param2@pos:2521
                /\ type_err:2419 = mid_param1@pos:2522
                /\ 0 = mid_param0@pos:2512
                /\ return@pos:405 = mid_return@pos:2523
                /\ a@pos:192 = mid_a@pos:2513 /\ 20 = mid_param2:2516
                /\ 0 = mid_param1:2517 /\ alloc:27 = mid_param0:2511
                /\ return:404 = mid_return:2524 /\ hi:182 = mid_hi:2525
                /\ lo:181 = mid_lo:2526 /\ a:193 = mid_a:2514
                /\ m2:198 = mid_m2:2527 /\ 0 = mid___cost:2515)
               \/ (1 <= K:2508 /\ 0 <= (-1 + 20)
                     /\ (-mid_a:2514 + mid_param0:2511) = 0
                     /\ (-mid_a@pos:2513 + mid_param0@pos:2512) = 0
                     /\ (-mid_a@width:2510 + mid_param0@width:2509) = 0
                     /\ 0 <= (-1 + -mid_lo:2526 + -mid_param2:2516
                                + mid_hi:2525 + mid_param1:2517)
                     /\ 0 <= (-mid_lo:2526 + mid_m2:2527)
                     /\ 0 <= (-mid_lo:2526 + mid_param1:2517)
                     /\ 0 <= (-2 + -mid_lo:2526 + mid___cost:2515
                                + mid_param1:2517)
                     /\ 0 <= (-mid_param2:2516 + mid_hi:2525)
                     /\ 0 <= (1 + -mid_param1:2517 + mid_m2:2527)
                     /\ 0 <= (-1 + mid_hi:2525 + -mid_m2:2527)
                     /\ 0 <= (mid_param2:2516 + -mid_param1:2517)
                     /\ 0 <= (mid_param2:2516 + -mid_m2:2527)
                     /\ 0 <= (-1 + mid___cost:2515)
                     /\ 0 <= (-2 + mid___cost:2515 + mid_param2:2516
                                + -mid_m2:2527))) /\ K:2528 = 0
         /\ mid_param2@width:2518 = param2@width':2529
         /\ mid_param1@width:2519 = param1@width':2530
         /\ mid_param0@width:2509 = param0@width':2531
         /\ mid_return@width:2520 = return@width':2532
         /\ mid_a@width:2510 = a@width':2533
         /\ mid_param2@pos:2521 = param2@pos':2534
         /\ mid_param1@pos:2522 = param1@pos':2535
         /\ mid_param0@pos:2512 = param0@pos':2536
         /\ mid_return@pos:2523 = return@pos':2537
         /\ mid_a@pos:2513 = a@pos':2538 /\ mid_param2:2516 = param2':2539
         /\ mid_param1:2517 = param1':2540 /\ mid_param0:2511 = param0':2541
         /\ mid_return:2524 = return':2542 /\ mid_hi:2525 = hi':2543
         /\ mid_lo:2526 = lo':2544 /\ mid_a:2514 = a':2545
         /\ mid_m2:2527 = m2':2546 /\ mid___cost:2515 = __cost':2547
         /\ 0 = K:2528 /\ (K:2508 + K:2528) = K:2548 /\ 0 <= K:2548)}
    ( __pstate , (Unique State Name,72)_g1 , __done )	Base relation: 
{__cost := 0
 len := 20
 a := alloc:27
 i := i':293
 param0 := alloc:27
 param1 := 20
 a@pos := 0
 param0@pos := 0
 param1@pos := type_err:295
 a@width := 80
 param0@width := 80
 param1@width := type_err:296
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293)}

Weights on states: 
__pstate 0x9b65950: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x9b65aa0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
================================================
Procedure Summaries

------------------------------------------------
Procedure summary for main

Base relation: 
{__cost := (fresh___cost:2227 + 1)
 len := 20
 a := alloc:27
 i := i':293
 return := 0
 param0 := fresh_param0:2235
 param1 := fresh_param1:2229
 param2 := fresh_param2:2228
 a@pos := 0
 return@pos := type_err:2285
 param0@pos := fresh_param0@pos:2233
 param1@pos := fresh_param1@pos:2254
 param2@pos := fresh_param2@pos:2252
 a@width := 80
 return@width := type_err:2286
 param0@width := fresh_param0@width:2237
 param1@width := fresh_param1@width:2248
 param2@width := fresh_param2@width:2246
 when ((!(0 <= K:290) \/ mid_i:291 = K:290)
         /\ ((K:290 = 0 /\ 0 = mid_i:291)
               \/ (1 <= K:290 /\ (-20 + 20) = 0 /\ (-20 + 20) = 0
                     /\ 0 <= (20 + -mid_i:291) /\ 0 <= (-1 + mid_i:291)))
         /\ K:292 = 0 /\ mid_i:291 = i':293 /\ 0 = K:292
         /\ (K:290 + K:292) = K:294 /\ 0 <= K:294 /\ i':293 <= 20
         /\ 0 <= i':293 /\ 20 <= i':293 /\ 0 <= fresh___cost:2227
         /\ 0 <= (fresh___cost:2227 + 1)
         /\ (fresh_param2:2228 + -fresh_param1:2229) < 1
         /\ (!(0 <= K:2230)
               \/ mid_(NewtonDomain.Left param1):2231 = fresh_param1:2229)
         /\ (!(0 <= K:2230)
               \/ mid_(NewtonDomain.Left param0@pos):2232 = fresh_param0@pos:2233)
         /\ (!(0 <= K:2230)
               \/ mid_(NewtonDomain.Left param0):2234 = fresh_param0:2235)
         /\ (!(0 <= K:2230)
               \/ mid_(NewtonDomain.Left param0@width):2236 = fresh_param0@width:2237)
         /\ (!(0 <= K:2230)
               \/ (-mid_(NewtonDomain.Left __cost):2238
                     + (-2 * mid_(NewtonDomain.Left param2):2239)) <= (
                  -fresh___cost:2227 + (-2 * fresh_param2:2228)))
         /\ ((K:2230 = 0
                /\ type_err:2240 = mid_(NewtonDomain.Right return@width):2241
                /\ type_err:2242 = mid_(NewtonDomain.Right return@pos):2243
                /\ havoc:2244 = mid_(NewtonDomain.Right return):2245
                /\ fresh_param2@width:2246 = mid_(NewtonDomain.Left param2@width):2247
                /\ fresh_param1@width:2248 = mid_(NewtonDomain.Left param1@width):2249
                /\ fresh_param0@width:2237 = mid_(NewtonDomain.Left param0@width):2236
                /\ fresh_return@width:2250 = mid_(NewtonDomain.Left return@width):2251
                /\ fresh_param2@pos:2252 = mid_(NewtonDomain.Left param2@pos):2253
                /\ fresh_param1@pos:2254 = mid_(NewtonDomain.Left param1@pos):2255
                /\ fresh_param0@pos:2233 = mid_(NewtonDomain.Left param0@pos):2232
                /\ fresh_return@pos:2256 = mid_(NewtonDomain.Left return@pos):2257
                /\ fresh_param2:2228 = mid_(NewtonDomain.Left param2):2239
                /\ fresh_param1:2229 = mid_(NewtonDomain.Left param1):2231
                /\ fresh_param0:2235 = mid_(NewtonDomain.Left param0):2234
                /\ fresh_return:2258 = mid_(NewtonDomain.Left return):2259
                /\ fresh___cost:2227 = mid_(NewtonDomain.Left __cost):2238)
               \/ (1 <= K:2230
                     /\ 0 <= (-fresh_param1:2229 + fresh_param2:2228)
                     /\ 0 <= (-2 + fresh___cost:2227)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2231
                                + mid_(NewtonDomain.Left param2):2239)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):2238))
         /\ K:2260 = 0
         /\ mid_(NewtonDomain.Right return@width):2241 = (NewtonDomain.Right return@width)':2261
         /\ mid_(NewtonDomain.Right return@pos):2243 = (NewtonDomain.Right return@pos)':2262
         /\ mid_(NewtonDomain.Right return):2245 = (NewtonDomain.Right return)':2263
         /\ mid_(NewtonDomain.Left param2@width):2247 = (NewtonDomain.Left param2@width)':2264
         /\ mid_(NewtonDomain.Left param1@width):2249 = (NewtonDomain.Left param1@width)':2265
         /\ mid_(NewtonDomain.Left param0@width):2236 = (NewtonDomain.Left param0@width)':2266
         /\ mid_(NewtonDomain.Left return@width):2251 = (NewtonDomain.Left return@width)':2267
         /\ mid_(NewtonDomain.Left param2@pos):2253 = (NewtonDomain.Left param2@pos)':2268
         /\ mid_(NewtonDomain.Left param1@pos):2255 = (NewtonDomain.Left param1@pos)':2269
         /\ mid_(NewtonDomain.Left param0@pos):2232 = (NewtonDomain.Left param0@pos)':2270
         /\ mid_(NewtonDomain.Left return@pos):2257 = (NewtonDomain.Left return@pos)':2271
         /\ mid_(NewtonDomain.Left param2):2239 = (NewtonDomain.Left param2)':2272
         /\ mid_(NewtonDomain.Left param1):2231 = (NewtonDomain.Left param1)':2273
         /\ mid_(NewtonDomain.Left param0):2234 = (NewtonDomain.Left param0)':2274
         /\ mid_(NewtonDomain.Left return):2259 = (NewtonDomain.Left return)':2275
         /\ mid_(NewtonDomain.Left __cost):2238 = (NewtonDomain.Left __cost)':2276
         /\ 0 = K:2260 /\ (K:2230 + K:2260) = K:2277 /\ 0 <= K:2277
         /\ type_err:2278 = (NewtonDomain.Left param2@width)':2264
         /\ type_err:2279 = (NewtonDomain.Left param1@width)':2265
         /\ 80 = (NewtonDomain.Left param0@width)':2266
         /\ return@width:406 = (NewtonDomain.Left return@width)':2267
         /\ type_err:2280 = (NewtonDomain.Left param2@pos)':2268
         /\ type_err:2281 = (NewtonDomain.Left param1@pos)':2269
         /\ 0 = (NewtonDomain.Left param0@pos)':2270
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':2271
         /\ 20 = (NewtonDomain.Left param2)':2272
         /\ 0 = (NewtonDomain.Left param1)':2273
         /\ alloc:27 = (NewtonDomain.Left param0)':2274
         /\ return:404 = (NewtonDomain.Left return)':2275
         /\ 0 = (NewtonDomain.Left __cost)':2276)}

------------------------------------------------
Procedure summary for qsort

Base relation: 
{__cost := phi___cost:2351
 m2 := phi_m2:2350
 a := param0:157
 lo := param1:160
 hi := param2:213
 return := havoc:2352
 param0 := phi_param0:2348
 param1 := phi_param1:2347
 param2 := phi_param2:2346
 a@pos := param0@pos:156
 return@pos := type_err:2353
 param0@pos := phi_param0@pos:2344
 param1@pos := phi_param1@pos:2343
 param2@pos := phi_param2@pos:2342
 a@width := param0@width:155
 return@width := type_err:2354
 param0@width := phi_param0@width:2340
 param1@width := phi_param1@width:2339
 param2@width := phi_param2@width:2338
 when ((0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
          /\ (param2:213 + -param1:160) < 1
          /\ (__cost:106 + 1) = phi___cost:2351 /\ m2:198 = phi_m2:2350
          /\ return:404 = phi_return:2349 /\ param0:157 = phi_param0:2348
          /\ param1:160 = phi_param1:2347 /\ param2:213 = phi_param2:2346
          /\ return@pos:405 = phi_return@pos:2345
          /\ param0@pos:156 = phi_param0@pos:2344
          /\ param1@pos:159 = phi_param1@pos:2343
          /\ param2@pos:212 = phi_param2@pos:2342
          /\ return@width:406 = phi_return@width:2341
          /\ param0@width:155 = phi_param0@width:2340
          /\ param1@width:158 = phi_param1@width:2339
          /\ param2@width:211 = phi_param2@width:2338)
         \/ (0 <= __cost:106 /\ 0 <= (__cost:106 + 1)
               /\ 1 <= (param2:213 + -param1:160) /\ 0 < havoc:297
               /\ (param1:160 + havoc:297) <= param2:213
               /\ 0 <= fresh___cost:1894 /\ 0 <= (fresh___cost:1894 + 1)
               /\ (fresh_param2:1895 + -fresh_param1:1896) < 1
               /\ (!(0 <= K:1897)
                     \/ mid_(NewtonDomain.Left param0):1898 = fresh_param0:1899)
               /\ (!(0 <= K:1897)
                     \/ mid_(NewtonDomain.Left param0@pos):1900 = fresh_param0@pos:1901)
               /\ (!(0 <= K:1897)
                     \/ mid_(NewtonDomain.Left param1):1902 = fresh_param1:1896)
               /\ (!(0 <= K:1897)
                     \/ mid_(NewtonDomain.Left param0@width):1903 = fresh_param0@width:1904)
               /\ (!(0 <= K:1897)
                     \/ (-mid_(NewtonDomain.Left __cost):1905
                           + (-2 * mid_(NewtonDomain.Left param2):1906)) <= (
                        -fresh___cost:1894 + (-2 * fresh_param2:1895)))
               /\ ((K:1897 = 0
                      /\ type_err:1907 = mid_(NewtonDomain.Right return@width):1908
                      /\ type_err:1909 = mid_(NewtonDomain.Right return@pos):1910
                      /\ havoc:1911 = mid_(NewtonDomain.Right return):1912
                      /\ fresh_param2@width:1913 = mid_(NewtonDomain.Left param2@width):1914
                      /\ fresh_param1@width:1915 = mid_(NewtonDomain.Left param1@width):1916
                      /\ fresh_param0@width:1904 = mid_(NewtonDomain.Left param0@width):1903
                      /\ fresh_return@width:1917 = mid_(NewtonDomain.Left return@width):1918
                      /\ fresh_param2@pos:1919 = mid_(NewtonDomain.Left param2@pos):1920
                      /\ fresh_param1@pos:1921 = mid_(NewtonDomain.Left param1@pos):1922
                      /\ fresh_param0@pos:1901 = mid_(NewtonDomain.Left param0@pos):1900
                      /\ fresh_return@pos:1923 = mid_(NewtonDomain.Left return@pos):1924
                      /\ fresh_param2:1895 = mid_(NewtonDomain.Left param2):1906
                      /\ fresh_param1:1896 = mid_(NewtonDomain.Left param1):1902
                      /\ fresh_param0:1899 = mid_(NewtonDomain.Left param0):1898
                      /\ fresh_return:1925 = mid_(NewtonDomain.Left return):1926
                      /\ fresh___cost:1894 = mid_(NewtonDomain.Left __cost):1905)
                     \/ (1 <= K:1897
                           /\ 0 <= (-fresh_param1:1896 + fresh_param2:1895)
                           /\ 0 <= (-2 + fresh___cost:1894)
                           /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):1902
                                      + mid_(NewtonDomain.Left param2):1906)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1905))
               /\ K:1927 = 0
               /\ mid_(NewtonDomain.Right return@width):1908 = (NewtonDomain.Right return@width)':1928
               /\ mid_(NewtonDomain.Right return@pos):1910 = (NewtonDomain.Right return@pos)':1929
               /\ mid_(NewtonDomain.Right return):1912 = (NewtonDomain.Right return)':1930
               /\ mid_(NewtonDomain.Left param2@width):1914 = (NewtonDomain.Left param2@width)':1931
               /\ mid_(NewtonDomain.Left param1@width):1916 = (NewtonDomain.Left param1@width)':1932
               /\ mid_(NewtonDomain.Left param0@width):1903 = (NewtonDomain.Left param0@width)':1933
               /\ mid_(NewtonDomain.Left return@width):1918 = (NewtonDomain.Left return@width)':1934
               /\ mid_(NewtonDomain.Left param2@pos):1920 = (NewtonDomain.Left param2@pos)':1935
               /\ mid_(NewtonDomain.Left param1@pos):1922 = (NewtonDomain.Left param1@pos)':1936
               /\ mid_(NewtonDomain.Left param0@pos):1900 = (NewtonDomain.Left param0@pos)':1937
               /\ mid_(NewtonDomain.Left return@pos):1924 = (NewtonDomain.Left return@pos)':1938
               /\ mid_(NewtonDomain.Left param2):1906 = (NewtonDomain.Left param2)':1939
               /\ mid_(NewtonDomain.Left param1):1902 = (NewtonDomain.Left param1)':1940
               /\ mid_(NewtonDomain.Left param0):1898 = (NewtonDomain.Left param0)':1941
               /\ mid_(NewtonDomain.Left return):1926 = (NewtonDomain.Left return)':1942
               /\ mid_(NewtonDomain.Left __cost):1905 = (NewtonDomain.Left __cost)':1943
               /\ 0 = K:1927 /\ (K:1897 + K:1927) = K:1944 /\ 0 <= K:1944
               /\ type_err:301 = (NewtonDomain.Left param2@width)':1931
               /\ type_err:300 = (NewtonDomain.Left param1@width)':1932
               /\ param0@width:155 = (NewtonDomain.Left param0@width)':1933
               /\ return@width:406 = (NewtonDomain.Left return@width)':1934
               /\ type_err:299 = (NewtonDomain.Left param2@pos)':1935
               /\ type_err:298 = (NewtonDomain.Left param1@pos)':1936
               /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':1937
               /\ return@pos:405 = (NewtonDomain.Left return@pos)':1938
               /\ param2:213 = (NewtonDomain.Left param2)':1939
               /\ (havoc:297 + param1:160) = (NewtonDomain.Left param1)':1940
               /\ param0:157 = (NewtonDomain.Left param0)':1941
               /\ return:404 = (NewtonDomain.Left return)':1942
               /\ (__cost:106 + 1) = (NewtonDomain.Left __cost)':1943
               /\ 0 <= fresh___cost:2287 /\ 0 <= (fresh___cost:2287 + 1)
               /\ (fresh_param2:2288 + -fresh_param1:2289) < 1
               /\ (!(0 <= K:2290)
                     \/ mid_(NewtonDomain.Left param0):2291 = fresh_param0:2292)
               /\ (!(0 <= K:2290)
                     \/ mid_(NewtonDomain.Left param0@pos):2293 = fresh_param0@pos:2294)
               /\ (!(0 <= K:2290)
                     \/ mid_(NewtonDomain.Left param1):2295 = fresh_param1:2289)
               /\ (!(0 <= K:2290)
                     \/ mid_(NewtonDomain.Left param0@width):2296 = fresh_param0@width:2297)
               /\ (!(0 <= K:2290)
                     \/ (-mid_(NewtonDomain.Left __cost):2298
                           + (-2 * mid_(NewtonDomain.Left param2):2299)) <= (
                        -fresh___cost:2287 + (-2 * fresh_param2:2288)))
               /\ ((K:2290 = 0
                      /\ type_err:2300 = mid_(NewtonDomain.Right return@width):2301
                      /\ type_err:2302 = mid_(NewtonDomain.Right return@pos):2303
                      /\ havoc:2304 = mid_(NewtonDomain.Right return):2305
                      /\ fresh_param2@width:2306 = mid_(NewtonDomain.Left param2@width):2307
                      /\ fresh_param1@width:2308 = mid_(NewtonDomain.Left param1@width):2309
                      /\ fresh_param0@width:2297 = mid_(NewtonDomain.Left param0@width):2296
                      /\ fresh_return@width:2310 = mid_(NewtonDomain.Left return@width):2311
                      /\ fresh_param2@pos:2312 = mid_(NewtonDomain.Left param2@pos):2313
                      /\ fresh_param1@pos:2314 = mid_(NewtonDomain.Left param1@pos):2315
                      /\ fresh_param0@pos:2294 = mid_(NewtonDomain.Left param0@pos):2293
                      /\ fresh_return@pos:2316 = mid_(NewtonDomain.Left return@pos):2317
                      /\ fresh_param2:2288 = mid_(NewtonDomain.Left param2):2299
                      /\ fresh_param1:2289 = mid_(NewtonDomain.Left param1):2295
                      /\ fresh_param0:2292 = mid_(NewtonDomain.Left param0):2291
                      /\ fresh_return:2318 = mid_(NewtonDomain.Left return):2319
                      /\ fresh___cost:2287 = mid_(NewtonDomain.Left __cost):2298)
                     \/ (1 <= K:2290
                           /\ 0 <= (-fresh_param1:2289 + fresh_param2:2288)
                           /\ 0 <= (-2 + fresh___cost:2287)
                           /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2295
                                      + mid_(NewtonDomain.Left param2):2299)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):2298))
               /\ K:2320 = 0
               /\ mid_(NewtonDomain.Right return@width):2301 = (NewtonDomain.Right return@width)':2321
               /\ mid_(NewtonDomain.Right return@pos):2303 = (NewtonDomain.Right return@pos)':2322
               /\ mid_(NewtonDomain.Right return):2305 = (NewtonDomain.Right return)':2323
               /\ mid_(NewtonDomain.Left param2@width):2307 = (NewtonDomain.Left param2@width)':2324
               /\ mid_(NewtonDomain.Left param1@width):2309 = (NewtonDomain.Left param1@width)':2325
               /\ mid_(NewtonDomain.Left param0@width):2296 = (NewtonDomain.Left param0@width)':2326
               /\ mid_(NewtonDomain.Left return@width):2311 = (NewtonDomain.Left return@width)':2327
               /\ mid_(NewtonDomain.Left param2@pos):2313 = (NewtonDomain.Left param2@pos)':2328
               /\ mid_(NewtonDomain.Left param1@pos):2315 = (NewtonDomain.Left param1@pos)':2329
               /\ mid_(NewtonDomain.Left param0@pos):2293 = (NewtonDomain.Left param0@pos)':2330
               /\ mid_(NewtonDomain.Left return@pos):2317 = (NewtonDomain.Left return@pos)':2331
               /\ mid_(NewtonDomain.Left param2):2299 = (NewtonDomain.Left param2)':2332
               /\ mid_(NewtonDomain.Left param1):2295 = (NewtonDomain.Left param1)':2333
               /\ mid_(NewtonDomain.Left param0):2291 = (NewtonDomain.Left param0)':2334
               /\ mid_(NewtonDomain.Left return):2319 = (NewtonDomain.Left return)':2335
               /\ mid_(NewtonDomain.Left __cost):2298 = (NewtonDomain.Left __cost)':2336
               /\ 0 = K:2320 /\ (K:2290 + K:2320) = K:2337 /\ 0 <= K:2337
               /\ type_err:1948 = (NewtonDomain.Left param2@width)':2324
               /\ type_err:1947 = (NewtonDomain.Left param1@width)':2325
               /\ param0@width:155 = (NewtonDomain.Left param0@width)':2326
               /\ (NewtonDomain.Right return@width)':1928 = (NewtonDomain.Left return@width)':2327
               /\ type_err:1946 = (NewtonDomain.Left param2@pos)':2328
               /\ type_err:1945 = (NewtonDomain.Left param1@pos)':2329
               /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':2330
               /\ (NewtonDomain.Right return@pos)':1929 = (NewtonDomain.Left return@pos)':2331
               /\ ((havoc:297 + param1:160) + -1) = (NewtonDomain.Left param2)':2332
               /\ param1:160 = (NewtonDomain.Left param1)':2333
               /\ param0:157 = (NewtonDomain.Left param0)':2334
               /\ (NewtonDomain.Right return)':1930 = (NewtonDomain.Left return)':2335
               /\ (fresh___cost:1894 + 1) = (NewtonDomain.Left __cost)':2336
               /\ (fresh___cost:2287 + 1) = phi___cost:2351
               /\ ((havoc:297 + param1:160) + -1) = phi_m2:2350
               /\ (NewtonDomain.Right return)':2323 = phi_return:2349
               /\ fresh_param0:2292 = phi_param0:2348
               /\ fresh_param1:2289 = phi_param1:2347
               /\ fresh_param2:2288 = phi_param2:2346
               /\ (NewtonDomain.Right return@pos)':2322 = phi_return@pos:2345
               /\ fresh_param0@pos:2294 = phi_param0@pos:2344
               /\ fresh_param1@pos:2314 = phi_param1@pos:2343
               /\ fresh_param2@pos:2312 = phi_param2@pos:2342
               /\ (NewtonDomain.Right return@width)':2321 = phi_return@width:2341
               /\ fresh_param0@width:2297 = phi_param0@width:2340
               /\ fresh_param1@width:2308 = phi_param1@width:2339
               /\ fresh_param2@width:2306 = phi_param2@width:2338))}

------------------------------------------------
Procedure summary for start

Base relation: 
{__cost := (fresh___cost:2355 + 1)
 return := havoc:2406
 param0 := fresh_param0:2360
 param1 := fresh_param1:2357
 param2 := fresh_param2:2356
 return@pos := type_err:2407
 param0@pos := fresh_param0@pos:2362
 param1@pos := fresh_param1@pos:2382
 param2@pos := fresh_param2@pos:2380
 return@width := type_err:2408
 param0@width := fresh_param0@width:2365
 param1@width := fresh_param1@width:2376
 param2@width := fresh_param2@width:2374
 when (0 <= fresh___cost:2355 /\ 0 <= (fresh___cost:2355 + 1)
         /\ (fresh_param2:2356 + -fresh_param1:2357) < 1
         /\ (!(0 <= K:2358)
               \/ mid_(NewtonDomain.Left param0):2359 = fresh_param0:2360)
         /\ (!(0 <= K:2358)
               \/ mid_(NewtonDomain.Left param0@pos):2361 = fresh_param0@pos:2362)
         /\ (!(0 <= K:2358)
               \/ mid_(NewtonDomain.Left param1):2363 = fresh_param1:2357)
         /\ (!(0 <= K:2358)
               \/ mid_(NewtonDomain.Left param0@width):2364 = fresh_param0@width:2365)
         /\ (!(0 <= K:2358)
               \/ (-mid_(NewtonDomain.Left __cost):2366
                     + (-2 * mid_(NewtonDomain.Left param2):2367)) <= (
                  -fresh___cost:2355 + (-2 * fresh_param2:2356)))
         /\ ((K:2358 = 0
                /\ type_err:2368 = mid_(NewtonDomain.Right return@width):2369
                /\ type_err:2370 = mid_(NewtonDomain.Right return@pos):2371
                /\ havoc:2372 = mid_(NewtonDomain.Right return):2373
                /\ fresh_param2@width:2374 = mid_(NewtonDomain.Left param2@width):2375
                /\ fresh_param1@width:2376 = mid_(NewtonDomain.Left param1@width):2377
                /\ fresh_param0@width:2365 = mid_(NewtonDomain.Left param0@width):2364
                /\ fresh_return@width:2378 = mid_(NewtonDomain.Left return@width):2379
                /\ fresh_param2@pos:2380 = mid_(NewtonDomain.Left param2@pos):2381
                /\ fresh_param1@pos:2382 = mid_(NewtonDomain.Left param1@pos):2383
                /\ fresh_param0@pos:2362 = mid_(NewtonDomain.Left param0@pos):2361
                /\ fresh_return@pos:2384 = mid_(NewtonDomain.Left return@pos):2385
                /\ fresh_param2:2356 = mid_(NewtonDomain.Left param2):2367
                /\ fresh_param1:2357 = mid_(NewtonDomain.Left param1):2363
                /\ fresh_param0:2360 = mid_(NewtonDomain.Left param0):2359
                /\ fresh_return:2386 = mid_(NewtonDomain.Left return):2387
                /\ fresh___cost:2355 = mid_(NewtonDomain.Left __cost):2366)
               \/ (1 <= K:2358
                     /\ 0 <= (-fresh_param1:2357 + fresh_param2:2356)
                     /\ 0 <= (-2 + fresh___cost:2355)
                     /\ 0 <= (-1 + -mid_(NewtonDomain.Left param1):2363
                                + mid_(NewtonDomain.Left param2):2367)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):2366))
         /\ K:2388 = 0
         /\ mid_(NewtonDomain.Right return@width):2369 = (NewtonDomain.Right return@width)':2389
         /\ mid_(NewtonDomain.Right return@pos):2371 = (NewtonDomain.Right return@pos)':2390
         /\ mid_(NewtonDomain.Right return):2373 = (NewtonDomain.Right return)':2391
         /\ mid_(NewtonDomain.Left param2@width):2375 = (NewtonDomain.Left param2@width)':2392
         /\ mid_(NewtonDomain.Left param1@width):2377 = (NewtonDomain.Left param1@width)':2393
         /\ mid_(NewtonDomain.Left param0@width):2364 = (NewtonDomain.Left param0@width)':2394
         /\ mid_(NewtonDomain.Left return@width):2379 = (NewtonDomain.Left return@width)':2395
         /\ mid_(NewtonDomain.Left param2@pos):2381 = (NewtonDomain.Left param2@pos)':2396
         /\ mid_(NewtonDomain.Left param1@pos):2383 = (NewtonDomain.Left param1@pos)':2397
         /\ mid_(NewtonDomain.Left param0@pos):2361 = (NewtonDomain.Left param0@pos)':2398
         /\ mid_(NewtonDomain.Left return@pos):2385 = (NewtonDomain.Left return@pos)':2399
         /\ mid_(NewtonDomain.Left param2):2367 = (NewtonDomain.Left param2)':2400
         /\ mid_(NewtonDomain.Left param1):2363 = (NewtonDomain.Left param1)':2401
         /\ mid_(NewtonDomain.Left param0):2359 = (NewtonDomain.Left param0)':2402
         /\ mid_(NewtonDomain.Left return):2387 = (NewtonDomain.Left return)':2403
         /\ mid_(NewtonDomain.Left __cost):2366 = (NewtonDomain.Left __cost)':2404
         /\ 0 = K:2388 /\ (K:2358 + K:2388) = K:2405 /\ 0 <= K:2405
         /\ type_err:168 = (NewtonDomain.Left param2@width)':2392
         /\ type_err:167 = (NewtonDomain.Left param1@width)':2393
         /\ param0@width:155 = (NewtonDomain.Left param0@width)':2394
         /\ return@width:406 = (NewtonDomain.Left return@width)':2395
         /\ type_err:166 = (NewtonDomain.Left param2@pos)':2396
         /\ type_err:165 = (NewtonDomain.Left param1@pos)':2397
         /\ param0@pos:156 = (NewtonDomain.Left param0@pos)':2398
         /\ return@pos:405 = (NewtonDomain.Left return@pos)':2399
         /\ param1:160 = (NewtonDomain.Left param2)':2400
         /\ 0 = (NewtonDomain.Left param1)':2401
         /\ param0:157 = (NewtonDomain.Left param0)':2402
         /\ return:404 = (NewtonDomain.Left return)':2403
         /\ __cost:106 = (NewtonDomain.Left __cost)':2404)}

================================================
Assertion Checking at Error Points

================================================
Bounds on Variables

Variable bounds at line 28 in start

min((1 + __cost), 3) <= __cost
__cost is o(1)
__cost <= max((1 + __cost), (1 + __cost + (2 * len)))
__cost is O(n)

================================================
Finished!