/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, 71> -> <Unique State Name, 72 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 66> -> <Unique State Name, 56>	Base relation: 
{__cost := (__cost:101 + 1)
 x := param0:80
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}	
<Unique State Name, 80> -> <Unique State Name, 96>	Base relation: 
{return := havoc:102
 return@pos := type_err:105
 return@width := type_err:106}	
<Unique State Name, 25> -> <Unique State Name, 97>	Base relation: 
{return := havoc:63
 return@pos := type_err:66
 return@width := type_err:67}	
<Unique State Name, 93> -> <Unique State Name, 88 92>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 92> -> <Unique State Name, 98>	Base relation: 
{return := 0
 return@pos := type_err:32
 return@width := type_err:33
 when (((0 < x:4 /\ x:4 = phi_tmp___1:23) \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
         /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
               \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}	
<Unique State Name, 94> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 23> -> <Unique State Name, 93>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<Unique State Name, 98> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 81> -> <Unique State Name, 66 80>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 70> -> <Unique State Name, 45>	Base relation: 
{y := return:109}	
<Unique State Name, 64> -> <Unique State Name, 57>	Base relation: 
{}	
<Unique State Name, 77> -> <Unique State Name, 81>	Base relation: 
{y := return:109
 param0 := return:109
 param0@pos := type_err:128
 param0@width := type_err:129}	
<Unique State Name, 87> -> <Unique State Name, 82 86>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 86> -> <Unique State Name, 25>	Base relation: 
{}	
<Unique State Name, 72> -> <Unique State Name, 44>	Base relation: 
{__cost := (__cost:101 + 1)
 x := param0:80
 y := param1:83
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}	
<Unique State Name, 57> -> <Unique State Name, 94>	Base relation: 
{return := havoc:200
 return@pos := type_err:203
 return@width := type_err:204}	
<Unique State Name, 96> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 65> -> <Unique State Name, 66 64>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 56> -> <Unique State Name, 57>	Base relation: 
{when x:199 <= 0}	
<Unique State Name, 56> -> <Unique State Name, 65>	Base relation: 
{x := (x:199 + -1)
 param0 := (x:199 + -1)
 param0@pos := type_err:209
 param0@width := type_err:210
 when 0 < x:199}	
<Unique State Name, 44> -> <Unique State Name, 45>	Base relation: 
{when x:152 <= 0}	
<Unique State Name, 44> -> <Unique State Name, 71>	Base relation: 
{x := (x:152 + -1)
 y := (y:151 + 1)
 param0 := (x:152 + -1)
 param1 := (y:151 + 1)
 param0@pos := type_err:165
 param1@pos := type_err:167
 param0@width := type_err:166
 param1@width := type_err:168
 when 0 < x:152}	
<Unique State Name, 88> -> <Unique State Name, 87>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<Unique State Name, 78> -> <Unique State Name, 72 77>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 45> -> <Unique State Name, 95>	Base relation: 
{return := y:151
 return@pos := type_err:155
 return@width := type_err:156}	
<Unique State Name, 82> -> <Unique State Name, 78>	Base relation: 
{__cost := (__cost:101 + 1)
 y := param1:83
 param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:130
 param1@pos := type_err:131
 param0@width := type_err:132
 param1@width := type_err:133
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}	
<Unique State Name, 95> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 97> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  22  29  37  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       x := havoc:21
       y := havoc:22
       param0 := havoc:21
       param1 := havoc:22
       param0@pos := type_err:27
       param1@pos := type_err:29
       param0@width := type_err:28
       param1@width := type_err:30}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:32
     return@width := type_err:33
     when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
              \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
             /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                   \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:80
       param1 := param1:83
       param0@pos := type_err:88
       param1@pos := type_err:89
       param0@width := type_err:90
       param1@width := type_err:91}    )
    ,
    Var(22)
  )
  ,
  Weight(Base relation: 
    {return := havoc:63
     return@pos := type_err:66
     return@width := type_err:67}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=22: 
Dot(
  Dot(
    Dot(
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           y := param1:83
           param0 := param0:80
           param1 := param1:83
           param0@pos := type_err:130
           param1@pos := type_err:131
           param0@width := type_err:132
           param1@width := type_err:133
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}        )
        ,
        Var(29)
      )
      ,
      Weight(Base relation: 
        {y := return:109
         param0 := return:109
         param0@pos := type_err:128
         param0@width := type_err:129}      )
    )
    ,
    Var(37)
  )
  ,
  Weight(Base relation: 
    {return := havoc:102
     return@pos := type_err:105
     return@width := type_err:106}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=29: 
Dot(
  Plus(
    Weight(Base relation: 
      {__cost := (__cost:101 + 1)
       x := param0:80
       y := param1:83
       when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}    )
    ,
    Dot(
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           x := (param0:80 + -1)
           y := (param1:83 + 1)
           param0 := (param0:80 + -1)
           param1 := (param1:83 + 1)
           param0@pos := type_err:233
           param1@pos := type_err:234
           param0@width := type_err:235
           param1@width := type_err:236
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}        )
        ,
        Var(29)
      )
      ,
      Weight(Base relation: 
        {y := return:109}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := y:151
     return@pos := type_err:155
     return@width := type_err:156}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=37: 
Dot(
  Plus(
    Weight(Base relation: 
      {__cost := (__cost:101 + 1)
       x := param0:80
       when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}    )
    ,
    Dot(
      Weight(Base relation: 
        {__cost := (__cost:101 + 1)
         x := (param0:80 + -1)
         param0 := (param0:80 + -1)
         param0@pos := type_err:237
         param0@width := type_err:238
         when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}      )
      ,
      Var(37)
    )
  )
  ,
  Weight(Base relation: 
    {return := havoc:200
     return@pos := type_err:203
     return@width := type_err:204}  )
)



Performing Gaussian Elimination.


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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         x := havoc:21
         y := havoc:22
         param0 := havoc:21
         param1 := havoc:22
         param0@pos := type_err:27
         param1@pos := type_err:29
         param0@width := type_err:28
         param1@width := type_err:30}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:32
       return@width := type_err:33
       when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
                \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
               /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                     \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:80
         param1 := param1:83
         param0@pos := type_err:88
         param1@pos := type_err:89
         param0@width := type_err:90
         param1@width := type_err:91}      )
      ,
      Var(22)
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)



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

Project(
  Dot(
    Dot(
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := (__cost:101 + 1)
             y := param1:83
             param0 := param0:80
             param1 := param1:83
             param0@pos := type_err:130
             param1@pos := type_err:131
             param0@width := type_err:132
             param1@width := type_err:133
             when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}          )
          ,
          Var(29)
        )
        ,
        Weight(Base relation: 
          {y := return:109
           param0 := return:109
           param0@pos := type_err:128
           param0@width := type_err:129}        )
      )
      ,
      Var(37)
    )
    ,
    Weight(Base relation: 
      {return := havoc:102
       return@pos := type_err:105
       return@width := type_err:106}    )
  )
)



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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:101 + 1)
         x := param0:80
         y := param1:83
         when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := (__cost:101 + 1)
             x := (param0:80 + -1)
             y := (param1:83 + 1)
             param0 := (param0:80 + -1)
             param1 := (param1:83 + 1)
             param0@pos := type_err:233
             param1@pos := type_err:234
             param0@width := type_err:235
             param1@width := type_err:236
             when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}          )
          ,
          Var(29)
        )
        ,
        Weight(Base relation: 
          {y := return:109}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := y:151
       return@pos := type_err:155
       return@width := type_err:156}    )
  )
)



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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:101 + 1)
         x := param0:80
         when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}      )
      ,
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           x := (param0:80 + -1)
           param0 := (param0:80 + -1)
           param0@pos := type_err:237
           param0@width := type_err:238
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}        )
        ,
        Var(37)
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:200
       return@pos := type_err:203
       return@width := type_err:204}    )
  )
)



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         x := havoc:21
         y := havoc:22
         param0 := havoc:21
         param1 := havoc:22
         param0@pos := type_err:27
         param1@pos := type_err:29
         param0@width := type_err:28
         param1@width := type_err:30}      )
      ,
      Project(
        Dot(
          Dot(
            Weight(Base relation: 
              {param0 := param0:80
               param1 := param1:83
               param0@pos := type_err:88
               param1@pos := type_err:89
               param0@width := type_err:90
               param1@width := type_err:91}            )
            ,
            Project(
              Dot(
                Dot(
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {__cost := (__cost:101 + 1)
                         y := param1:83
                         param0 := param0:80
                         param1 := param1:83
                         param0@pos := type_err:130
                         param1@pos := type_err:131
                         param0@width := type_err:132
                         param1@width := type_err:133
                         when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}                      )
                      ,
                      Detensor(
                        Weight(Base relation: 
                          {__cost := (__cost:101 + 1)
                           return := param1:83
                           return@pos := type_err:241
                           return@width := type_err:242
                           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                                   /\ param0:80 <= 0)}                        )
                        ,
                        KleeneT( key=1
                          ProjectT(
                            Tensor(
                              Weight(Base relation: 
                                {__cost := (__cost:101 + 1)
                                 x := (param0:80 + -1)
                                 y := (param1:83 + 1)
                                 param0 := (param0:80 + -1)
                                 param1 := (param1:83 + 1)
                                 param0@pos := type_err:233
                                 param1@pos := type_err:234
                                 param0@width := type_err:235
                                 param1@width := type_err:236
                                 when (0 <= __cost:101
                                         /\ 0 <= (__cost:101 + 1)
                                         /\ 0 < param0:80)}                              )
                              ,
                              Weight(Base relation: 
                                {y := return:109
                                 return := return:109
                                 return@pos := type_err:239
                                 return@width := type_err:240}                              )
                            )
                          )
                        )
                      )
                    )
                    ,
                    Weight(Base relation: 
                      {y := return:109
                       param0 := return:109
                       param0@pos := type_err:128
                       param0@width := type_err:129}                    )
                  )
                  ,
                  Detensor(
                    Weight(Base relation: 
                      {__cost := (__cost:101 + 1)
                       return := havoc:243
                       return@pos := type_err:244
                       return@width := type_err:245
                       when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                               /\ param0:80 <= 0)}                    )
                    ,
                    KleeneT( key=2
                      ProjectT(
                        Tensor(
                          Weight(Base relation: 
                            {__cost := (__cost:101 + 1)
                             x := (param0:80 + -1)
                             param0 := (param0:80 + -1)
                             param0@pos := type_err:237
                             param0@width := type_err:238
                             when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                                     /\ 0 < param0:80)}                          )
                          ,
                          Weight(Base relation: 
                            {return := havoc:200
                             return@pos := type_err:203
                             return@width := type_err:204}                          )
                        )
                      )
                    )
                  )
                )
                ,
                Weight(Base relation: 
                  {return := havoc:102
                   return@pos := type_err:105
                   return@width := type_err:106}                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:63
             return@pos := type_err:66
             return@width := type_err:67}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:32
       return@width := type_err:33
       when (((0 < x:4 /\ x:4 = phi_tmp___1:23)
                \/ (x:4 <= 0 /\ 0 = phi_tmp___1:23))
               /\ ((0 < y:5 /\ y:5 = phi_tmp___2:31)
                     \/ (y:5 <= 0 /\ 0 = phi_tmp___2:31)))}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:80
         param1 := param1:83
         param0@pos := type_err:88
         param1@pos := type_err:89
         param0@width := type_err:90
         param1@width := type_err:91}      )
      ,
      Project(
        Dot(
          Dot(
            Dot(
              Dot(
                Weight(Base relation: 
                  {__cost := (__cost:101 + 1)
                   y := param1:83
                   param0 := param0:80
                   param1 := param1:83
                   param0@pos := type_err:130
                   param1@pos := type_err:131
                   param0@width := type_err:132
                   param1@width := type_err:133
                   when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}                )
                ,
                Detensor(
                  Weight(Base relation: 
                    {__cost := (__cost:101 + 1)
                     return := param1:83
                     return@pos := type_err:241
                     return@width := type_err:242
                     when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                             /\ param0:80 <= 0)}                  )
                  ,
                  KleeneT( key=1
                    ProjectT(
                      Tensor(
                        Weight(Base relation: 
                          {__cost := (__cost:101 + 1)
                           x := (param0:80 + -1)
                           y := (param1:83 + 1)
                           param0 := (param0:80 + -1)
                           param1 := (param1:83 + 1)
                           param0@pos := type_err:233
                           param1@pos := type_err:234
                           param0@width := type_err:235
                           param1@width := type_err:236
                           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                                   /\ 0 < param0:80)}                        )
                        ,
                        Weight(Base relation: 
                          {y := return:109
                           return := return:109
                           return@pos := type_err:239
                           return@width := type_err:240}                        )
                      )
                    )
                  )
                )
              )
              ,
              Weight(Base relation: 
                {y := return:109
                 param0 := return:109
                 param0@pos := type_err:128
                 param0@width := type_err:129}              )
            )
            ,
            Detensor(
              Weight(Base relation: 
                {__cost := (__cost:101 + 1)
                 return := havoc:243
                 return@pos := type_err:244
                 return@width := type_err:245
                 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                         /\ param0:80 <= 0)}              )
              ,
              KleeneT( key=2
                ProjectT(
                  Tensor(
                    Weight(Base relation: 
                      {__cost := (__cost:101 + 1)
                       x := (param0:80 + -1)
                       param0 := (param0:80 + -1)
                       param0@pos := type_err:237
                       param0@width := type_err:238
                       when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                               /\ 0 < param0:80)}                    )
                    ,
                    Weight(Base relation: 
                      {return := havoc:200
                       return@pos := type_err:203
                       return@width := type_err:204}                    )
                  )
                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:102
             return@pos := type_err:105
             return@width := type_err:106}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:63
       return@pos := type_err:66
       return@width := type_err:67}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=22: 
Project(
  Dot(
    Dot(
      Dot(
        Dot(
          Weight(Base relation: 
            {__cost := (__cost:101 + 1)
             y := param1:83
             param0 := param0:80
             param1 := param1:83
             param0@pos := type_err:130
             param1@pos := type_err:131
             param0@width := type_err:132
             param1@width := type_err:133
             when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}          )
          ,
          Detensor(
            Weight(Base relation: 
              {__cost := (__cost:101 + 1)
               return := param1:83
               return@pos := type_err:241
               return@width := type_err:242
               when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                       /\ param0:80 <= 0)}            )
            ,
            KleeneT( key=1
              ProjectT(
                Tensor(
                  Weight(Base relation: 
                    {__cost := (__cost:101 + 1)
                     x := (param0:80 + -1)
                     y := (param1:83 + 1)
                     param0 := (param0:80 + -1)
                     param1 := (param1:83 + 1)
                     param0@pos := type_err:233
                     param1@pos := type_err:234
                     param0@width := type_err:235
                     param1@width := type_err:236
                     when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                             /\ 0 < param0:80)}                  )
                  ,
                  Weight(Base relation: 
                    {y := return:109
                     return := return:109
                     return@pos := type_err:239
                     return@width := type_err:240}                  )
                )
              )
            )
          )
        )
        ,
        Weight(Base relation: 
          {y := return:109
           param0 := return:109
           param0@pos := type_err:128
           param0@width := type_err:129}        )
      )
      ,
      Detensor(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           return := havoc:243
           return@pos := type_err:244
           return@width := type_err:245
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}        )
        ,
        KleeneT( key=2
          ProjectT(
            Tensor(
              Weight(Base relation: 
                {__cost := (__cost:101 + 1)
                 x := (param0:80 + -1)
                 param0 := (param0:80 + -1)
                 param0@pos := type_err:237
                 param0@width := type_err:238
                 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1)
                         /\ 0 < param0:80)}              )
              ,
              Weight(Base relation: 
                {return := havoc:200
                 return@pos := type_err:203
                 return@width := type_err:204}              )
            )
          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:102
       return@pos := type_err:105
       return@width := type_err:106}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=29: 
Detensor(
  Weight(Base relation: 
    {__cost := (__cost:101 + 1)
     return := param1:83
     return@pos := type_err:241
     return@width := type_err:242
     when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}  )
  ,
  KleeneT( key=1
    ProjectT(
      Tensor(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           x := (param0:80 + -1)
           y := (param1:83 + 1)
           param0 := (param0:80 + -1)
           param1 := (param1:83 + 1)
           param0@pos := type_err:233
           param1@pos := type_err:234
           param0@width := type_err:235
           param1@width := type_err:236
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}        )
        ,
        Weight(Base relation: 
          {y := return:109
           return := return:109
           return@pos := type_err:239
           return@width := type_err:240}        )
      )
    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=37: 
Detensor(
  Weight(Base relation: 
    {__cost := (__cost:101 + 1)
     return := havoc:243
     return@pos := type_err:244
     return@width := type_err:245
     when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0)}  )
  ,
  KleeneT( key=2
    ProjectT(
      Tensor(
        Weight(Base relation: 
          {__cost := (__cost:101 + 1)
           x := (param0:80 + -1)
           param0 := (param0:80 + -1)
           param0@pos := type_err:237
           param0@width := type_err:238
           when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}        )
        ,
        Weight(Base relation: 
          {return := havoc:200
           return@pos := type_err:203
           return@width := type_err:204}        )
      )
    )
  )
)


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:246
 (NewtonDomain.Left param0) := fresh_param0:249
 (NewtonDomain.Left param1) := fresh_param1:250
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:251
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:252
 (NewtonDomain.Left param0@width) := fresh_param0@width:253
 (NewtonDomain.Left param1@width) := fresh_param1@width:254
 (NewtonDomain.Right return) := (NewtonDomain.Right return):255
 (NewtonDomain.Right return@pos) := type_err:239
 (NewtonDomain.Right return@width) := type_err:240
 when (0 <= fresh___cost:246 /\ 0 <= (fresh___cost:246 + 1)
         /\ 0 < fresh_param0:249
         /\ (NewtonDomain.Left __cost):256 = (fresh___cost:246 + 1)
         /\ (NewtonDomain.Right x):267 = (fresh_param0:249 + -1)
         /\ (NewtonDomain.Right y):268 = (fresh_param1:250 + 1)
         /\ (NewtonDomain.Left param0):259 = (fresh_param0:249 + -1)
         /\ (NewtonDomain.Left param1):260 = (fresh_param1:250 + 1)
         /\ (NewtonDomain.Left param0@pos):261 = type_err:233
         /\ (NewtonDomain.Left param1@pos):262 = type_err:234
         /\ (NewtonDomain.Left param0@width):263 = type_err:235
         /\ (NewtonDomain.Left param1@width):264 = type_err:236)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':270) = (1)*((NewtonDomain.Left param0):259)
                                                 + 1
           ((NewtonDomain.Left __cost)':269) = (1)*((NewtonDomain.Left __cost):256)
                                                + (-1)*1
           ((NewtonDomain.Left param1)':271) = (1)*((NewtonDomain.Left param1):260)
                                                + (-1)*1
           ((NewtonDomain.Right return)':276) = (1)*((NewtonDomain.Right return):255)
                                                 + 0
           }
          pre:
            [|(NewtonDomain.Left param0):259>=0;
              (NewtonDomain.Left __cost):256-1>=0|]
          post:
            [|(NewtonDomain.Left __cost)':269>=0;
              (NewtonDomain.Left param0)':270-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':269
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':270
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':271
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':272
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':273
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':274
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':275
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':276
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':278
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':280
   when ((!(0 <= K:306)
            \/ mid_(NewtonDomain.Left param0):316 = ((NewtonDomain.Left param0):259
                                                       + K:306))
           /\ (!(0 <= K:306)
                 \/ mid_(NewtonDomain.Left __cost):317 = ((NewtonDomain.Left __cost):256
                                                            + -K:306))
           /\ (!(0 <= K:306)
                 \/ mid_(NewtonDomain.Left param1):315 = ((NewtonDomain.Left param1):260
                                                            + -K:306))
           /\ (!(0 <= K:306)
                 \/ mid_(NewtonDomain.Right return):310 = (NewtonDomain.Right return):255)
           /\ ((K:306 = 0
                  /\ (NewtonDomain.Right return@width):279 = mid_(NewtonDomain.Right return@width):308
                  /\ (NewtonDomain.Right return@pos):277 = mid_(NewtonDomain.Right return@pos):309
                  /\ (NewtonDomain.Right return):255 = mid_(NewtonDomain.Right return):310
                  /\ (NewtonDomain.Left param1@width):264 = mid_(NewtonDomain.Left param1@width):311
                  /\ (NewtonDomain.Left param0@width):263 = mid_(NewtonDomain.Left param0@width):312
                  /\ (NewtonDomain.Left param1@pos):262 = mid_(NewtonDomain.Left param1@pos):313
                  /\ (NewtonDomain.Left param0@pos):261 = mid_(NewtonDomain.Left param0@pos):314
                  /\ (NewtonDomain.Left param1):260 = mid_(NewtonDomain.Left param1):315
                  /\ (NewtonDomain.Left param0):259 = mid_(NewtonDomain.Left param0):316
                  /\ (NewtonDomain.Left __cost):256 = mid_(NewtonDomain.Left __cost):317)
                 \/ (1 <= K:306 /\ 0 <= (NewtonDomain.Left param0):259
                       /\ 0 <= (-1 + (NewtonDomain.Left __cost):256)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):317
                       /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):316)))
           /\ K:307 = 0
           /\ mid_(NewtonDomain.Right return@width):308 = (NewtonDomain.Right return@width)':280
           /\ mid_(NewtonDomain.Right return@pos):309 = (NewtonDomain.Right return@pos)':278
           /\ mid_(NewtonDomain.Right return):310 = (NewtonDomain.Right return)':276
           /\ mid_(NewtonDomain.Left param1@width):311 = (NewtonDomain.Left param1@width)':275
           /\ mid_(NewtonDomain.Left param0@width):312 = (NewtonDomain.Left param0@width)':274
           /\ mid_(NewtonDomain.Left param1@pos):313 = (NewtonDomain.Left param1@pos)':273
           /\ mid_(NewtonDomain.Left param0@pos):314 = (NewtonDomain.Left param0@pos)':272
           /\ mid_(NewtonDomain.Left param1):315 = (NewtonDomain.Left param1)':271
           /\ mid_(NewtonDomain.Left param0):316 = (NewtonDomain.Left param0)':270
           /\ mid_(NewtonDomain.Left __cost):317 = (NewtonDomain.Left __cost)':269
           /\ 0 = K:307 /\ (K:306 + K:307) = K:305 /\ 0 <= K:305)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:385
 (NewtonDomain.Left param0) := fresh_param0:387
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:388
 (NewtonDomain.Left param0@width) := fresh_param0@width:389
 (NewtonDomain.Right return) := havoc:200
 (NewtonDomain.Right return@pos) := type_err:203
 (NewtonDomain.Right return@width) := type_err:204
 when (0 <= fresh___cost:385 /\ 0 <= (fresh___cost:385 + 1)
         /\ 0 < fresh_param0:387
         /\ (NewtonDomain.Left __cost):256 = (fresh___cost:385 + 1)
         /\ (NewtonDomain.Right x):392 = (fresh_param0:387 + -1)
         /\ (NewtonDomain.Left param0):259 = (fresh_param0:387 + -1)
         /\ (NewtonDomain.Left param0@pos):261 = type_err:237
         /\ (NewtonDomain.Left param0@width):263 = type_err:238)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':270) = (1)*((NewtonDomain.Left param0):259)
                                                 + 1
           ((NewtonDomain.Left __cost)':269) = (1)*((NewtonDomain.Left __cost):256)
                                                + (-1)*1
           }
          pre:
            [|(NewtonDomain.Left param0):259>=0;
              (NewtonDomain.Left __cost):256-1>=0|]
          post:
            [|(NewtonDomain.Left __cost)':269>=0;
              (NewtonDomain.Left param0)':270-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':269
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':270
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':272
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':274
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':276
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':278
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':280
   when ((!(0 <= K:410)
            \/ mid_(NewtonDomain.Left param0):417 = ((NewtonDomain.Left param0):259
                                                       + K:410))
           /\ (!(0 <= K:410)
                 \/ mid_(NewtonDomain.Left __cost):418 = ((NewtonDomain.Left __cost):256
                                                            + -K:410))
           /\ ((K:410 = 0
                  /\ (NewtonDomain.Right return@width):279 = mid_(NewtonDomain.Right return@width):412
                  /\ (NewtonDomain.Right return@pos):277 = mid_(NewtonDomain.Right return@pos):413
                  /\ (NewtonDomain.Right return):255 = mid_(NewtonDomain.Right return):414
                  /\ (NewtonDomain.Left param0@width):263 = mid_(NewtonDomain.Left param0@width):415
                  /\ (NewtonDomain.Left param0@pos):261 = mid_(NewtonDomain.Left param0@pos):416
                  /\ (NewtonDomain.Left param0):259 = mid_(NewtonDomain.Left param0):417
                  /\ (NewtonDomain.Left __cost):256 = mid_(NewtonDomain.Left __cost):418)
                 \/ (1 <= K:410 /\ 0 <= (NewtonDomain.Left param0):259
                       /\ 0 <= (-1 + (NewtonDomain.Left __cost):256)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):418
                       /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):417)))
           /\ K:411 = 0
           /\ mid_(NewtonDomain.Right return@width):412 = (NewtonDomain.Right return@width)':280
           /\ mid_(NewtonDomain.Right return@pos):413 = (NewtonDomain.Right return@pos)':278
           /\ mid_(NewtonDomain.Right return):414 = (NewtonDomain.Right return)':276
           /\ mid_(NewtonDomain.Left param0@width):415 = (NewtonDomain.Left param0@width)':274
           /\ mid_(NewtonDomain.Left param0@pos):416 = (NewtonDomain.Left param0@pos)':272
           /\ mid_(NewtonDomain.Left param0):417 = (NewtonDomain.Left param0)':270
           /\ mid_(NewtonDomain.Left __cost):418 = (NewtonDomain.Left __cost)':269
           /\ 0 = K:411 /\ (K:410 + K:411) = K:409 /\ 0 <= K:409)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:571 + 1)
 return := 0
 param0 := fresh_param0:572
 param1 := fresh_param1:541
 return@pos := type_err:602
 param0@pos := fresh_param0@pos:584
 param1@pos := fresh_param1@pos:551
 return@width := type_err:603
 param0@width := fresh_param0@width:582
 param1@width := fresh_param1@width:547
 when (0 <= fresh___cost:535 /\ 0 <= (fresh___cost:535 + 1)
         /\ fresh_param0:536 <= 0
         /\ (!(0 <= K:537)
               \/ mid_(NewtonDomain.Left param0):538 = (fresh_param0:536
                                                          + K:537))
         /\ (!(0 <= K:537)
               \/ mid_(NewtonDomain.Left __cost):539 = (fresh___cost:535
                                                          + -K:537))
         /\ (!(0 <= K:537)
               \/ mid_(NewtonDomain.Left param1):540 = (fresh_param1:541
                                                          + -K:537))
         /\ (!(0 <= K:537)
               \/ mid_(NewtonDomain.Right return):542 = fresh_param1:541)
         /\ ((K:537 = 0
                /\ type_err:543 = mid_(NewtonDomain.Right return@width):544
                /\ type_err:545 = mid_(NewtonDomain.Right return@pos):546
                /\ fresh_param1:541 = mid_(NewtonDomain.Right return):542
                /\ fresh_param1@width:547 = mid_(NewtonDomain.Left param1@width):548
                /\ fresh_param0@width:549 = mid_(NewtonDomain.Left param0@width):550
                /\ fresh_param1@pos:551 = mid_(NewtonDomain.Left param1@pos):552
                /\ fresh_param0@pos:553 = mid_(NewtonDomain.Left param0@pos):554
                /\ fresh_param1:541 = mid_(NewtonDomain.Left param1):540
                /\ fresh_param0:536 = mid_(NewtonDomain.Left param0):538
                /\ fresh___cost:535 = mid_(NewtonDomain.Left __cost):539)
               \/ (1 <= K:537 /\ 0 <= fresh_param0:536
                     /\ 0 <= (-1 + fresh___cost:535)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):539
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):538)))
         /\ K:555 = 0
         /\ mid_(NewtonDomain.Right return@width):544 = (NewtonDomain.Right return@width)':556
         /\ mid_(NewtonDomain.Right return@pos):546 = (NewtonDomain.Right return@pos)':557
         /\ mid_(NewtonDomain.Right return):542 = (NewtonDomain.Right return)':558
         /\ mid_(NewtonDomain.Left param1@width):548 = (NewtonDomain.Left param1@width)':559
         /\ mid_(NewtonDomain.Left param0@width):550 = (NewtonDomain.Left param0@width)':560
         /\ mid_(NewtonDomain.Left param1@pos):552 = (NewtonDomain.Left param1@pos)':561
         /\ mid_(NewtonDomain.Left param0@pos):554 = (NewtonDomain.Left param0@pos)':562
         /\ mid_(NewtonDomain.Left param1):540 = (NewtonDomain.Left param1)':563
         /\ mid_(NewtonDomain.Left param0):538 = (NewtonDomain.Left param0)':564
         /\ mid_(NewtonDomain.Left __cost):539 = (NewtonDomain.Left __cost)':565
         /\ 0 = K:555 /\ (K:537 + K:555) = K:566 /\ 0 <= K:566
         /\ type_err:567 = (NewtonDomain.Left param1@width)':559
         /\ type_err:568 = (NewtonDomain.Left param0@width)':560
         /\ type_err:569 = (NewtonDomain.Left param1@pos)':561
         /\ type_err:570 = (NewtonDomain.Left param0@pos)':562
         /\ havoc:22 = (NewtonDomain.Left param1)':563
         /\ havoc:21 = (NewtonDomain.Left param0)':564
         /\ 1 = (NewtonDomain.Left __cost)':565 /\ 0 <= fresh___cost:571
         /\ 0 <= (fresh___cost:571 + 1) /\ fresh_param0:572 <= 0
         /\ (!(0 <= K:573)
               \/ mid_(NewtonDomain.Left param0):574 = (fresh_param0:572
                                                          + K:573))
         /\ (!(0 <= K:573)
               \/ mid_(NewtonDomain.Left __cost):575 = (fresh___cost:571
                                                          + -K:573))
         /\ ((K:573 = 0
                /\ type_err:576 = mid_(NewtonDomain.Right return@width):577
                /\ type_err:578 = mid_(NewtonDomain.Right return@pos):579
                /\ havoc:580 = mid_(NewtonDomain.Right return):581
                /\ fresh_param0@width:582 = mid_(NewtonDomain.Left param0@width):583
                /\ fresh_param0@pos:584 = mid_(NewtonDomain.Left param0@pos):585
                /\ fresh_param0:572 = mid_(NewtonDomain.Left param0):574
                /\ fresh___cost:571 = mid_(NewtonDomain.Left __cost):575)
               \/ (1 <= K:573 /\ 0 <= fresh_param0:572
                     /\ 0 <= (-1 + fresh___cost:571)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):575
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):574)))
         /\ K:586 = 0
         /\ mid_(NewtonDomain.Right return@width):577 = (NewtonDomain.Right return@width)':587
         /\ mid_(NewtonDomain.Right return@pos):579 = (NewtonDomain.Right return@pos)':588
         /\ mid_(NewtonDomain.Right return):581 = (NewtonDomain.Right return)':589
         /\ mid_(NewtonDomain.Left param0@width):583 = (NewtonDomain.Left param0@width)':590
         /\ mid_(NewtonDomain.Left param0@pos):585 = (NewtonDomain.Left param0@pos)':591
         /\ mid_(NewtonDomain.Left param0):574 = (NewtonDomain.Left param0)':592
         /\ mid_(NewtonDomain.Left __cost):575 = (NewtonDomain.Left __cost)':593
         /\ 0 = K:586 /\ (K:573 + K:586) = K:594 /\ 0 <= K:594
         /\ type_err:595 = (NewtonDomain.Left param0@width)':590
         /\ type_err:596 = (NewtonDomain.Left param0@pos)':591
         /\ (NewtonDomain.Right return)':558 = (NewtonDomain.Left param0)':592
         /\ (fresh___cost:535 + 1) = (NewtonDomain.Left __cost)':593
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:600)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:600))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:601)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:601)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:503 + 1)
 return := havoc:532
 param0 := fresh_param0:504
 param1 := fresh_param1:473
 return@pos := type_err:533
 param0@pos := fresh_param0@pos:516
 param1@pos := fresh_param1@pos:483
 return@width := type_err:534
 param0@width := fresh_param0@width:514
 param1@width := fresh_param1@width:479
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:467
         /\ 0 <= (fresh___cost:467 + 1) /\ fresh_param0:468 <= 0
         /\ (!(0 <= K:469)
               \/ mid_(NewtonDomain.Left param0):470 = (fresh_param0:468
                                                          + K:469))
         /\ (!(0 <= K:469)
               \/ mid_(NewtonDomain.Left __cost):471 = (fresh___cost:467
                                                          + -K:469))
         /\ (!(0 <= K:469)
               \/ mid_(NewtonDomain.Left param1):472 = (fresh_param1:473
                                                          + -K:469))
         /\ (!(0 <= K:469)
               \/ mid_(NewtonDomain.Right return):474 = fresh_param1:473)
         /\ ((K:469 = 0
                /\ type_err:475 = mid_(NewtonDomain.Right return@width):476
                /\ type_err:477 = mid_(NewtonDomain.Right return@pos):478
                /\ fresh_param1:473 = mid_(NewtonDomain.Right return):474
                /\ fresh_param1@width:479 = mid_(NewtonDomain.Left param1@width):480
                /\ fresh_param0@width:481 = mid_(NewtonDomain.Left param0@width):482
                /\ fresh_param1@pos:483 = mid_(NewtonDomain.Left param1@pos):484
                /\ fresh_param0@pos:485 = mid_(NewtonDomain.Left param0@pos):486
                /\ fresh_param1:473 = mid_(NewtonDomain.Left param1):472
                /\ fresh_param0:468 = mid_(NewtonDomain.Left param0):470
                /\ fresh___cost:467 = mid_(NewtonDomain.Left __cost):471)
               \/ (1 <= K:469 /\ 0 <= fresh_param0:468
                     /\ 0 <= (-1 + fresh___cost:467)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):471
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):470)))
         /\ K:487 = 0
         /\ mid_(NewtonDomain.Right return@width):476 = (NewtonDomain.Right return@width)':488
         /\ mid_(NewtonDomain.Right return@pos):478 = (NewtonDomain.Right return@pos)':489
         /\ mid_(NewtonDomain.Right return):474 = (NewtonDomain.Right return)':490
         /\ mid_(NewtonDomain.Left param1@width):480 = (NewtonDomain.Left param1@width)':491
         /\ mid_(NewtonDomain.Left param0@width):482 = (NewtonDomain.Left param0@width)':492
         /\ mid_(NewtonDomain.Left param1@pos):484 = (NewtonDomain.Left param1@pos)':493
         /\ mid_(NewtonDomain.Left param0@pos):486 = (NewtonDomain.Left param0@pos)':494
         /\ mid_(NewtonDomain.Left param1):472 = (NewtonDomain.Left param1)':495
         /\ mid_(NewtonDomain.Left param0):470 = (NewtonDomain.Left param0)':496
         /\ mid_(NewtonDomain.Left __cost):471 = (NewtonDomain.Left __cost)':497
         /\ 0 = K:487 /\ (K:469 + K:487) = K:498 /\ 0 <= K:498
         /\ type_err:499 = (NewtonDomain.Left param1@width)':491
         /\ type_err:500 = (NewtonDomain.Left param0@width)':492
         /\ type_err:501 = (NewtonDomain.Left param1@pos)':493
         /\ type_err:502 = (NewtonDomain.Left param0@pos)':494
         /\ param1:83 = (NewtonDomain.Left param1)':495
         /\ param0:80 = (NewtonDomain.Left param0)':496
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':497
         /\ 0 <= fresh___cost:503 /\ 0 <= (fresh___cost:503 + 1)
         /\ fresh_param0:504 <= 0
         /\ (!(0 <= K:505)
               \/ mid_(NewtonDomain.Left param0):506 = (fresh_param0:504
                                                          + K:505))
         /\ (!(0 <= K:505)
               \/ mid_(NewtonDomain.Left __cost):507 = (fresh___cost:503
                                                          + -K:505))
         /\ ((K:505 = 0
                /\ type_err:508 = mid_(NewtonDomain.Right return@width):509
                /\ type_err:510 = mid_(NewtonDomain.Right return@pos):511
                /\ havoc:512 = mid_(NewtonDomain.Right return):513
                /\ fresh_param0@width:514 = mid_(NewtonDomain.Left param0@width):515
                /\ fresh_param0@pos:516 = mid_(NewtonDomain.Left param0@pos):517
                /\ fresh_param0:504 = mid_(NewtonDomain.Left param0):506
                /\ fresh___cost:503 = mid_(NewtonDomain.Left __cost):507)
               \/ (1 <= K:505 /\ 0 <= fresh_param0:504
                     /\ 0 <= (-1 + fresh___cost:503)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):507
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):506)))
         /\ K:518 = 0
         /\ mid_(NewtonDomain.Right return@width):509 = (NewtonDomain.Right return@width)':519
         /\ mid_(NewtonDomain.Right return@pos):511 = (NewtonDomain.Right return@pos)':520
         /\ mid_(NewtonDomain.Right return):513 = (NewtonDomain.Right return)':521
         /\ mid_(NewtonDomain.Left param0@width):515 = (NewtonDomain.Left param0@width)':522
         /\ mid_(NewtonDomain.Left param0@pos):517 = (NewtonDomain.Left param0@pos)':523
         /\ mid_(NewtonDomain.Left param0):506 = (NewtonDomain.Left param0)':524
         /\ mid_(NewtonDomain.Left __cost):507 = (NewtonDomain.Left __cost)':525
         /\ 0 = K:518 /\ (K:505 + K:518) = K:526 /\ 0 <= K:526
         /\ type_err:527 = (NewtonDomain.Left param0@width)':522
         /\ type_err:528 = (NewtonDomain.Left param0@pos)':523
         /\ (NewtonDomain.Right return)':490 = (NewtonDomain.Left param0)':524
         /\ (fresh___cost:467 + 1) = (NewtonDomain.Left __cost)':525)}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:440 + 1)
 return := havoc:464
 param0 := fresh_param0:441
 param1 := fresh_param1:357
 return@pos := type_err:465
 param0@pos := fresh_param0@pos:453
 param1@pos := fresh_param1@pos:367
 return@width := type_err:466
 param0@width := fresh_param0@width:451
 param1@width := fresh_param1@width:363
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:351
         /\ 0 <= (fresh___cost:351 + 1) /\ fresh_param0:352 <= 0
         /\ (!(0 <= K:353)
               \/ mid_(NewtonDomain.Left param0):354 = (fresh_param0:352
                                                          + K:353))
         /\ (!(0 <= K:353)
               \/ mid_(NewtonDomain.Left __cost):355 = (fresh___cost:351
                                                          + -K:353))
         /\ (!(0 <= K:353)
               \/ mid_(NewtonDomain.Left param1):356 = (fresh_param1:357
                                                          + -K:353))
         /\ (!(0 <= K:353)
               \/ mid_(NewtonDomain.Right return):358 = fresh_param1:357)
         /\ ((K:353 = 0
                /\ type_err:359 = mid_(NewtonDomain.Right return@width):360
                /\ type_err:361 = mid_(NewtonDomain.Right return@pos):362
                /\ fresh_param1:357 = mid_(NewtonDomain.Right return):358
                /\ fresh_param1@width:363 = mid_(NewtonDomain.Left param1@width):364
                /\ fresh_param0@width:365 = mid_(NewtonDomain.Left param0@width):366
                /\ fresh_param1@pos:367 = mid_(NewtonDomain.Left param1@pos):368
                /\ fresh_param0@pos:369 = mid_(NewtonDomain.Left param0@pos):370
                /\ fresh_param1:357 = mid_(NewtonDomain.Left param1):356
                /\ fresh_param0:352 = mid_(NewtonDomain.Left param0):354
                /\ fresh___cost:351 = mid_(NewtonDomain.Left __cost):355)
               \/ (1 <= K:353 /\ 0 <= fresh_param0:352
                     /\ 0 <= (-1 + fresh___cost:351)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):355
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):354)))
         /\ K:371 = 0
         /\ mid_(NewtonDomain.Right return@width):360 = (NewtonDomain.Right return@width)':372
         /\ mid_(NewtonDomain.Right return@pos):362 = (NewtonDomain.Right return@pos)':373
         /\ mid_(NewtonDomain.Right return):358 = (NewtonDomain.Right return)':374
         /\ mid_(NewtonDomain.Left param1@width):364 = (NewtonDomain.Left param1@width)':375
         /\ mid_(NewtonDomain.Left param0@width):366 = (NewtonDomain.Left param0@width)':376
         /\ mid_(NewtonDomain.Left param1@pos):368 = (NewtonDomain.Left param1@pos)':377
         /\ mid_(NewtonDomain.Left param0@pos):370 = (NewtonDomain.Left param0@pos)':378
         /\ mid_(NewtonDomain.Left param1):356 = (NewtonDomain.Left param1)':379
         /\ mid_(NewtonDomain.Left param0):354 = (NewtonDomain.Left param0)':380
         /\ mid_(NewtonDomain.Left __cost):355 = (NewtonDomain.Left __cost)':381
         /\ 0 = K:371 /\ (K:353 + K:371) = K:382 /\ 0 <= K:382
         /\ type_err:133 = (NewtonDomain.Left param1@width)':375
         /\ type_err:132 = (NewtonDomain.Left param0@width)':376
         /\ type_err:131 = (NewtonDomain.Left param1@pos)':377
         /\ type_err:130 = (NewtonDomain.Left param0@pos)':378
         /\ param1:83 = (NewtonDomain.Left param1)':379
         /\ param0:80 = (NewtonDomain.Left param0)':380
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':381
         /\ 0 <= fresh___cost:440 /\ 0 <= (fresh___cost:440 + 1)
         /\ fresh_param0:441 <= 0
         /\ (!(0 <= K:442)
               \/ mid_(NewtonDomain.Left param0):443 = (fresh_param0:441
                                                          + K:442))
         /\ (!(0 <= K:442)
               \/ mid_(NewtonDomain.Left __cost):444 = (fresh___cost:440
                                                          + -K:442))
         /\ ((K:442 = 0
                /\ type_err:445 = mid_(NewtonDomain.Right return@width):446
                /\ type_err:447 = mid_(NewtonDomain.Right return@pos):448
                /\ havoc:449 = mid_(NewtonDomain.Right return):450
                /\ fresh_param0@width:451 = mid_(NewtonDomain.Left param0@width):452
                /\ fresh_param0@pos:453 = mid_(NewtonDomain.Left param0@pos):454
                /\ fresh_param0:441 = mid_(NewtonDomain.Left param0):443
                /\ fresh___cost:440 = mid_(NewtonDomain.Left __cost):444)
               \/ (1 <= K:442 /\ 0 <= fresh_param0:441
                     /\ 0 <= (-1 + fresh___cost:440)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):444
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):443)))
         /\ K:455 = 0
         /\ mid_(NewtonDomain.Right return@width):446 = (NewtonDomain.Right return@width)':456
         /\ mid_(NewtonDomain.Right return@pos):448 = (NewtonDomain.Right return@pos)':457
         /\ mid_(NewtonDomain.Right return):450 = (NewtonDomain.Right return)':458
         /\ mid_(NewtonDomain.Left param0@width):452 = (NewtonDomain.Left param0@width)':459
         /\ mid_(NewtonDomain.Left param0@pos):454 = (NewtonDomain.Left param0@pos)':460
         /\ mid_(NewtonDomain.Left param0):443 = (NewtonDomain.Left param0)':461
         /\ mid_(NewtonDomain.Left __cost):444 = (NewtonDomain.Left __cost)':462
         /\ 0 = K:455 /\ (K:442 + K:455) = K:463 /\ 0 <= K:463
         /\ type_err:384 = (NewtonDomain.Left param0@width)':459
         /\ type_err:383 = (NewtonDomain.Left param0@pos)':460
         /\ (NewtonDomain.Right return)':374 = (NewtonDomain.Left param0)':461
         /\ (fresh___cost:351 + 1) = (NewtonDomain.Left __cost)':462)}

Evaluating variable number 29 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:344 + 1)
 return := (NewtonDomain.Right return)':335
 param0 := fresh_param0:345
 param1 := fresh_param1:346
 return@pos := (NewtonDomain.Right return@pos)':334
 param0@pos := fresh_param0@pos:347
 param1@pos := fresh_param1@pos:348
 return@width := (NewtonDomain.Right return@width)':333
 param0@width := fresh_param0@width:349
 param1@width := fresh_param1@width:350
 when (0 <= fresh___cost:344 /\ 0 <= (fresh___cost:344 + 1)
         /\ fresh_param0:345 <= 0
         /\ (!(0 <= K:321)
               \/ mid_(NewtonDomain.Left param0):322 = (fresh_param0:345
                                                          + K:321))
         /\ (!(0 <= K:321)
               \/ mid_(NewtonDomain.Left __cost):323 = (fresh___cost:344
                                                          + -K:321))
         /\ (!(0 <= K:321)
               \/ mid_(NewtonDomain.Left param1):324 = (fresh_param1:346
                                                          + -K:321))
         /\ (!(0 <= K:321)
               \/ mid_(NewtonDomain.Right return):325 = fresh_param1:346)
         /\ ((K:321 = 0
                /\ type_err:242 = mid_(NewtonDomain.Right return@width):326
                /\ type_err:241 = mid_(NewtonDomain.Right return@pos):327
                /\ fresh_param1:346 = mid_(NewtonDomain.Right return):325
                /\ fresh_param1@width:350 = mid_(NewtonDomain.Left param1@width):328
                /\ fresh_param0@width:349 = mid_(NewtonDomain.Left param0@width):329
                /\ fresh_param1@pos:348 = mid_(NewtonDomain.Left param1@pos):330
                /\ fresh_param0@pos:347 = mid_(NewtonDomain.Left param0@pos):331
                /\ fresh_param1:346 = mid_(NewtonDomain.Left param1):324
                /\ fresh_param0:345 = mid_(NewtonDomain.Left param0):322
                /\ fresh___cost:344 = mid_(NewtonDomain.Left __cost):323)
               \/ (1 <= K:321 /\ 0 <= fresh_param0:345
                     /\ 0 <= (-1 + fresh___cost:344)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):323
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):322)))
         /\ K:332 = 0
         /\ mid_(NewtonDomain.Right return@width):326 = (NewtonDomain.Right return@width)':333
         /\ mid_(NewtonDomain.Right return@pos):327 = (NewtonDomain.Right return@pos)':334
         /\ mid_(NewtonDomain.Right return):325 = (NewtonDomain.Right return)':335
         /\ mid_(NewtonDomain.Left param1@width):328 = (NewtonDomain.Left param1@width)':336
         /\ mid_(NewtonDomain.Left param0@width):329 = (NewtonDomain.Left param0@width)':337
         /\ mid_(NewtonDomain.Left param1@pos):330 = (NewtonDomain.Left param1@pos)':338
         /\ mid_(NewtonDomain.Left param0@pos):331 = (NewtonDomain.Left param0@pos)':339
         /\ mid_(NewtonDomain.Left param1):324 = (NewtonDomain.Left param1)':340
         /\ mid_(NewtonDomain.Left param0):322 = (NewtonDomain.Left param0)':341
         /\ mid_(NewtonDomain.Left __cost):323 = (NewtonDomain.Left __cost)':342
         /\ 0 = K:332 /\ (K:321 + K:332) = K:343 /\ 0 <= K:343
         /\ param1@width:81 = (NewtonDomain.Left param1@width)':336
         /\ param0@width:78 = (NewtonDomain.Left param0@width)':337
         /\ param1@pos:82 = (NewtonDomain.Left param1@pos)':338
         /\ param0@pos:79 = (NewtonDomain.Left param0@pos)':339
         /\ param1:83 = (NewtonDomain.Left param1)':340
         /\ param0:80 = (NewtonDomain.Left param0)':341
         /\ __cost:101 = (NewtonDomain.Left __cost)':342)}

Evaluating variable number 37 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:436 + 1)
 return := (NewtonDomain.Right return)':430
 param0 := fresh_param0:437
 return@pos := (NewtonDomain.Right return@pos)':429
 param0@pos := fresh_param0@pos:438
 return@width := (NewtonDomain.Right return@width)':428
 param0@width := fresh_param0@width:439
 when (0 <= fresh___cost:436 /\ 0 <= (fresh___cost:436 + 1)
         /\ fresh_param0:437 <= 0
         /\ (!(0 <= K:419)
               \/ mid_(NewtonDomain.Left param0):420 = (fresh_param0:437
                                                          + K:419))
         /\ (!(0 <= K:419)
               \/ mid_(NewtonDomain.Left __cost):421 = (fresh___cost:436
                                                          + -K:419))
         /\ ((K:419 = 0
                /\ type_err:245 = mid_(NewtonDomain.Right return@width):422
                /\ type_err:244 = mid_(NewtonDomain.Right return@pos):423
                /\ havoc:243 = mid_(NewtonDomain.Right return):424
                /\ fresh_param0@width:439 = mid_(NewtonDomain.Left param0@width):425
                /\ fresh_param0@pos:438 = mid_(NewtonDomain.Left param0@pos):426
                /\ fresh_param0:437 = mid_(NewtonDomain.Left param0):420
                /\ fresh___cost:436 = mid_(NewtonDomain.Left __cost):421)
               \/ (1 <= K:419 /\ 0 <= fresh_param0:437
                     /\ 0 <= (-1 + fresh___cost:436)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):421
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):420)))
         /\ K:427 = 0
         /\ mid_(NewtonDomain.Right return@width):422 = (NewtonDomain.Right return@width)':428
         /\ mid_(NewtonDomain.Right return@pos):423 = (NewtonDomain.Right return@pos)':429
         /\ mid_(NewtonDomain.Right return):424 = (NewtonDomain.Right return)':430
         /\ mid_(NewtonDomain.Left param0@width):425 = (NewtonDomain.Left param0@width)':431
         /\ mid_(NewtonDomain.Left param0@pos):426 = (NewtonDomain.Left param0@pos)':432
         /\ mid_(NewtonDomain.Left param0):420 = (NewtonDomain.Left param0)':433
         /\ mid_(NewtonDomain.Left __cost):421 = (NewtonDomain.Left __cost)':434
         /\ 0 = K:427 /\ (K:419 + K:427) = K:435 /\ 0 <= K:435
         /\ param0@width:78 = (NewtonDomain.Left param0@width)':431
         /\ param0@pos:79 = (NewtonDomain.Left param0@pos)':432
         /\ param0:80 = (NewtonDomain.Left param0)':433
         /\ __cost:101 = (NewtonDomain.Left __cost)':434)}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> First round; nothing to compare against; continuing loop.
-------------------------------------------------------------------------------
Round 1:
Evaluating variable number 6 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:604
 (NewtonDomain.Left param0) := fresh_param0:607
 (NewtonDomain.Left param1) := fresh_param1:608
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:609
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:610
 (NewtonDomain.Left param0@width) := fresh_param0@width:611
 (NewtonDomain.Left param1@width) := fresh_param1@width:612
 (NewtonDomain.Right return) := (NewtonDomain.Right return):255
 (NewtonDomain.Right return@pos) := type_err:239
 (NewtonDomain.Right return@width) := type_err:240
 when (0 <= fresh___cost:604 /\ 0 <= (fresh___cost:604 + 1)
         /\ 0 < fresh_param0:607
         /\ (NewtonDomain.Left __cost):256 = (fresh___cost:604 + 1)
         /\ (NewtonDomain.Right x):613 = (fresh_param0:607 + -1)
         /\ (NewtonDomain.Right y):614 = (fresh_param1:608 + 1)
         /\ (NewtonDomain.Left param0):259 = (fresh_param0:607 + -1)
         /\ (NewtonDomain.Left param1):260 = (fresh_param1:608 + 1)
         /\ (NewtonDomain.Left param0@pos):261 = type_err:233
         /\ (NewtonDomain.Left param1@pos):262 = type_err:234
         /\ (NewtonDomain.Left param0@width):263 = type_err:235
         /\ (NewtonDomain.Left param1@width):264 = type_err:236)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':270) = (1)*((NewtonDomain.Left param0):259)
                                                 + 1
           ((NewtonDomain.Left __cost)':269) = (1)*((NewtonDomain.Left __cost):256)
                                                + (-1)*1
           ((NewtonDomain.Left param1)':271) = (1)*((NewtonDomain.Left param1):260)
                                                + (-1)*1
           ((NewtonDomain.Right return)':276) = (1)*((NewtonDomain.Right return):255)
                                                 + 0
           }
          pre:
            [|(NewtonDomain.Left param0):259>=0;
              (NewtonDomain.Left __cost):256-1>=0|]
          post:
            [|(NewtonDomain.Left __cost)':269>=0;
              (NewtonDomain.Left param0)':270-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':269
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':270
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':271
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':272
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':273
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':274
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':275
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':276
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':278
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':280
   when ((!(0 <= K:640)
            \/ mid_(NewtonDomain.Left param0):650 = ((NewtonDomain.Left param0):259
                                                       + K:640))
           /\ (!(0 <= K:640)
                 \/ mid_(NewtonDomain.Left __cost):651 = ((NewtonDomain.Left __cost):256
                                                            + -K:640))
           /\ (!(0 <= K:640)
                 \/ mid_(NewtonDomain.Left param1):649 = ((NewtonDomain.Left param1):260
                                                            + -K:640))
           /\ (!(0 <= K:640)
                 \/ mid_(NewtonDomain.Right return):644 = (NewtonDomain.Right return):255)
           /\ ((K:640 = 0
                  /\ (NewtonDomain.Right return@width):279 = mid_(NewtonDomain.Right return@width):642
                  /\ (NewtonDomain.Right return@pos):277 = mid_(NewtonDomain.Right return@pos):643
                  /\ (NewtonDomain.Right return):255 = mid_(NewtonDomain.Right return):644
                  /\ (NewtonDomain.Left param1@width):264 = mid_(NewtonDomain.Left param1@width):645
                  /\ (NewtonDomain.Left param0@width):263 = mid_(NewtonDomain.Left param0@width):646
                  /\ (NewtonDomain.Left param1@pos):262 = mid_(NewtonDomain.Left param1@pos):647
                  /\ (NewtonDomain.Left param0@pos):261 = mid_(NewtonDomain.Left param0@pos):648
                  /\ (NewtonDomain.Left param1):260 = mid_(NewtonDomain.Left param1):649
                  /\ (NewtonDomain.Left param0):259 = mid_(NewtonDomain.Left param0):650
                  /\ (NewtonDomain.Left __cost):256 = mid_(NewtonDomain.Left __cost):651)
                 \/ (1 <= K:640 /\ 0 <= (NewtonDomain.Left param0):259
                       /\ 0 <= (-1 + (NewtonDomain.Left __cost):256)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):651
                       /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):650)))
           /\ K:641 = 0
           /\ mid_(NewtonDomain.Right return@width):642 = (NewtonDomain.Right return@width)':280
           /\ mid_(NewtonDomain.Right return@pos):643 = (NewtonDomain.Right return@pos)':278
           /\ mid_(NewtonDomain.Right return):644 = (NewtonDomain.Right return)':276
           /\ mid_(NewtonDomain.Left param1@width):645 = (NewtonDomain.Left param1@width)':275
           /\ mid_(NewtonDomain.Left param0@width):646 = (NewtonDomain.Left param0@width)':274
           /\ mid_(NewtonDomain.Left param1@pos):647 = (NewtonDomain.Left param1@pos)':273
           /\ mid_(NewtonDomain.Left param0@pos):648 = (NewtonDomain.Left param0@pos)':272
           /\ mid_(NewtonDomain.Left param1):649 = (NewtonDomain.Left param1)':271
           /\ mid_(NewtonDomain.Left param0):650 = (NewtonDomain.Left param0)':270
           /\ mid_(NewtonDomain.Left __cost):651 = (NewtonDomain.Left __cost)':269
           /\ 0 = K:641 /\ (K:640 + K:641) = K:639 /\ 0 <= K:639)}
}
(Not performing widening.)
alphaHatStar {
**** body value: Tensored relation: 
{(NewtonDomain.Left __cost) := fresh___cost:716
 (NewtonDomain.Left param0) := fresh_param0:718
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:719
 (NewtonDomain.Left param0@width) := fresh_param0@width:720
 (NewtonDomain.Right return) := havoc:200
 (NewtonDomain.Right return@pos) := type_err:203
 (NewtonDomain.Right return@width) := type_err:204
 when (0 <= fresh___cost:716 /\ 0 <= (fresh___cost:716 + 1)
         /\ 0 < fresh_param0:718
         /\ (NewtonDomain.Left __cost):256 = (fresh___cost:716 + 1)
         /\ (NewtonDomain.Right x):721 = (fresh_param0:718 + -1)
         /\ (NewtonDomain.Left param0):259 = (fresh_param0:718 + -1)
         /\ (NewtonDomain.Left param0@pos):261 = type_err:237
         /\ (NewtonDomain.Left param0@width):263 = type_err:238)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':270) = (1)*((NewtonDomain.Left param0):259)
                                                 + 1
           ((NewtonDomain.Left __cost)':269) = (1)*((NewtonDomain.Left __cost):256)
                                                + (-1)*1
           }
          pre:
            [|(NewtonDomain.Left param0):259>=0;
              (NewtonDomain.Left __cost):256-1>=0|]
          post:
            [|(NewtonDomain.Left __cost)':269>=0;
              (NewtonDomain.Left param0)':270-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':269
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':270
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':272
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':274
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':276
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':278
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':280
   when ((!(0 <= K:739)
            \/ mid_(NewtonDomain.Left param0):746 = ((NewtonDomain.Left param0):259
                                                       + K:739))
           /\ (!(0 <= K:739)
                 \/ mid_(NewtonDomain.Left __cost):747 = ((NewtonDomain.Left __cost):256
                                                            + -K:739))
           /\ ((K:739 = 0
                  /\ (NewtonDomain.Right return@width):279 = mid_(NewtonDomain.Right return@width):741
                  /\ (NewtonDomain.Right return@pos):277 = mid_(NewtonDomain.Right return@pos):742
                  /\ (NewtonDomain.Right return):255 = mid_(NewtonDomain.Right return):743
                  /\ (NewtonDomain.Left param0@width):263 = mid_(NewtonDomain.Left param0@width):744
                  /\ (NewtonDomain.Left param0@pos):261 = mid_(NewtonDomain.Left param0@pos):745
                  /\ (NewtonDomain.Left param0):259 = mid_(NewtonDomain.Left param0):746
                  /\ (NewtonDomain.Left __cost):256 = mid_(NewtonDomain.Left __cost):747)
                 \/ (1 <= K:739 /\ 0 <= (NewtonDomain.Left param0):259
                       /\ 0 <= (-1 + (NewtonDomain.Left __cost):256)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):747
                       /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):746)))
           /\ K:740 = 0
           /\ mid_(NewtonDomain.Right return@width):741 = (NewtonDomain.Right return@width)':280
           /\ mid_(NewtonDomain.Right return@pos):742 = (NewtonDomain.Right return@pos)':278
           /\ mid_(NewtonDomain.Right return):743 = (NewtonDomain.Right return)':276
           /\ mid_(NewtonDomain.Left param0@width):744 = (NewtonDomain.Left param0@width)':274
           /\ mid_(NewtonDomain.Left param0@pos):745 = (NewtonDomain.Left param0@pos)':272
           /\ mid_(NewtonDomain.Left param0):746 = (NewtonDomain.Left param0)':270
           /\ mid_(NewtonDomain.Left __cost):747 = (NewtonDomain.Left __cost)':269
           /\ 0 = K:740 /\ (K:739 + K:740) = K:738 /\ 0 <= K:738)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:900 + 1)
 return := 0
 param0 := fresh_param0:901
 param1 := fresh_param1:870
 return@pos := type_err:931
 param0@pos := fresh_param0@pos:913
 param1@pos := fresh_param1@pos:880
 return@width := type_err:932
 param0@width := fresh_param0@width:911
 param1@width := fresh_param1@width:876
 when (0 <= fresh___cost:864 /\ 0 <= (fresh___cost:864 + 1)
         /\ fresh_param0:865 <= 0
         /\ (!(0 <= K:866)
               \/ mid_(NewtonDomain.Left param0):867 = (fresh_param0:865
                                                          + K:866))
         /\ (!(0 <= K:866)
               \/ mid_(NewtonDomain.Left __cost):868 = (fresh___cost:864
                                                          + -K:866))
         /\ (!(0 <= K:866)
               \/ mid_(NewtonDomain.Left param1):869 = (fresh_param1:870
                                                          + -K:866))
         /\ (!(0 <= K:866)
               \/ mid_(NewtonDomain.Right return):871 = fresh_param1:870)
         /\ ((K:866 = 0
                /\ type_err:872 = mid_(NewtonDomain.Right return@width):873
                /\ type_err:874 = mid_(NewtonDomain.Right return@pos):875
                /\ fresh_param1:870 = mid_(NewtonDomain.Right return):871
                /\ fresh_param1@width:876 = mid_(NewtonDomain.Left param1@width):877
                /\ fresh_param0@width:878 = mid_(NewtonDomain.Left param0@width):879
                /\ fresh_param1@pos:880 = mid_(NewtonDomain.Left param1@pos):881
                /\ fresh_param0@pos:882 = mid_(NewtonDomain.Left param0@pos):883
                /\ fresh_param1:870 = mid_(NewtonDomain.Left param1):869
                /\ fresh_param0:865 = mid_(NewtonDomain.Left param0):867
                /\ fresh___cost:864 = mid_(NewtonDomain.Left __cost):868)
               \/ (1 <= K:866 /\ 0 <= fresh_param0:865
                     /\ 0 <= (-1 + fresh___cost:864)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):868
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):867)))
         /\ K:884 = 0
         /\ mid_(NewtonDomain.Right return@width):873 = (NewtonDomain.Right return@width)':885
         /\ mid_(NewtonDomain.Right return@pos):875 = (NewtonDomain.Right return@pos)':886
         /\ mid_(NewtonDomain.Right return):871 = (NewtonDomain.Right return)':887
         /\ mid_(NewtonDomain.Left param1@width):877 = (NewtonDomain.Left param1@width)':888
         /\ mid_(NewtonDomain.Left param0@width):879 = (NewtonDomain.Left param0@width)':889
         /\ mid_(NewtonDomain.Left param1@pos):881 = (NewtonDomain.Left param1@pos)':890
         /\ mid_(NewtonDomain.Left param0@pos):883 = (NewtonDomain.Left param0@pos)':891
         /\ mid_(NewtonDomain.Left param1):869 = (NewtonDomain.Left param1)':892
         /\ mid_(NewtonDomain.Left param0):867 = (NewtonDomain.Left param0)':893
         /\ mid_(NewtonDomain.Left __cost):868 = (NewtonDomain.Left __cost)':894
         /\ 0 = K:884 /\ (K:866 + K:884) = K:895 /\ 0 <= K:895
         /\ type_err:896 = (NewtonDomain.Left param1@width)':888
         /\ type_err:897 = (NewtonDomain.Left param0@width)':889
         /\ type_err:898 = (NewtonDomain.Left param1@pos)':890
         /\ type_err:899 = (NewtonDomain.Left param0@pos)':891
         /\ havoc:22 = (NewtonDomain.Left param1)':892
         /\ havoc:21 = (NewtonDomain.Left param0)':893
         /\ 1 = (NewtonDomain.Left __cost)':894 /\ 0 <= fresh___cost:900
         /\ 0 <= (fresh___cost:900 + 1) /\ fresh_param0:901 <= 0
         /\ (!(0 <= K:902)
               \/ mid_(NewtonDomain.Left param0):903 = (fresh_param0:901
                                                          + K:902))
         /\ (!(0 <= K:902)
               \/ mid_(NewtonDomain.Left __cost):904 = (fresh___cost:900
                                                          + -K:902))
         /\ ((K:902 = 0
                /\ type_err:905 = mid_(NewtonDomain.Right return@width):906
                /\ type_err:907 = mid_(NewtonDomain.Right return@pos):908
                /\ havoc:909 = mid_(NewtonDomain.Right return):910
                /\ fresh_param0@width:911 = mid_(NewtonDomain.Left param0@width):912
                /\ fresh_param0@pos:913 = mid_(NewtonDomain.Left param0@pos):914
                /\ fresh_param0:901 = mid_(NewtonDomain.Left param0):903
                /\ fresh___cost:900 = mid_(NewtonDomain.Left __cost):904)
               \/ (1 <= K:902 /\ 0 <= fresh_param0:901
                     /\ 0 <= (-1 + fresh___cost:900)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):904
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):903)))
         /\ K:915 = 0
         /\ mid_(NewtonDomain.Right return@width):906 = (NewtonDomain.Right return@width)':916
         /\ mid_(NewtonDomain.Right return@pos):908 = (NewtonDomain.Right return@pos)':917
         /\ mid_(NewtonDomain.Right return):910 = (NewtonDomain.Right return)':918
         /\ mid_(NewtonDomain.Left param0@width):912 = (NewtonDomain.Left param0@width)':919
         /\ mid_(NewtonDomain.Left param0@pos):914 = (NewtonDomain.Left param0@pos)':920
         /\ mid_(NewtonDomain.Left param0):903 = (NewtonDomain.Left param0)':921
         /\ mid_(NewtonDomain.Left __cost):904 = (NewtonDomain.Left __cost)':922
         /\ 0 = K:915 /\ (K:902 + K:915) = K:923 /\ 0 <= K:923
         /\ type_err:924 = (NewtonDomain.Left param0@width)':919
         /\ type_err:925 = (NewtonDomain.Left param0@pos)':920
         /\ (NewtonDomain.Right return)':887 = (NewtonDomain.Left param0)':921
         /\ (fresh___cost:864 + 1) = (NewtonDomain.Left __cost)':922
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:929)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:929))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:930)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:930)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:832 + 1)
 return := havoc:861
 param0 := fresh_param0:833
 param1 := fresh_param1:802
 return@pos := type_err:862
 param0@pos := fresh_param0@pos:845
 param1@pos := fresh_param1@pos:812
 return@width := type_err:863
 param0@width := fresh_param0@width:843
 param1@width := fresh_param1@width:808
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:796
         /\ 0 <= (fresh___cost:796 + 1) /\ fresh_param0:797 <= 0
         /\ (!(0 <= K:798)
               \/ mid_(NewtonDomain.Left param0):799 = (fresh_param0:797
                                                          + K:798))
         /\ (!(0 <= K:798)
               \/ mid_(NewtonDomain.Left __cost):800 = (fresh___cost:796
                                                          + -K:798))
         /\ (!(0 <= K:798)
               \/ mid_(NewtonDomain.Left param1):801 = (fresh_param1:802
                                                          + -K:798))
         /\ (!(0 <= K:798)
               \/ mid_(NewtonDomain.Right return):803 = fresh_param1:802)
         /\ ((K:798 = 0
                /\ type_err:804 = mid_(NewtonDomain.Right return@width):805
                /\ type_err:806 = mid_(NewtonDomain.Right return@pos):807
                /\ fresh_param1:802 = mid_(NewtonDomain.Right return):803
                /\ fresh_param1@width:808 = mid_(NewtonDomain.Left param1@width):809
                /\ fresh_param0@width:810 = mid_(NewtonDomain.Left param0@width):811
                /\ fresh_param1@pos:812 = mid_(NewtonDomain.Left param1@pos):813
                /\ fresh_param0@pos:814 = mid_(NewtonDomain.Left param0@pos):815
                /\ fresh_param1:802 = mid_(NewtonDomain.Left param1):801
                /\ fresh_param0:797 = mid_(NewtonDomain.Left param0):799
                /\ fresh___cost:796 = mid_(NewtonDomain.Left __cost):800)
               \/ (1 <= K:798 /\ 0 <= fresh_param0:797
                     /\ 0 <= (-1 + fresh___cost:796)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):800
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):799)))
         /\ K:816 = 0
         /\ mid_(NewtonDomain.Right return@width):805 = (NewtonDomain.Right return@width)':817
         /\ mid_(NewtonDomain.Right return@pos):807 = (NewtonDomain.Right return@pos)':818
         /\ mid_(NewtonDomain.Right return):803 = (NewtonDomain.Right return)':819
         /\ mid_(NewtonDomain.Left param1@width):809 = (NewtonDomain.Left param1@width)':820
         /\ mid_(NewtonDomain.Left param0@width):811 = (NewtonDomain.Left param0@width)':821
         /\ mid_(NewtonDomain.Left param1@pos):813 = (NewtonDomain.Left param1@pos)':822
         /\ mid_(NewtonDomain.Left param0@pos):815 = (NewtonDomain.Left param0@pos)':823
         /\ mid_(NewtonDomain.Left param1):801 = (NewtonDomain.Left param1)':824
         /\ mid_(NewtonDomain.Left param0):799 = (NewtonDomain.Left param0)':825
         /\ mid_(NewtonDomain.Left __cost):800 = (NewtonDomain.Left __cost)':826
         /\ 0 = K:816 /\ (K:798 + K:816) = K:827 /\ 0 <= K:827
         /\ type_err:828 = (NewtonDomain.Left param1@width)':820
         /\ type_err:829 = (NewtonDomain.Left param0@width)':821
         /\ type_err:830 = (NewtonDomain.Left param1@pos)':822
         /\ type_err:831 = (NewtonDomain.Left param0@pos)':823
         /\ param1:83 = (NewtonDomain.Left param1)':824
         /\ param0:80 = (NewtonDomain.Left param0)':825
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':826
         /\ 0 <= fresh___cost:832 /\ 0 <= (fresh___cost:832 + 1)
         /\ fresh_param0:833 <= 0
         /\ (!(0 <= K:834)
               \/ mid_(NewtonDomain.Left param0):835 = (fresh_param0:833
                                                          + K:834))
         /\ (!(0 <= K:834)
               \/ mid_(NewtonDomain.Left __cost):836 = (fresh___cost:832
                                                          + -K:834))
         /\ ((K:834 = 0
                /\ type_err:837 = mid_(NewtonDomain.Right return@width):838
                /\ type_err:839 = mid_(NewtonDomain.Right return@pos):840
                /\ havoc:841 = mid_(NewtonDomain.Right return):842
                /\ fresh_param0@width:843 = mid_(NewtonDomain.Left param0@width):844
                /\ fresh_param0@pos:845 = mid_(NewtonDomain.Left param0@pos):846
                /\ fresh_param0:833 = mid_(NewtonDomain.Left param0):835
                /\ fresh___cost:832 = mid_(NewtonDomain.Left __cost):836)
               \/ (1 <= K:834 /\ 0 <= fresh_param0:833
                     /\ 0 <= (-1 + fresh___cost:832)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):836
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):835)))
         /\ K:847 = 0
         /\ mid_(NewtonDomain.Right return@width):838 = (NewtonDomain.Right return@width)':848
         /\ mid_(NewtonDomain.Right return@pos):840 = (NewtonDomain.Right return@pos)':849
         /\ mid_(NewtonDomain.Right return):842 = (NewtonDomain.Right return)':850
         /\ mid_(NewtonDomain.Left param0@width):844 = (NewtonDomain.Left param0@width)':851
         /\ mid_(NewtonDomain.Left param0@pos):846 = (NewtonDomain.Left param0@pos)':852
         /\ mid_(NewtonDomain.Left param0):835 = (NewtonDomain.Left param0)':853
         /\ mid_(NewtonDomain.Left __cost):836 = (NewtonDomain.Left __cost)':854
         /\ 0 = K:847 /\ (K:834 + K:847) = K:855 /\ 0 <= K:855
         /\ type_err:856 = (NewtonDomain.Left param0@width)':851
         /\ type_err:857 = (NewtonDomain.Left param0@pos)':852
         /\ (NewtonDomain.Right return)':819 = (NewtonDomain.Left param0)':853
         /\ (fresh___cost:796 + 1) = (NewtonDomain.Left __cost)':854)}

Evaluating variable number 22 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:769 + 1)
 return := havoc:793
 param0 := fresh_param0:770
 param1 := fresh_param1:688
 return@pos := type_err:794
 param0@pos := fresh_param0@pos:782
 param1@pos := fresh_param1@pos:698
 return@width := type_err:795
 param0@width := fresh_param0@width:780
 param1@width := fresh_param1@width:694
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:682
         /\ 0 <= (fresh___cost:682 + 1) /\ fresh_param0:683 <= 0
         /\ (!(0 <= K:684)
               \/ mid_(NewtonDomain.Left param0):685 = (fresh_param0:683
                                                          + K:684))
         /\ (!(0 <= K:684)
               \/ mid_(NewtonDomain.Left __cost):686 = (fresh___cost:682
                                                          + -K:684))
         /\ (!(0 <= K:684)
               \/ mid_(NewtonDomain.Left param1):687 = (fresh_param1:688
                                                          + -K:684))
         /\ (!(0 <= K:684)
               \/ mid_(NewtonDomain.Right return):689 = fresh_param1:688)
         /\ ((K:684 = 0
                /\ type_err:690 = mid_(NewtonDomain.Right return@width):691
                /\ type_err:692 = mid_(NewtonDomain.Right return@pos):693
                /\ fresh_param1:688 = mid_(NewtonDomain.Right return):689
                /\ fresh_param1@width:694 = mid_(NewtonDomain.Left param1@width):695
                /\ fresh_param0@width:696 = mid_(NewtonDomain.Left param0@width):697
                /\ fresh_param1@pos:698 = mid_(NewtonDomain.Left param1@pos):699
                /\ fresh_param0@pos:700 = mid_(NewtonDomain.Left param0@pos):701
                /\ fresh_param1:688 = mid_(NewtonDomain.Left param1):687
                /\ fresh_param0:683 = mid_(NewtonDomain.Left param0):685
                /\ fresh___cost:682 = mid_(NewtonDomain.Left __cost):686)
               \/ (1 <= K:684 /\ 0 <= fresh_param0:683
                     /\ 0 <= (-1 + fresh___cost:682)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):686
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):685)))
         /\ K:702 = 0
         /\ mid_(NewtonDomain.Right return@width):691 = (NewtonDomain.Right return@width)':703
         /\ mid_(NewtonDomain.Right return@pos):693 = (NewtonDomain.Right return@pos)':704
         /\ mid_(NewtonDomain.Right return):689 = (NewtonDomain.Right return)':705
         /\ mid_(NewtonDomain.Left param1@width):695 = (NewtonDomain.Left param1@width)':706
         /\ mid_(NewtonDomain.Left param0@width):697 = (NewtonDomain.Left param0@width)':707
         /\ mid_(NewtonDomain.Left param1@pos):699 = (NewtonDomain.Left param1@pos)':708
         /\ mid_(NewtonDomain.Left param0@pos):701 = (NewtonDomain.Left param0@pos)':709
         /\ mid_(NewtonDomain.Left param1):687 = (NewtonDomain.Left param1)':710
         /\ mid_(NewtonDomain.Left param0):685 = (NewtonDomain.Left param0)':711
         /\ mid_(NewtonDomain.Left __cost):686 = (NewtonDomain.Left __cost)':712
         /\ 0 = K:702 /\ (K:684 + K:702) = K:713 /\ 0 <= K:713
         /\ type_err:133 = (NewtonDomain.Left param1@width)':706
         /\ type_err:132 = (NewtonDomain.Left param0@width)':707
         /\ type_err:131 = (NewtonDomain.Left param1@pos)':708
         /\ type_err:130 = (NewtonDomain.Left param0@pos)':709
         /\ param1:83 = (NewtonDomain.Left param1)':710
         /\ param0:80 = (NewtonDomain.Left param0)':711
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':712
         /\ 0 <= fresh___cost:769 /\ 0 <= (fresh___cost:769 + 1)
         /\ fresh_param0:770 <= 0
         /\ (!(0 <= K:771)
               \/ mid_(NewtonDomain.Left param0):772 = (fresh_param0:770
                                                          + K:771))
         /\ (!(0 <= K:771)
               \/ mid_(NewtonDomain.Left __cost):773 = (fresh___cost:769
                                                          + -K:771))
         /\ ((K:771 = 0
                /\ type_err:774 = mid_(NewtonDomain.Right return@width):775
                /\ type_err:776 = mid_(NewtonDomain.Right return@pos):777
                /\ havoc:778 = mid_(NewtonDomain.Right return):779
                /\ fresh_param0@width:780 = mid_(NewtonDomain.Left param0@width):781
                /\ fresh_param0@pos:782 = mid_(NewtonDomain.Left param0@pos):783
                /\ fresh_param0:770 = mid_(NewtonDomain.Left param0):772
                /\ fresh___cost:769 = mid_(NewtonDomain.Left __cost):773)
               \/ (1 <= K:771 /\ 0 <= fresh_param0:770
                     /\ 0 <= (-1 + fresh___cost:769)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):773
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):772)))
         /\ K:784 = 0
         /\ mid_(NewtonDomain.Right return@width):775 = (NewtonDomain.Right return@width)':785
         /\ mid_(NewtonDomain.Right return@pos):777 = (NewtonDomain.Right return@pos)':786
         /\ mid_(NewtonDomain.Right return):779 = (NewtonDomain.Right return)':787
         /\ mid_(NewtonDomain.Left param0@width):781 = (NewtonDomain.Left param0@width)':788
         /\ mid_(NewtonDomain.Left param0@pos):783 = (NewtonDomain.Left param0@pos)':789
         /\ mid_(NewtonDomain.Left param0):772 = (NewtonDomain.Left param0)':790
         /\ mid_(NewtonDomain.Left __cost):773 = (NewtonDomain.Left __cost)':791
         /\ 0 = K:784 /\ (K:771 + K:784) = K:792 /\ 0 <= K:792
         /\ type_err:715 = (NewtonDomain.Left param0@width)':788
         /\ type_err:714 = (NewtonDomain.Left param0@pos)':789
         /\ (NewtonDomain.Right return)':705 = (NewtonDomain.Left param0)':790
         /\ (fresh___cost:682 + 1) = (NewtonDomain.Left __cost)':791)}

Evaluating variable number 29 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:675 + 1)
 return := (NewtonDomain.Right return)':666
 param0 := fresh_param0:676
 param1 := fresh_param1:677
 return@pos := (NewtonDomain.Right return@pos)':665
 param0@pos := fresh_param0@pos:678
 param1@pos := fresh_param1@pos:679
 return@width := (NewtonDomain.Right return@width)':664
 param0@width := fresh_param0@width:680
 param1@width := fresh_param1@width:681
 when (0 <= fresh___cost:675 /\ 0 <= (fresh___cost:675 + 1)
         /\ fresh_param0:676 <= 0
         /\ (!(0 <= K:652)
               \/ mid_(NewtonDomain.Left param0):653 = (fresh_param0:676
                                                          + K:652))
         /\ (!(0 <= K:652)
               \/ mid_(NewtonDomain.Left __cost):654 = (fresh___cost:675
                                                          + -K:652))
         /\ (!(0 <= K:652)
               \/ mid_(NewtonDomain.Left param1):655 = (fresh_param1:677
                                                          + -K:652))
         /\ (!(0 <= K:652)
               \/ mid_(NewtonDomain.Right return):656 = fresh_param1:677)
         /\ ((K:652 = 0
                /\ type_err:242 = mid_(NewtonDomain.Right return@width):657
                /\ type_err:241 = mid_(NewtonDomain.Right return@pos):658
                /\ fresh_param1:677 = mid_(NewtonDomain.Right return):656
                /\ fresh_param1@width:681 = mid_(NewtonDomain.Left param1@width):659
                /\ fresh_param0@width:680 = mid_(NewtonDomain.Left param0@width):660
                /\ fresh_param1@pos:679 = mid_(NewtonDomain.Left param1@pos):661
                /\ fresh_param0@pos:678 = mid_(NewtonDomain.Left param0@pos):662
                /\ fresh_param1:677 = mid_(NewtonDomain.Left param1):655
                /\ fresh_param0:676 = mid_(NewtonDomain.Left param0):653
                /\ fresh___cost:675 = mid_(NewtonDomain.Left __cost):654)
               \/ (1 <= K:652 /\ 0 <= fresh_param0:676
                     /\ 0 <= (-1 + fresh___cost:675)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):654
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):653)))
         /\ K:663 = 0
         /\ mid_(NewtonDomain.Right return@width):657 = (NewtonDomain.Right return@width)':664
         /\ mid_(NewtonDomain.Right return@pos):658 = (NewtonDomain.Right return@pos)':665
         /\ mid_(NewtonDomain.Right return):656 = (NewtonDomain.Right return)':666
         /\ mid_(NewtonDomain.Left param1@width):659 = (NewtonDomain.Left param1@width)':667
         /\ mid_(NewtonDomain.Left param0@width):660 = (NewtonDomain.Left param0@width)':668
         /\ mid_(NewtonDomain.Left param1@pos):661 = (NewtonDomain.Left param1@pos)':669
         /\ mid_(NewtonDomain.Left param0@pos):662 = (NewtonDomain.Left param0@pos)':670
         /\ mid_(NewtonDomain.Left param1):655 = (NewtonDomain.Left param1)':671
         /\ mid_(NewtonDomain.Left param0):653 = (NewtonDomain.Left param0)':672
         /\ mid_(NewtonDomain.Left __cost):654 = (NewtonDomain.Left __cost)':673
         /\ 0 = K:663 /\ (K:652 + K:663) = K:674 /\ 0 <= K:674
         /\ param1@width:81 = (NewtonDomain.Left param1@width)':667
         /\ param0@width:78 = (NewtonDomain.Left param0@width)':668
         /\ param1@pos:82 = (NewtonDomain.Left param1@pos)':669
         /\ param0@pos:79 = (NewtonDomain.Left param0@pos)':670
         /\ param1:83 = (NewtonDomain.Left param1)':671
         /\ param0:80 = (NewtonDomain.Left param0)':672
         /\ __cost:101 = (NewtonDomain.Left __cost)':673)}

Evaluating variable number 37 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := (fresh___cost:765 + 1)
 return := (NewtonDomain.Right return)':759
 param0 := fresh_param0:766
 return@pos := (NewtonDomain.Right return@pos)':758
 param0@pos := fresh_param0@pos:767
 return@width := (NewtonDomain.Right return@width)':757
 param0@width := fresh_param0@width:768
 when (0 <= fresh___cost:765 /\ 0 <= (fresh___cost:765 + 1)
         /\ fresh_param0:766 <= 0
         /\ (!(0 <= K:748)
               \/ mid_(NewtonDomain.Left param0):749 = (fresh_param0:766
                                                          + K:748))
         /\ (!(0 <= K:748)
               \/ mid_(NewtonDomain.Left __cost):750 = (fresh___cost:765
                                                          + -K:748))
         /\ ((K:748 = 0
                /\ type_err:245 = mid_(NewtonDomain.Right return@width):751
                /\ type_err:244 = mid_(NewtonDomain.Right return@pos):752
                /\ havoc:243 = mid_(NewtonDomain.Right return):753
                /\ fresh_param0@width:768 = mid_(NewtonDomain.Left param0@width):754
                /\ fresh_param0@pos:767 = mid_(NewtonDomain.Left param0@pos):755
                /\ fresh_param0:766 = mid_(NewtonDomain.Left param0):749
                /\ fresh___cost:765 = mid_(NewtonDomain.Left __cost):750)
               \/ (1 <= K:748 /\ 0 <= fresh_param0:766
                     /\ 0 <= (-1 + fresh___cost:765)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):750
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):749)))
         /\ K:756 = 0
         /\ mid_(NewtonDomain.Right return@width):751 = (NewtonDomain.Right return@width)':757
         /\ mid_(NewtonDomain.Right return@pos):752 = (NewtonDomain.Right return@pos)':758
         /\ mid_(NewtonDomain.Right return):753 = (NewtonDomain.Right return)':759
         /\ mid_(NewtonDomain.Left param0@width):754 = (NewtonDomain.Left param0@width)':760
         /\ mid_(NewtonDomain.Left param0@pos):755 = (NewtonDomain.Left param0@pos)':761
         /\ mid_(NewtonDomain.Left param0):749 = (NewtonDomain.Left param0)':762
         /\ mid_(NewtonDomain.Left __cost):750 = (NewtonDomain.Left __cost)':763
         /\ 0 = K:756 /\ (K:748 + K:756) = K:764 /\ 0 <= K:764
         /\ param0@width:78 = (NewtonDomain.Left param0@width)':760
         /\ param0@pos:79 = (NewtonDomain.Left param0@pos)':761
         /\ param0:80 = (NewtonDomain.Left param0)':762
         /\ __cost:101 = (NewtonDomain.Left __cost)':763)}

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

NumRnds: 2

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,82)_g1> -> <__pstate, (Unique State Name,66)_g1>	Base relation: 
{__cost := (fresh___cost:1151 + 1)
 y := (NewtonDomain.Right return)':1174
 return := (NewtonDomain.Right return)':1174
 param0 := (NewtonDomain.Right return)':1174
 param1 := fresh_param1:1157
 return@pos := (NewtonDomain.Right return@pos)':1173
 param0@pos := type_err:1183
 param1@pos := fresh_param1@pos:1167
 return@width := (NewtonDomain.Right return@width)':1172
 param0@width := type_err:1184
 param1@width := fresh_param1@width:1163
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:1151
         /\ 0 <= (fresh___cost:1151 + 1) /\ fresh_param0:1152 <= 0
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param0):1154 = (fresh_param0:1152
                                                           + K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left __cost):1155 = (fresh___cost:1151
                                                           + -K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param1):1156 = (fresh_param1:1157
                                                           + -K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Right return):1158 = fresh_param1:1157)
         /\ ((K:1153 = 0
                /\ type_err:1159 = mid_(NewtonDomain.Right return@width):1160
                /\ type_err:1161 = mid_(NewtonDomain.Right return@pos):1162
                /\ fresh_param1:1157 = mid_(NewtonDomain.Right return):1158
                /\ fresh_param1@width:1163 = mid_(NewtonDomain.Left param1@width):1164
                /\ fresh_param0@width:1165 = mid_(NewtonDomain.Left param0@width):1166
                /\ fresh_param1@pos:1167 = mid_(NewtonDomain.Left param1@pos):1168
                /\ fresh_param0@pos:1169 = mid_(NewtonDomain.Left param0@pos):1170
                /\ fresh_param1:1157 = mid_(NewtonDomain.Left param1):1156
                /\ fresh_param0:1152 = mid_(NewtonDomain.Left param0):1154
                /\ fresh___cost:1151 = mid_(NewtonDomain.Left __cost):1155)
               \/ (1 <= K:1153 /\ 0 <= fresh_param0:1152
                     /\ 0 <= (-1 + fresh___cost:1151)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1155
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1154)))
         /\ K:1171 = 0
         /\ mid_(NewtonDomain.Right return@width):1160 = (NewtonDomain.Right return@width)':1172
         /\ mid_(NewtonDomain.Right return@pos):1162 = (NewtonDomain.Right return@pos)':1173
         /\ mid_(NewtonDomain.Right return):1158 = (NewtonDomain.Right return)':1174
         /\ mid_(NewtonDomain.Left param1@width):1164 = (NewtonDomain.Left param1@width)':1175
         /\ mid_(NewtonDomain.Left param0@width):1166 = (NewtonDomain.Left param0@width)':1176
         /\ mid_(NewtonDomain.Left param1@pos):1168 = (NewtonDomain.Left param1@pos)':1177
         /\ mid_(NewtonDomain.Left param0@pos):1170 = (NewtonDomain.Left param0@pos)':1178
         /\ mid_(NewtonDomain.Left param1):1156 = (NewtonDomain.Left param1)':1179
         /\ mid_(NewtonDomain.Left param0):1154 = (NewtonDomain.Left param0)':1180
         /\ mid_(NewtonDomain.Left __cost):1155 = (NewtonDomain.Left __cost)':1181
         /\ 0 = K:1171 /\ (K:1153 + K:1171) = K:1182 /\ 0 <= K:1182
         /\ type_err:133 = (NewtonDomain.Left param1@width)':1175
         /\ type_err:132 = (NewtonDomain.Left param0@width)':1176
         /\ type_err:131 = (NewtonDomain.Left param1@pos)':1177
         /\ type_err:130 = (NewtonDomain.Left param0@pos)':1178
         /\ param1:83 = (NewtonDomain.Left param1)':1179
         /\ param0:80 = (NewtonDomain.Left param0)':1180
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':1181)}	
<__pstate, (Unique State Name,82)_g1> -> <__pstate, (Unique State Name,72)_g1>	Base relation: 
{__cost := (__cost:101 + 1)
 y := param1:83
 param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:130
 param1@pos := type_err:131
 param0@width := type_err:132
 param1@width := type_err:133
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1))}	
<__pstate, accept> -> <__pstate, (Unique State Name,88)_g1>	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}	
<__pstate, (Unique State Name,66)_g1> -> <__pstate, (Unique State Name,66)_g1>	Base relation: 
{__cost := (__cost:101 + 1)
 x := (param0:80 + -1)
 param0 := (param0:80 + -1)
 param0@pos := type_err:237
 param0@width := type_err:238
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}	
<__pstate, (Unique State Name,88)_g1> -> <__pstate, (Unique State Name,82)_g1>	Base relation: 
{param0 := param0:80
 param1 := param1:83
 param0@pos := type_err:88
 param1@pos := type_err:89
 param0@width := type_err:90
 param1@width := type_err:91}	
<__pstate, (Unique State Name,72)_g1> -> <__pstate, (Unique State Name,72)_g1>	Base relation: 
{__cost := (__cost:101 + 1)
 x := (param0:80 + -1)
 y := (param1:83 + 1)
 param0 := (param0:80 + -1)
 param1 := (param1:83 + 1)
 param0@pos := type_err:233
 param1@pos := type_err:234
 param0@width := type_err:235
 param1@width := type_err:236
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80)}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x69dc7b0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x6a40260: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,88)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:27
 param1@pos := type_err:29
 param0@width := type_err:28
 param1@width := type_err:30}
    ( __pstate , (Unique State Name,66)_g1 , __done )	Base relation: 
{__cost := __cost':1291
 x := havoc:21
 y := havoc:22
 y := (NewtonDomain.Right return)':1239
 x := x':1290
 return := (NewtonDomain.Right return)':1239
 param0 := param0':1289
 param1 := fresh_param1:1222
 return@pos := (NewtonDomain.Right return@pos)':1238
 param0@pos := param0@pos':1288
 param1@pos := fresh_param1@pos:1232
 return@width := (NewtonDomain.Right return@width)':1237
 param0@width := param0@width':1287
 param1@width := fresh_param1@width:1228
 when (0 <= fresh___cost:1216 /\ 0 <= (fresh___cost:1216 + 1)
         /\ fresh_param0:1217 <= 0
         /\ (!(0 <= K:1218)
               \/ mid_(NewtonDomain.Left param0):1219 = (fresh_param0:1217
                                                           + K:1218))
         /\ (!(0 <= K:1218)
               \/ mid_(NewtonDomain.Left __cost):1220 = (fresh___cost:1216
                                                           + -K:1218))
         /\ (!(0 <= K:1218)
               \/ mid_(NewtonDomain.Left param1):1221 = (fresh_param1:1222
                                                           + -K:1218))
         /\ (!(0 <= K:1218)
               \/ mid_(NewtonDomain.Right return):1223 = fresh_param1:1222)
         /\ ((K:1218 = 0
                /\ type_err:1224 = mid_(NewtonDomain.Right return@width):1225
                /\ type_err:1226 = mid_(NewtonDomain.Right return@pos):1227
                /\ fresh_param1:1222 = mid_(NewtonDomain.Right return):1223
                /\ fresh_param1@width:1228 = mid_(NewtonDomain.Left param1@width):1229
                /\ fresh_param0@width:1230 = mid_(NewtonDomain.Left param0@width):1231
                /\ fresh_param1@pos:1232 = mid_(NewtonDomain.Left param1@pos):1233
                /\ fresh_param0@pos:1234 = mid_(NewtonDomain.Left param0@pos):1235
                /\ fresh_param1:1222 = mid_(NewtonDomain.Left param1):1221
                /\ fresh_param0:1217 = mid_(NewtonDomain.Left param0):1219
                /\ fresh___cost:1216 = mid_(NewtonDomain.Left __cost):1220)
               \/ (1 <= K:1218 /\ 0 <= fresh_param0:1217
                     /\ 0 <= (-1 + fresh___cost:1216)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1220
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1219)))
         /\ K:1236 = 0
         /\ mid_(NewtonDomain.Right return@width):1225 = (NewtonDomain.Right return@width)':1237
         /\ mid_(NewtonDomain.Right return@pos):1227 = (NewtonDomain.Right return@pos)':1238
         /\ mid_(NewtonDomain.Right return):1223 = (NewtonDomain.Right return)':1239
         /\ mid_(NewtonDomain.Left param1@width):1229 = (NewtonDomain.Left param1@width)':1240
         /\ mid_(NewtonDomain.Left param0@width):1231 = (NewtonDomain.Left param0@width)':1241
         /\ mid_(NewtonDomain.Left param1@pos):1233 = (NewtonDomain.Left param1@pos)':1242
         /\ mid_(NewtonDomain.Left param0@pos):1235 = (NewtonDomain.Left param0@pos)':1243
         /\ mid_(NewtonDomain.Left param1):1221 = (NewtonDomain.Left param1)':1244
         /\ mid_(NewtonDomain.Left param0):1219 = (NewtonDomain.Left param0)':1245
         /\ mid_(NewtonDomain.Left __cost):1220 = (NewtonDomain.Left __cost)':1246
         /\ 0 = K:1236 /\ (K:1218 + K:1236) = K:1247 /\ 0 <= K:1247
         /\ type_err:1248 = (NewtonDomain.Left param1@width)':1240
         /\ type_err:1249 = (NewtonDomain.Left param0@width)':1241
         /\ type_err:1250 = (NewtonDomain.Left param1@pos)':1242
         /\ type_err:1251 = (NewtonDomain.Left param0@pos)':1243
         /\ havoc:22 = (NewtonDomain.Left param1)':1244
         /\ havoc:21 = (NewtonDomain.Left param0)':1245
         /\ 1 = (NewtonDomain.Left __cost)':1246
         /\ (!(0 <= K:1280)
               \/ mid___cost:1281 = ((fresh___cost:1216 + 1) + K:1280))
         /\ (!(0 <= K:1280)
               \/ mid_param0:1282 = ((NewtonDomain.Right return)':1239
                                       + -K:1280))
         /\ (!((0 <= K:1280 /\ K:1280 <= 0))
               \/ mid_x:1283 = (x:199 + -K:1280))
         /\ (!(1 <= K:1280)
               \/ mid_x:1283 = ((NewtonDomain.Right return)':1239 + -K:1280))
         /\ ((K:1280 = 0 /\ type_err:1253 = mid_param0@width:1284
                /\ type_err:1252 = mid_param0@pos:1285
                /\ (NewtonDomain.Right return)':1239 = mid_param0:1282
                /\ x:199 = mid_x:1283
                /\ (fresh___cost:1216 + 1) = mid___cost:1281)
               \/ (1 <= K:1280 /\ 0 <= (fresh___cost:1216 + 1)
                     /\ 0 <= (-1 + (NewtonDomain.Right return)':1239)
                     /\ (-mid_x:1283 + mid_param0:1282) = 0
                     /\ 0 <= mid_x:1283 /\ 0 <= (-1 + mid___cost:1281)))
         /\ K:1286 = 0 /\ mid_param0@width:1284 = param0@width':1287
         /\ mid_param0@pos:1285 = param0@pos':1288
         /\ mid_param0:1282 = param0':1289 /\ mid_x:1283 = x':1290
         /\ mid___cost:1281 = __cost':1291 /\ 0 = K:1286
         /\ (K:1280 + K:1286) = K:1292 /\ 0 <= K:1292)}
    ( __pstate , (Unique State Name,72)_g1 , __done )	Base relation: 
{__cost := __cost':1360
 x := havoc:21
 y := havoc:22
 y := havoc:22
 x := x':1359
 y := y':1358
 param0 := param0':1357
 param1 := param1':1356
 param0@pos := param0@pos':1355
 param1@pos := param1@pos':1354
 param0@width := param0@width':1353
 param1@width := param1@width':1352
 when ((!((0 <= K:1341 /\ K:1341 <= 0)) \/ mid_x:1342 = (x:152 + -K:1341))
         /\ (!(1 <= K:1341)
               \/ mid_x:1342 = (x:152 + havoc:21 + -x:152 + -K:1341))
         /\ (!(0 <= K:1341) \/ mid_param0:1343 = (havoc:21 + -K:1341))
         /\ (!(0 <= K:1341) \/ mid___cost:1344 = (1 + K:1341))
         /\ (!(0 <= K:1341) \/ mid_param1:1345 = (havoc:22 + K:1341))
         /\ (!((0 <= K:1341 /\ K:1341 <= 0)) \/ mid_y:1346 = (y:151 + K:1341))
         /\ (!(1 <= K:1341) \/ mid_y:1346 = (havoc:22 + K:1341))
         /\ (!((0 <= K:1341 /\ K:1341 <= 0))
               \/ -mid_x:1342 <= (-x:152 + (1/2 * K:1341)
                                    + (havoc:21 * K:1341)
                                    + (-1/2 * (K:1341 * K:1341))))
         /\ (!(1 <= K:1341)
               \/ -mid_x:1342 <= (x:152 + -x:152 + -havoc:21 + (1/2 * K:1341)
                                    + (havoc:21 * K:1341)
                                    + (-1/2 * (K:1341 * K:1341))))
         /\ ((K:1341 = 0 /\ type_err:1300 = mid_param1@width:1347
                /\ type_err:1299 = mid_param0@width:1348
                /\ type_err:1298 = mid_param1@pos:1349
                /\ type_err:1297 = mid_param0@pos:1350
                /\ havoc:22 = mid_param1:1345 /\ havoc:21 = mid_param0:1343
                /\ y:151 = mid_y:1346 /\ x:152 = mid_x:1342
                /\ 1 = mid___cost:1344)
               \/ (1 <= K:1341 /\ 0 <= (-1 + havoc:21)
                     /\ (-mid_y:1346 + mid_param1:1345) = 0
                     /\ (-mid_x:1342 + mid_param0:1343) = 0
                     /\ 0 <= mid_x:1342 /\ 0 <= (-1 + mid___cost:1344)))
         /\ K:1351 = 0 /\ mid_param1@width:1347 = param1@width':1352
         /\ mid_param0@width:1348 = param0@width':1353
         /\ mid_param1@pos:1349 = param1@pos':1354
         /\ mid_param0@pos:1350 = param0@pos':1355
         /\ mid_param1:1345 = param1':1356 /\ mid_param0:1343 = param0':1357
         /\ mid_y:1346 = y':1358 /\ mid_x:1342 = x':1359
         /\ mid___cost:1344 = __cost':1360 /\ 0 = K:1351
         /\ (K:1341 + K:1351) = K:1361 /\ 0 <= K:1361)}
    ( __pstate , (Unique State Name,82)_g1 , __done )	Base relation: 
{__cost := 0
 x := havoc:21
 y := havoc:22
 param0 := havoc:21
 param1 := havoc:22
 param0@pos := type_err:1362
 param1@pos := type_err:1363
 param0@width := type_err:1364
 param1@width := type_err:1365}

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

------------------------------------------------
Procedure summary for copy

Base relation: 
{__cost := phi___cost:1148
 x := phi_x:1147
 y := phi_y:1146
 return := phi_y:1146
 param0 := phi_param0:1144
 param1 := phi_param1:1143
 return@pos := type_err:1149
 param0@pos := phi_param0@pos:1141
 param1@pos := phi_param1@pos:1140
 return@width := type_err:1150
 param0@width := phi_param0@width:1138
 param1@width := phi_param1@width:1137
 when ((0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0
          /\ (__cost:101 + 1) = phi___cost:1148 /\ param0:80 = phi_x:1147
          /\ param1:83 = phi_y:1146 /\ return:109 = phi_return:1145
          /\ param0:80 = phi_param0:1144 /\ param1:83 = phi_param1:1143
          /\ return@pos:108 = phi_return@pos:1142
          /\ param0@pos:79 = phi_param0@pos:1141
          /\ param1@pos:82 = phi_param1@pos:1140
          /\ return@width:107 = phi_return@width:1139
          /\ param0@width:78 = phi_param0@width:1138
          /\ param1@width:81 = phi_param1@width:1137)
         \/ (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80
               /\ 0 <= fresh___cost:1105 /\ 0 <= (fresh___cost:1105 + 1)
               /\ fresh_param0:1106 <= 0
               /\ (!(0 <= K:1107)
                     \/ mid_(NewtonDomain.Left param0):1108 = (fresh_param0:1106
                                                                 + K:1107))
               /\ (!(0 <= K:1107)
                     \/ mid_(NewtonDomain.Left __cost):1109 = (fresh___cost:1105
                                                                 + -K:1107))
               /\ (!(0 <= K:1107)
                     \/ mid_(NewtonDomain.Left param1):1110 = (fresh_param1:1111
                                                                 + -K:1107))
               /\ (!(0 <= K:1107)
                     \/ mid_(NewtonDomain.Right return):1112 = fresh_param1:1111)
               /\ ((K:1107 = 0
                      /\ type_err:1113 = mid_(NewtonDomain.Right return@width):1114
                      /\ type_err:1115 = mid_(NewtonDomain.Right return@pos):1116
                      /\ fresh_param1:1111 = mid_(NewtonDomain.Right return):1112
                      /\ fresh_param1@width:1117 = mid_(NewtonDomain.Left param1@width):1118
                      /\ fresh_param0@width:1119 = mid_(NewtonDomain.Left param0@width):1120
                      /\ fresh_param1@pos:1121 = mid_(NewtonDomain.Left param1@pos):1122
                      /\ fresh_param0@pos:1123 = mid_(NewtonDomain.Left param0@pos):1124
                      /\ fresh_param1:1111 = mid_(NewtonDomain.Left param1):1110
                      /\ fresh_param0:1106 = mid_(NewtonDomain.Left param0):1108
                      /\ fresh___cost:1105 = mid_(NewtonDomain.Left __cost):1109)
                     \/ (1 <= K:1107 /\ 0 <= fresh_param0:1106
                           /\ 0 <= (-1 + fresh___cost:1105)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1109
                           /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1108)))
               /\ K:1125 = 0
               /\ mid_(NewtonDomain.Right return@width):1114 = (NewtonDomain.Right return@width)':1126
               /\ mid_(NewtonDomain.Right return@pos):1116 = (NewtonDomain.Right return@pos)':1127
               /\ mid_(NewtonDomain.Right return):1112 = (NewtonDomain.Right return)':1128
               /\ mid_(NewtonDomain.Left param1@width):1118 = (NewtonDomain.Left param1@width)':1129
               /\ mid_(NewtonDomain.Left param0@width):1120 = (NewtonDomain.Left param0@width)':1130
               /\ mid_(NewtonDomain.Left param1@pos):1122 = (NewtonDomain.Left param1@pos)':1131
               /\ mid_(NewtonDomain.Left param0@pos):1124 = (NewtonDomain.Left param0@pos)':1132
               /\ mid_(NewtonDomain.Left param1):1110 = (NewtonDomain.Left param1)':1133
               /\ mid_(NewtonDomain.Left param0):1108 = (NewtonDomain.Left param0)':1134
               /\ mid_(NewtonDomain.Left __cost):1109 = (NewtonDomain.Left __cost)':1135
               /\ 0 = K:1125 /\ (K:1107 + K:1125) = K:1136 /\ 0 <= K:1136
               /\ type_err:236 = (NewtonDomain.Left param1@width)':1129
               /\ type_err:235 = (NewtonDomain.Left param0@width)':1130
               /\ type_err:234 = (NewtonDomain.Left param1@pos)':1131
               /\ type_err:233 = (NewtonDomain.Left param0@pos)':1132
               /\ (param1:83 + 1) = (NewtonDomain.Left param1)':1133
               /\ (param0:80 + -1) = (NewtonDomain.Left param0)':1134
               /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':1135
               /\ (fresh___cost:1105 + 1) = phi___cost:1148
               /\ (param0:80 + -1) = phi_x:1147
               /\ (NewtonDomain.Right return)':1128 = phi_y:1146
               /\ (NewtonDomain.Right return)':1128 = phi_return:1145
               /\ fresh_param0:1106 = phi_param0:1144
               /\ fresh_param1:1111 = phi_param1:1143
               /\ (NewtonDomain.Right return@pos)':1127 = phi_return@pos:1142
               /\ fresh_param0@pos:1123 = phi_param0@pos:1141
               /\ fresh_param1@pos:1121 = phi_param1@pos:1140
               /\ (NewtonDomain.Right return@width)':1126 = phi_return@width:1139
               /\ fresh_param0@width:1119 = phi_param0@width:1138
               /\ fresh_param1@width:1117 = phi_param1@width:1137))}

------------------------------------------------
Procedure summary for count_down

Base relation: 
{__cost := phi___cost:1101
 x := phi_x:1100
 return := havoc:1102
 param0 := phi_param0:1098
 return@pos := type_err:1103
 param0@pos := phi_param0@pos:1096
 return@width := type_err:1104
 param0@width := phi_param0@width:1094
 when ((0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ param0:80 <= 0
          /\ (__cost:101 + 1) = phi___cost:1101 /\ param0:80 = phi_x:1100
          /\ return:109 = phi_return:1099 /\ param0:80 = phi_param0:1098
          /\ return@pos:108 = phi_return@pos:1097
          /\ param0@pos:79 = phi_param0@pos:1096
          /\ return@width:107 = phi_return@width:1095
          /\ param0@width:78 = phi_param0@width:1094)
         \/ (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 < param0:80
               /\ 0 <= fresh___cost:1070 /\ 0 <= (fresh___cost:1070 + 1)
               /\ fresh_param0:1071 <= 0
               /\ (!(0 <= K:1072)
                     \/ mid_(NewtonDomain.Left param0):1073 = (fresh_param0:1071
                                                                 + K:1072))
               /\ (!(0 <= K:1072)
                     \/ mid_(NewtonDomain.Left __cost):1074 = (fresh___cost:1070
                                                                 + -K:1072))
               /\ ((K:1072 = 0
                      /\ type_err:1075 = mid_(NewtonDomain.Right return@width):1076
                      /\ type_err:1077 = mid_(NewtonDomain.Right return@pos):1078
                      /\ havoc:1079 = mid_(NewtonDomain.Right return):1080
                      /\ fresh_param0@width:1081 = mid_(NewtonDomain.Left param0@width):1082
                      /\ fresh_param0@pos:1083 = mid_(NewtonDomain.Left param0@pos):1084
                      /\ fresh_param0:1071 = mid_(NewtonDomain.Left param0):1073
                      /\ fresh___cost:1070 = mid_(NewtonDomain.Left __cost):1074)
                     \/ (1 <= K:1072 /\ 0 <= fresh_param0:1071
                           /\ 0 <= (-1 + fresh___cost:1070)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1074
                           /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1073)))
               /\ K:1085 = 0
               /\ mid_(NewtonDomain.Right return@width):1076 = (NewtonDomain.Right return@width)':1086
               /\ mid_(NewtonDomain.Right return@pos):1078 = (NewtonDomain.Right return@pos)':1087
               /\ mid_(NewtonDomain.Right return):1080 = (NewtonDomain.Right return)':1088
               /\ mid_(NewtonDomain.Left param0@width):1082 = (NewtonDomain.Left param0@width)':1089
               /\ mid_(NewtonDomain.Left param0@pos):1084 = (NewtonDomain.Left param0@pos)':1090
               /\ mid_(NewtonDomain.Left param0):1073 = (NewtonDomain.Left param0)':1091
               /\ mid_(NewtonDomain.Left __cost):1074 = (NewtonDomain.Left __cost)':1092
               /\ 0 = K:1085 /\ (K:1072 + K:1085) = K:1093 /\ 0 <= K:1093
               /\ type_err:238 = (NewtonDomain.Left param0@width)':1089
               /\ type_err:237 = (NewtonDomain.Left param0@pos)':1090
               /\ (param0:80 + -1) = (NewtonDomain.Left param0)':1091
               /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':1092
               /\ (fresh___cost:1070 + 1) = phi___cost:1101
               /\ (param0:80 + -1) = phi_x:1100
               /\ (NewtonDomain.Right return)':1088 = phi_return:1099
               /\ fresh_param0:1071 = phi_param0:1098
               /\ (NewtonDomain.Right return@pos)':1087 = phi_return@pos:1097
               /\ fresh_param0@pos:1083 = phi_param0@pos:1096
               /\ (NewtonDomain.Right return@width)':1086 = phi_return@width:1095
               /\ fresh_param0@width:1081 = phi_param0@width:1094))}

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

Base relation: 
{__cost := (fresh___cost:969 + 1)
 x := havoc:21
 y := havoc:22
 return := 0
 param0 := fresh_param0:970
 param1 := fresh_param1:939
 return@pos := type_err:1000
 param0@pos := fresh_param0@pos:982
 param1@pos := fresh_param1@pos:949
 return@width := type_err:1001
 param0@width := fresh_param0@width:980
 param1@width := fresh_param1@width:945
 when (0 <= fresh___cost:933 /\ 0 <= (fresh___cost:933 + 1)
         /\ fresh_param0:934 <= 0
         /\ (!(0 <= K:935)
               \/ mid_(NewtonDomain.Left param0):936 = (fresh_param0:934
                                                          + K:935))
         /\ (!(0 <= K:935)
               \/ mid_(NewtonDomain.Left __cost):937 = (fresh___cost:933
                                                          + -K:935))
         /\ (!(0 <= K:935)
               \/ mid_(NewtonDomain.Left param1):938 = (fresh_param1:939
                                                          + -K:935))
         /\ (!(0 <= K:935)
               \/ mid_(NewtonDomain.Right return):940 = fresh_param1:939)
         /\ ((K:935 = 0
                /\ type_err:941 = mid_(NewtonDomain.Right return@width):942
                /\ type_err:943 = mid_(NewtonDomain.Right return@pos):944
                /\ fresh_param1:939 = mid_(NewtonDomain.Right return):940
                /\ fresh_param1@width:945 = mid_(NewtonDomain.Left param1@width):946
                /\ fresh_param0@width:947 = mid_(NewtonDomain.Left param0@width):948
                /\ fresh_param1@pos:949 = mid_(NewtonDomain.Left param1@pos):950
                /\ fresh_param0@pos:951 = mid_(NewtonDomain.Left param0@pos):952
                /\ fresh_param1:939 = mid_(NewtonDomain.Left param1):938
                /\ fresh_param0:934 = mid_(NewtonDomain.Left param0):936
                /\ fresh___cost:933 = mid_(NewtonDomain.Left __cost):937)
               \/ (1 <= K:935 /\ 0 <= fresh_param0:934
                     /\ 0 <= (-1 + fresh___cost:933)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):937
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):936)))
         /\ K:953 = 0
         /\ mid_(NewtonDomain.Right return@width):942 = (NewtonDomain.Right return@width)':954
         /\ mid_(NewtonDomain.Right return@pos):944 = (NewtonDomain.Right return@pos)':955
         /\ mid_(NewtonDomain.Right return):940 = (NewtonDomain.Right return)':956
         /\ mid_(NewtonDomain.Left param1@width):946 = (NewtonDomain.Left param1@width)':957
         /\ mid_(NewtonDomain.Left param0@width):948 = (NewtonDomain.Left param0@width)':958
         /\ mid_(NewtonDomain.Left param1@pos):950 = (NewtonDomain.Left param1@pos)':959
         /\ mid_(NewtonDomain.Left param0@pos):952 = (NewtonDomain.Left param0@pos)':960
         /\ mid_(NewtonDomain.Left param1):938 = (NewtonDomain.Left param1)':961
         /\ mid_(NewtonDomain.Left param0):936 = (NewtonDomain.Left param0)':962
         /\ mid_(NewtonDomain.Left __cost):937 = (NewtonDomain.Left __cost)':963
         /\ 0 = K:953 /\ (K:935 + K:953) = K:964 /\ 0 <= K:964
         /\ type_err:965 = (NewtonDomain.Left param1@width)':957
         /\ type_err:966 = (NewtonDomain.Left param0@width)':958
         /\ type_err:967 = (NewtonDomain.Left param1@pos)':959
         /\ type_err:968 = (NewtonDomain.Left param0@pos)':960
         /\ havoc:22 = (NewtonDomain.Left param1)':961
         /\ havoc:21 = (NewtonDomain.Left param0)':962
         /\ 1 = (NewtonDomain.Left __cost)':963 /\ 0 <= fresh___cost:969
         /\ 0 <= (fresh___cost:969 + 1) /\ fresh_param0:970 <= 0
         /\ (!(0 <= K:971)
               \/ mid_(NewtonDomain.Left param0):972 = (fresh_param0:970
                                                          + K:971))
         /\ (!(0 <= K:971)
               \/ mid_(NewtonDomain.Left __cost):973 = (fresh___cost:969
                                                          + -K:971))
         /\ ((K:971 = 0
                /\ type_err:974 = mid_(NewtonDomain.Right return@width):975
                /\ type_err:976 = mid_(NewtonDomain.Right return@pos):977
                /\ havoc:978 = mid_(NewtonDomain.Right return):979
                /\ fresh_param0@width:980 = mid_(NewtonDomain.Left param0@width):981
                /\ fresh_param0@pos:982 = mid_(NewtonDomain.Left param0@pos):983
                /\ fresh_param0:970 = mid_(NewtonDomain.Left param0):972
                /\ fresh___cost:969 = mid_(NewtonDomain.Left __cost):973)
               \/ (1 <= K:971 /\ 0 <= fresh_param0:970
                     /\ 0 <= (-1 + fresh___cost:969)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):973
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):972)))
         /\ K:984 = 0
         /\ mid_(NewtonDomain.Right return@width):975 = (NewtonDomain.Right return@width)':985
         /\ mid_(NewtonDomain.Right return@pos):977 = (NewtonDomain.Right return@pos)':986
         /\ mid_(NewtonDomain.Right return):979 = (NewtonDomain.Right return)':987
         /\ mid_(NewtonDomain.Left param0@width):981 = (NewtonDomain.Left param0@width)':988
         /\ mid_(NewtonDomain.Left param0@pos):983 = (NewtonDomain.Left param0@pos)':989
         /\ mid_(NewtonDomain.Left param0):972 = (NewtonDomain.Left param0)':990
         /\ mid_(NewtonDomain.Left __cost):973 = (NewtonDomain.Left __cost)':991
         /\ 0 = K:984 /\ (K:971 + K:984) = K:992 /\ 0 <= K:992
         /\ type_err:993 = (NewtonDomain.Left param0@width)':988
         /\ type_err:994 = (NewtonDomain.Left param0@pos)':989
         /\ (NewtonDomain.Right return)':956 = (NewtonDomain.Left param0)':990
         /\ (fresh___cost:933 + 1) = (NewtonDomain.Left __cost)':991
         /\ ((0 < havoc:21 /\ havoc:21 = phi_tmp___1:998)
               \/ (havoc:21 <= 0 /\ 0 = phi_tmp___1:998))
         /\ ((0 < havoc:22 /\ havoc:22 = phi_tmp___2:999)
               \/ (havoc:22 <= 0 /\ 0 = phi_tmp___2:999)))}

------------------------------------------------
Procedure summary for run

Base relation: 
{__cost := (fresh___cost:1038 + 1)
 return := havoc:1067
 param0 := fresh_param0:1039
 param1 := fresh_param1:1008
 return@pos := type_err:1068
 param0@pos := fresh_param0@pos:1051
 param1@pos := fresh_param1@pos:1018
 return@width := type_err:1069
 param0@width := fresh_param0@width:1049
 param1@width := fresh_param1@width:1014
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:1002
         /\ 0 <= (fresh___cost:1002 + 1) /\ fresh_param0:1003 <= 0
         /\ (!(0 <= K:1004)
               \/ mid_(NewtonDomain.Left param0):1005 = (fresh_param0:1003
                                                           + K:1004))
         /\ (!(0 <= K:1004)
               \/ mid_(NewtonDomain.Left __cost):1006 = (fresh___cost:1002
                                                           + -K:1004))
         /\ (!(0 <= K:1004)
               \/ mid_(NewtonDomain.Left param1):1007 = (fresh_param1:1008
                                                           + -K:1004))
         /\ (!(0 <= K:1004)
               \/ mid_(NewtonDomain.Right return):1009 = fresh_param1:1008)
         /\ ((K:1004 = 0
                /\ type_err:1010 = mid_(NewtonDomain.Right return@width):1011
                /\ type_err:1012 = mid_(NewtonDomain.Right return@pos):1013
                /\ fresh_param1:1008 = mid_(NewtonDomain.Right return):1009
                /\ fresh_param1@width:1014 = mid_(NewtonDomain.Left param1@width):1015
                /\ fresh_param0@width:1016 = mid_(NewtonDomain.Left param0@width):1017
                /\ fresh_param1@pos:1018 = mid_(NewtonDomain.Left param1@pos):1019
                /\ fresh_param0@pos:1020 = mid_(NewtonDomain.Left param0@pos):1021
                /\ fresh_param1:1008 = mid_(NewtonDomain.Left param1):1007
                /\ fresh_param0:1003 = mid_(NewtonDomain.Left param0):1005
                /\ fresh___cost:1002 = mid_(NewtonDomain.Left __cost):1006)
               \/ (1 <= K:1004 /\ 0 <= fresh_param0:1003
                     /\ 0 <= (-1 + fresh___cost:1002)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1006
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1005)))
         /\ K:1022 = 0
         /\ mid_(NewtonDomain.Right return@width):1011 = (NewtonDomain.Right return@width)':1023
         /\ mid_(NewtonDomain.Right return@pos):1013 = (NewtonDomain.Right return@pos)':1024
         /\ mid_(NewtonDomain.Right return):1009 = (NewtonDomain.Right return)':1025
         /\ mid_(NewtonDomain.Left param1@width):1015 = (NewtonDomain.Left param1@width)':1026
         /\ mid_(NewtonDomain.Left param0@width):1017 = (NewtonDomain.Left param0@width)':1027
         /\ mid_(NewtonDomain.Left param1@pos):1019 = (NewtonDomain.Left param1@pos)':1028
         /\ mid_(NewtonDomain.Left param0@pos):1021 = (NewtonDomain.Left param0@pos)':1029
         /\ mid_(NewtonDomain.Left param1):1007 = (NewtonDomain.Left param1)':1030
         /\ mid_(NewtonDomain.Left param0):1005 = (NewtonDomain.Left param0)':1031
         /\ mid_(NewtonDomain.Left __cost):1006 = (NewtonDomain.Left __cost)':1032
         /\ 0 = K:1022 /\ (K:1004 + K:1022) = K:1033 /\ 0 <= K:1033
         /\ type_err:1034 = (NewtonDomain.Left param1@width)':1026
         /\ type_err:1035 = (NewtonDomain.Left param0@width)':1027
         /\ type_err:1036 = (NewtonDomain.Left param1@pos)':1028
         /\ type_err:1037 = (NewtonDomain.Left param0@pos)':1029
         /\ param1:83 = (NewtonDomain.Left param1)':1030
         /\ param0:80 = (NewtonDomain.Left param0)':1031
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':1032
         /\ 0 <= fresh___cost:1038 /\ 0 <= (fresh___cost:1038 + 1)
         /\ fresh_param0:1039 <= 0
         /\ (!(0 <= K:1040)
               \/ mid_(NewtonDomain.Left param0):1041 = (fresh_param0:1039
                                                           + K:1040))
         /\ (!(0 <= K:1040)
               \/ mid_(NewtonDomain.Left __cost):1042 = (fresh___cost:1038
                                                           + -K:1040))
         /\ ((K:1040 = 0
                /\ type_err:1043 = mid_(NewtonDomain.Right return@width):1044
                /\ type_err:1045 = mid_(NewtonDomain.Right return@pos):1046
                /\ havoc:1047 = mid_(NewtonDomain.Right return):1048
                /\ fresh_param0@width:1049 = mid_(NewtonDomain.Left param0@width):1050
                /\ fresh_param0@pos:1051 = mid_(NewtonDomain.Left param0@pos):1052
                /\ fresh_param0:1039 = mid_(NewtonDomain.Left param0):1041
                /\ fresh___cost:1038 = mid_(NewtonDomain.Left __cost):1042)
               \/ (1 <= K:1040 /\ 0 <= fresh_param0:1039
                     /\ 0 <= (-1 + fresh___cost:1038)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1042
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1041)))
         /\ K:1053 = 0
         /\ mid_(NewtonDomain.Right return@width):1044 = (NewtonDomain.Right return@width)':1054
         /\ mid_(NewtonDomain.Right return@pos):1046 = (NewtonDomain.Right return@pos)':1055
         /\ mid_(NewtonDomain.Right return):1048 = (NewtonDomain.Right return)':1056
         /\ mid_(NewtonDomain.Left param0@width):1050 = (NewtonDomain.Left param0@width)':1057
         /\ mid_(NewtonDomain.Left param0@pos):1052 = (NewtonDomain.Left param0@pos)':1058
         /\ mid_(NewtonDomain.Left param0):1041 = (NewtonDomain.Left param0)':1059
         /\ mid_(NewtonDomain.Left __cost):1042 = (NewtonDomain.Left __cost)':1060
         /\ 0 = K:1053 /\ (K:1040 + K:1053) = K:1061 /\ 0 <= K:1061
         /\ type_err:1062 = (NewtonDomain.Left param0@width)':1057
         /\ type_err:1063 = (NewtonDomain.Left param0@pos)':1058
         /\ (NewtonDomain.Right return)':1025 = (NewtonDomain.Left param0)':1059
         /\ (fresh___cost:1002 + 1) = (NewtonDomain.Left __cost)':1060)}

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

Base relation: 
{__cost := (fresh___cost:1185 + 1)
 y := (NewtonDomain.Right return)':1174
 return := havoc:1209
 param0 := fresh_param0:1186
 param1 := fresh_param1:1157
 return@pos := type_err:1210
 param0@pos := fresh_param0@pos:1198
 param1@pos := fresh_param1@pos:1167
 return@width := type_err:1211
 param0@width := fresh_param0@width:1196
 param1@width := fresh_param1@width:1163
 when (0 <= __cost:101 /\ 0 <= (__cost:101 + 1) /\ 0 <= fresh___cost:1151
         /\ 0 <= (fresh___cost:1151 + 1) /\ fresh_param0:1152 <= 0
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param0):1154 = (fresh_param0:1152
                                                           + K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left __cost):1155 = (fresh___cost:1151
                                                           + -K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Left param1):1156 = (fresh_param1:1157
                                                           + -K:1153))
         /\ (!(0 <= K:1153)
               \/ mid_(NewtonDomain.Right return):1158 = fresh_param1:1157)
         /\ ((K:1153 = 0
                /\ type_err:1159 = mid_(NewtonDomain.Right return@width):1160
                /\ type_err:1161 = mid_(NewtonDomain.Right return@pos):1162
                /\ fresh_param1:1157 = mid_(NewtonDomain.Right return):1158
                /\ fresh_param1@width:1163 = mid_(NewtonDomain.Left param1@width):1164
                /\ fresh_param0@width:1165 = mid_(NewtonDomain.Left param0@width):1166
                /\ fresh_param1@pos:1167 = mid_(NewtonDomain.Left param1@pos):1168
                /\ fresh_param0@pos:1169 = mid_(NewtonDomain.Left param0@pos):1170
                /\ fresh_param1:1157 = mid_(NewtonDomain.Left param1):1156
                /\ fresh_param0:1152 = mid_(NewtonDomain.Left param0):1154
                /\ fresh___cost:1151 = mid_(NewtonDomain.Left __cost):1155)
               \/ (1 <= K:1153 /\ 0 <= fresh_param0:1152
                     /\ 0 <= (-1 + fresh___cost:1151)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1155
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1154)))
         /\ K:1171 = 0
         /\ mid_(NewtonDomain.Right return@width):1160 = (NewtonDomain.Right return@width)':1172
         /\ mid_(NewtonDomain.Right return@pos):1162 = (NewtonDomain.Right return@pos)':1173
         /\ mid_(NewtonDomain.Right return):1158 = (NewtonDomain.Right return)':1174
         /\ mid_(NewtonDomain.Left param1@width):1164 = (NewtonDomain.Left param1@width)':1175
         /\ mid_(NewtonDomain.Left param0@width):1166 = (NewtonDomain.Left param0@width)':1176
         /\ mid_(NewtonDomain.Left param1@pos):1168 = (NewtonDomain.Left param1@pos)':1177
         /\ mid_(NewtonDomain.Left param0@pos):1170 = (NewtonDomain.Left param0@pos)':1178
         /\ mid_(NewtonDomain.Left param1):1156 = (NewtonDomain.Left param1)':1179
         /\ mid_(NewtonDomain.Left param0):1154 = (NewtonDomain.Left param0)':1180
         /\ mid_(NewtonDomain.Left __cost):1155 = (NewtonDomain.Left __cost)':1181
         /\ 0 = K:1171 /\ (K:1153 + K:1171) = K:1182 /\ 0 <= K:1182
         /\ type_err:133 = (NewtonDomain.Left param1@width)':1175
         /\ type_err:132 = (NewtonDomain.Left param0@width)':1176
         /\ type_err:131 = (NewtonDomain.Left param1@pos)':1177
         /\ type_err:130 = (NewtonDomain.Left param0@pos)':1178
         /\ param1:83 = (NewtonDomain.Left param1)':1179
         /\ param0:80 = (NewtonDomain.Left param0)':1180
         /\ (__cost:101 + 1) = (NewtonDomain.Left __cost)':1181
         /\ 0 <= fresh___cost:1185 /\ 0 <= (fresh___cost:1185 + 1)
         /\ fresh_param0:1186 <= 0
         /\ (!(0 <= K:1187)
               \/ mid_(NewtonDomain.Left param0):1188 = (fresh_param0:1186
                                                           + K:1187))
         /\ (!(0 <= K:1187)
               \/ mid_(NewtonDomain.Left __cost):1189 = (fresh___cost:1185
                                                           + -K:1187))
         /\ ((K:1187 = 0
                /\ type_err:1190 = mid_(NewtonDomain.Right return@width):1191
                /\ type_err:1192 = mid_(NewtonDomain.Right return@pos):1193
                /\ havoc:1194 = mid_(NewtonDomain.Right return):1195
                /\ fresh_param0@width:1196 = mid_(NewtonDomain.Left param0@width):1197
                /\ fresh_param0@pos:1198 = mid_(NewtonDomain.Left param0@pos):1199
                /\ fresh_param0:1186 = mid_(NewtonDomain.Left param0):1188
                /\ fresh___cost:1185 = mid_(NewtonDomain.Left __cost):1189)
               \/ (1 <= K:1187 /\ 0 <= fresh_param0:1186
                     /\ 0 <= (-1 + fresh___cost:1185)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):1189
                     /\ 0 <= (-1 + mid_(NewtonDomain.Left param0):1188)))
         /\ K:1200 = 0
         /\ mid_(NewtonDomain.Right return@width):1191 = (NewtonDomain.Right return@width)':1201
         /\ mid_(NewtonDomain.Right return@pos):1193 = (NewtonDomain.Right return@pos)':1202
         /\ mid_(NewtonDomain.Right return):1195 = (NewtonDomain.Right return)':1203
         /\ mid_(NewtonDomain.Left param0@width):1197 = (NewtonDomain.Left param0@width)':1204
         /\ mid_(NewtonDomain.Left param0@pos):1199 = (NewtonDomain.Left param0@pos)':1205
         /\ mid_(NewtonDomain.Left param0):1188 = (NewtonDomain.Left param0)':1206
         /\ mid_(NewtonDomain.Left __cost):1189 = (NewtonDomain.Left __cost)':1207
         /\ 0 = K:1200 /\ (K:1187 + K:1200) = K:1208 /\ 0 <= K:1208
         /\ type_err:1184 = (NewtonDomain.Left param0@width)':1204
         /\ type_err:1183 = (NewtonDomain.Left param0@pos)':1205
         /\ (NewtonDomain.Right return)':1174 = (NewtonDomain.Left param0)':1206
         /\ (fresh___cost:1151 + 1) = (NewtonDomain.Left __cost)':1207)}

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

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

Variable bounds at line 32 in run

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

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