/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, 73> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 79> -> <Unique State Name, 85>	Base relation: 
{return := 0
 return@pos := type_err:92
 return@width := type_err:93
 when ((z:67 < y:68 /\ (y:68 + -z:67) = phi_tmp___1:85)
         \/ (y:68 <= z:67 /\ 0 = phi_tmp___1:85))}	
<Unique State Name, 83> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 55> -> <Unique State Name, 47>	Base relation: 
{}	
<Unique State Name, 69> -> <Unique State Name, 68>	Base relation: 
{param0 := param0:18
 param1 := param1:21
 param0@pos := type_err:163
 param1@pos := type_err:164
 param0@width := type_err:165
 param1@width := type_err:166}	
<Unique State Name, 82> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 74> -> <Unique State Name, 69 73>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 33> -> <Unique State Name, 34>	Base relation: 
{when x:2 <= (y:1 + 1)}	
<Unique State Name, 33> -> <Unique State Name, 62>	Base relation: 
{y := (y:1 + 2)
 param0 := x:2
 param1 := (y:1 + 2)
 param0@pos := type_err:22
 param1@pos := type_err:24
 param0@width := type_err:23
 param1@width := type_err:25
 when (y:1 + 1) < x:2}	
<Unique State Name, 61> -> <Unique State Name, 34>	Base relation: 
{}	
<Unique State Name, 62> -> <Unique State Name, 57 61>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 17> -> <Unique State Name, 80>	Base relation: 
{__cost := 0
 y := havoc:83
 z := havoc:84
 param0 := havoc:83
 param1 := havoc:84
 param0@pos := type_err:88
 param1@pos := type_err:90
 param0@width := type_err:89
 param1@width := type_err:91}	
<Unique State Name, 80> -> <Unique State Name, 75 79>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 57> -> <Unique State Name, 46>	Base relation: 
{__cost := (__cost:0 + 1)
 x := param0:18
 y := param1:21
 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1))}	
<Unique State Name, 85> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 68> -> <Unique State Name, 57 67>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 56> -> <Unique State Name, 63 55>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 84> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 47> -> <Unique State Name, 81>	Base relation: 
{return := havoc:178
 return@pos := type_err:181
 return@width := type_err:182}	
<Unique State Name, 19> -> <Unique State Name, 84>	Base relation: 
{return := havoc:112
 return@pos := type_err:115
 return@width := type_err:116}	
<Unique State Name, 63> -> <Unique State Name, 33>	Base relation: 
{__cost := (__cost:0 + 1)
 x := param0:18
 y := param1:21
 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1))}	
<Unique State Name, 67> -> <Unique State Name, 83>	Base relation: 
{return := havoc:144
 return@pos := type_err:147
 return@width := type_err:148}	
<Unique State Name, 81> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 46> -> <Unique State Name, 47>	Base relation: 
{when x:176 <= y:177}	
<Unique State Name, 46> -> <Unique State Name, 56>	Base relation: 
{x := (x:176 + -1)
 param0 := (x:176 + -1)
 param1 := y:177
 param0@pos := type_err:191
 param1@pos := type_err:193
 param0@width := type_err:192
 param1@width := type_err:194
 when y:177 < x:176}	
<Unique State Name, 75> -> <Unique State Name, 74>	Base relation: 
{param0 := param0:18
 param1 := param1:21
 param0@pos := type_err:131
 param1@pos := type_err:132
 param0@width := type_err:133
 param1@width := type_err:134}	
<Unique State Name, 34> -> <Unique State Name, 82>	Base relation: 
{return := havoc:3
 return@pos := type_err:6
 return@width := type_err:7}	
#################################################################
           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  19  27  34  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       y := havoc:83
       z := havoc:84
       param0 := havoc:83
       param1 := havoc:84
       param0@pos := type_err:88
       param1@pos := type_err:90
       param0@width := type_err:89
       param1@width := type_err:91}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:92
     return@width := type_err:93
     when ((z:67 < y:68 /\ (y:68 + -z:67) = phi_tmp___1:85)
             \/ (y:68 <= z:67 /\ 0 = phi_tmp___1:85))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:18
       param1 := param1:21
       param0@pos := type_err:131
       param1@pos := type_err:132
       param0@width := type_err:133
       param1@width := type_err:134}    )
    ,
    Var(19)
  )
  ,
  Weight(Base relation: 
    {return := havoc:112
     return@pos := type_err:115
     return@width := type_err:116}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=19: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:18
       param1 := param1:21
       param0@pos := type_err:163
       param1@pos := type_err:164
       param0@width := type_err:165
       param1@width := type_err:166}    )
    ,
    Var(27)
  )
  ,
  Weight(Base relation: 
    {return := havoc:144
     return@pos := type_err:147
     return@width := type_err:148}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=27: 
Dot(
  Plus(
    Weight(Base relation: 
      {__cost := (__cost:0 + 1)
       x := param0:18
       y := param1:21
       when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21)}    )
    ,
    Dot(
      Weight(Base relation: 
        {__cost := (__cost:0 + 1)
         x := (param0:18 + -1)
         y := param1:21
         param0 := (param0:18 + -1)
         param1 := param1:21
         param0@pos := type_err:225
         param1@pos := type_err:226
         param0@width := type_err:227
         param1@width := type_err:228
         when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18)}      )
      ,
      Var(34)
    )
  )
  ,
  Weight(Base relation: 
    {return := havoc:178
     return@pos := type_err:181
     return@width := type_err:182}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=34: 
Dot(
  Plus(
    Weight(Base relation: 
      {__cost := (__cost:0 + 1)
       x := param0:18
       y := param1:21
       when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
               /\ param0:18 <= (param1:21 + 1))}    )
    ,
    Dot(
      Weight(Base relation: 
        {__cost := (__cost:0 + 1)
         x := param0:18
         y := (param1:21 + 2)
         param0 := param0:18
         param1 := (param1:21 + 2)
         param0@pos := type_err:229
         param1@pos := type_err:230
         param0@width := type_err:231
         param1@width := type_err:232
         when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                 /\ (param1:21 + 1) < param0:18)}      )
      ,
      Var(27)
    )
  )
  ,
  Weight(Base relation: 
    {return := havoc:3
     return@pos := type_err:6
     return@width := type_err:7}  )
)



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
         y := havoc:83
         z := havoc:84
         param0 := havoc:83
         param1 := havoc:84
         param0@pos := type_err:88
         param1@pos := type_err:90
         param0@width := type_err:89
         param1@width := type_err:91}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:92
       return@width := type_err:93
       when ((z:67 < y:68 /\ (y:68 + -z:67) = phi_tmp___1:85)
               \/ (y:68 <= z:67 /\ 0 = phi_tmp___1:85))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:18
         param1 := param1:21
         param0@pos := type_err:131
         param1@pos := type_err:132
         param0@width := type_err:133
         param1@width := type_err:134}      )
      ,
      Var(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:112
       return@pos := type_err:115
       return@width := type_err:116}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:18
         param1 := param1:21
         param0@pos := type_err:163
         param1@pos := type_err:164
         param0@width := type_err:165
         param1@width := type_err:166}      )
      ,
      Var(27)
    )
    ,
    Weight(Base relation: 
      {return := havoc:144
       return@pos := type_err:147
       return@width := type_err:148}    )
  )
)



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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:0 + 1)
         x := param0:18
         y := param1:21
         when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21)}      )
      ,
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:0 + 1)
           x := (param0:18 + -1)
           y := param1:21
           param0 := (param0:18 + -1)
           param1 := param1:21
           param0@pos := type_err:225
           param1@pos := type_err:226
           param0@width := type_err:227
           param1@width := type_err:228
           when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                   /\ param1:21 < param0:18)}        )
        ,
        Var(34)
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:178
       return@pos := type_err:181
       return@width := type_err:182}    )
  )
)



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

Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:0 + 1)
         x := param0:18
         y := param1:21
         when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                 /\ param0:18 <= (param1:21 + 1))}      )
      ,
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:0 + 1)
           x := param0:18
           y := (param1:21 + 2)
           param0 := param0:18
           param1 := (param1:21 + 2)
           param0@pos := type_err:229
           param1@pos := type_err:230
           param0@width := type_err:231
           param1@width := type_err:232
           when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                   /\ (param1:21 + 1) < param0:18)}        )
        ,
        Project(
          Dot(
            Plus(
              Weight(Base relation: 
                {__cost := (__cost:0 + 1)
                 x := param0:18
                 y := param1:21
                 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                         /\ param0:18 <= param1:21)}              )
              ,
              Dot(
                Weight(Base relation: 
                  {__cost := (__cost:0 + 1)
                   x := (param0:18 + -1)
                   y := param1:21
                   param0 := (param0:18 + -1)
                   param1 := param1:21
                   param0@pos := type_err:225
                   param1@pos := type_err:226
                   param0@width := type_err:227
                   param1@width := type_err:228
                   when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                           /\ param1:21 < param0:18)}                )
                ,
                Var(34)
              )
            )
            ,
            Weight(Base relation: 
              {return := havoc:178
               return@pos := type_err:181
               return@width := type_err:182}            )
          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:3
       return@pos := type_err:6
       return@width := type_err:7}    )
  )
)



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         y := havoc:83
         z := havoc:84
         param0 := havoc:83
         param1 := havoc:84
         param0@pos := type_err:88
         param1@pos := type_err:90
         param0@width := type_err:89
         param1@width := type_err:91}      )
      ,
      Project(
        Dot(
          Dot(
            Weight(Base relation: 
              {param0 := param0:18
               param1 := param1:21
               param0@pos := type_err:131
               param1@pos := type_err:132
               param0@width := type_err:133
               param1@width := type_err:134}            )
            ,
            Project(
              Dot(
                Dot(
                  Weight(Base relation: 
                    {param0 := param0:18
                     param1 := param1:21
                     param0@pos := type_err:163
                     param1@pos := type_err:164
                     param0@width := type_err:165
                     param1@width := type_err:166}                  )
                  ,
                  Project(
                    Dot(
                      Plus(
                        Weight(Base relation: 
                          {__cost := (__cost:0 + 1)
                           x := param0:18
                           y := param1:21
                           when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                   /\ param0:18 <= param1:21)}                        )
                        ,
                        Dot(
                          Weight(Base relation: 
                            {__cost := (__cost:0 + 1)
                             x := (param0:18 + -1)
                             y := param1:21
                             param0 := (param0:18 + -1)
                             param1 := param1:21
                             param0@pos := type_err:225
                             param1@pos := type_err:226
                             param0@width := type_err:227
                             param1@width := type_err:228
                             when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                     /\ param1:21 < param0:18)}                          )
                          ,
                          Detensor(
                            Weight(Base relation: 
                              {__cost := phi___cost:252
                               return := havoc:253
                               param0 := phi_param0:248
                               param1 := phi_param1:247
                               return@pos := type_err:254
                               param0@pos := phi_param0@pos:244
                               param1@pos := phi_param1@pos:243
                               return@width := type_err:255
                               param0@width := phi_param0@width:240
                               param1@width := phi_param1@width:239
                               when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                        /\ param0:18 <= (param1:21 + 1)
                                        /\ (__cost:0 + 1) = phi___cost:252
                                        /\ param1:21 = phi_y:251
                                        /\ return:250 = phi_return:249
                                        /\ param0:18 = phi_param0:248
                                        /\ param1:21 = phi_param1:247
                                        /\ return@pos:246 = phi_return@pos:245
                                        /\ param0@pos:17 = phi_param0@pos:244
                                        /\ param1@pos:20 = phi_param1@pos:243
                                        /\ return@width:242 = phi_return@width:241
                                        /\ param0@width:16 = phi_param0@width:240
                                        /\ param1@width:19 = phi_param1@width:239)
                                       \/ (0 <= __cost:0
                                             /\ 0 <= (__cost:0 + 1)
                                             /\ (param1:21 + 1) < param0:18
                                             /\ 0 <= (__cost:0 + 1)
                                             /\ 0 <= ((__cost:0 + 1) + 1)
                                             /\ param0:18 <= (param1:21 + 2)
                                             /\ ((__cost:0 + 1) + 1) = phi___cost:252
                                             /\ (param1:21 + 2) = phi_y:251
                                             /\ havoc:236 = phi_return:249
                                             /\ param0:18 = phi_param0:248
                                             /\ (param1:21 + 2) = phi_param1:247
                                             /\ type_err:237 = phi_return@pos:245
                                             /\ type_err:229 = phi_param0@pos:244
                                             /\ type_err:230 = phi_param1@pos:243
                                             /\ type_err:238 = phi_return@width:241
                                             /\ type_err:231 = phi_param0@width:240
                                             /\ type_err:232 = phi_param1@width:239))}                            )
                            ,
                            KleeneT( key=1
                              ProjectT(
                                DotT(
                                  ProjectT(
                                    Tensor(
                                      Weight(Base relation: 
                                        {__cost := (__cost:0 + 1)
                                         x := (param0:18 + -1)
                                         y := param1:21
                                         param0 := (param0:18 + -1)
                                         param1 := param1:21
                                         param0@pos := type_err:225
                                         param1@pos := type_err:226
                                         param0@width := type_err:227
                                         param1@width := type_err:228
                                         when (0 <= __cost:0
                                                 /\ 0 <= (__cost:0 + 1)
                                                 /\ param1:21 < param0:18)}                                      )
                                      ,
                                      Weight(Base relation: 
                                        {return := havoc:178
                                         return@pos := type_err:181
                                         return@width := type_err:182}                                      )
                                    )
                                  )
                                  ,
                                  Tensor(
                                    Weight(Base relation: 
                                      {__cost := (__cost:0 + 1)
                                       x := param0:18
                                       y := (param1:21 + 2)
                                       param0 := param0:18
                                       param1 := (param1:21 + 2)
                                       param0@pos := type_err:229
                                       param1@pos := type_err:230
                                       param0@width := type_err:231
                                       param1@width := type_err:232
                                       when (0 <= __cost:0
                                               /\ 0 <= (__cost:0 + 1)
                                               /\ (param1:21 + 1) < param0:18)}                                    )
                                    ,
                                    Weight(Base relation: 
                                      {return := havoc:3
                                       return@pos := type_err:6
                                       return@width := type_err:7}                                    )
                                  )
                                )
                              )
                            )
                          )
                        )
                      )
                      ,
                      Weight(Base relation: 
                        {return := havoc:178
                         return@pos := type_err:181
                         return@width := type_err:182}                      )
                    )
                  )
                )
                ,
                Weight(Base relation: 
                  {return := havoc:144
                   return@pos := type_err:147
                   return@width := type_err:148}                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:112
             return@pos := type_err:115
             return@width := type_err:116}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:92
       return@width := type_err:93
       when ((z:67 < y:68 /\ (y:68 + -z:67) = phi_tmp___1:85)
               \/ (y:68 <= z:67 /\ 0 = phi_tmp___1:85))}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:18
         param1 := param1:21
         param0@pos := type_err:131
         param1@pos := type_err:132
         param0@width := type_err:133
         param1@width := type_err:134}      )
      ,
      Project(
        Dot(
          Dot(
            Weight(Base relation: 
              {param0 := param0:18
               param1 := param1:21
               param0@pos := type_err:163
               param1@pos := type_err:164
               param0@width := type_err:165
               param1@width := type_err:166}            )
            ,
            Project(
              Dot(
                Plus(
                  Weight(Base relation: 
                    {__cost := (__cost:0 + 1)
                     x := param0:18
                     y := param1:21
                     when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                             /\ param0:18 <= param1:21)}                  )
                  ,
                  Dot(
                    Weight(Base relation: 
                      {__cost := (__cost:0 + 1)
                       x := (param0:18 + -1)
                       y := param1:21
                       param0 := (param0:18 + -1)
                       param1 := param1:21
                       param0@pos := type_err:225
                       param1@pos := type_err:226
                       param0@width := type_err:227
                       param1@width := type_err:228
                       when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                               /\ param1:21 < param0:18)}                    )
                    ,
                    Detensor(
                      Weight(Base relation: 
                        {__cost := phi___cost:252
                         return := havoc:253
                         param0 := phi_param0:248
                         param1 := phi_param1:247
                         return@pos := type_err:254
                         param0@pos := phi_param0@pos:244
                         param1@pos := phi_param1@pos:243
                         return@width := type_err:255
                         param0@width := phi_param0@width:240
                         param1@width := phi_param1@width:239
                         when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                  /\ param0:18 <= (param1:21 + 1)
                                  /\ (__cost:0 + 1) = phi___cost:252
                                  /\ param1:21 = phi_y:251
                                  /\ return:250 = phi_return:249
                                  /\ param0:18 = phi_param0:248
                                  /\ param1:21 = phi_param1:247
                                  /\ return@pos:246 = phi_return@pos:245
                                  /\ param0@pos:17 = phi_param0@pos:244
                                  /\ param1@pos:20 = phi_param1@pos:243
                                  /\ return@width:242 = phi_return@width:241
                                  /\ param0@width:16 = phi_param0@width:240
                                  /\ param1@width:19 = phi_param1@width:239)
                                 \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                       /\ (param1:21 + 1) < param0:18
                                       /\ 0 <= (__cost:0 + 1)
                                       /\ 0 <= ((__cost:0 + 1) + 1)
                                       /\ param0:18 <= (param1:21 + 2)
                                       /\ ((__cost:0 + 1) + 1) = phi___cost:252
                                       /\ (param1:21 + 2) = phi_y:251
                                       /\ havoc:236 = phi_return:249
                                       /\ param0:18 = phi_param0:248
                                       /\ (param1:21 + 2) = phi_param1:247
                                       /\ type_err:237 = phi_return@pos:245
                                       /\ type_err:229 = phi_param0@pos:244
                                       /\ type_err:230 = phi_param1@pos:243
                                       /\ type_err:238 = phi_return@width:241
                                       /\ type_err:231 = phi_param0@width:240
                                       /\ type_err:232 = phi_param1@width:239))}                      )
                      ,
                      KleeneT( key=1
                        ProjectT(
                          DotT(
                            ProjectT(
                              Tensor(
                                Weight(Base relation: 
                                  {__cost := (__cost:0 + 1)
                                   x := (param0:18 + -1)
                                   y := param1:21
                                   param0 := (param0:18 + -1)
                                   param1 := param1:21
                                   param0@pos := type_err:225
                                   param1@pos := type_err:226
                                   param0@width := type_err:227
                                   param1@width := type_err:228
                                   when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                           /\ param1:21 < param0:18)}                                )
                                ,
                                Weight(Base relation: 
                                  {return := havoc:178
                                   return@pos := type_err:181
                                   return@width := type_err:182}                                )
                              )
                            )
                            ,
                            Tensor(
                              Weight(Base relation: 
                                {__cost := (__cost:0 + 1)
                                 x := param0:18
                                 y := (param1:21 + 2)
                                 param0 := param0:18
                                 param1 := (param1:21 + 2)
                                 param0@pos := type_err:229
                                 param1@pos := type_err:230
                                 param0@width := type_err:231
                                 param1@width := type_err:232
                                 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                         /\ (param1:21 + 1) < param0:18)}                              )
                              ,
                              Weight(Base relation: 
                                {return := havoc:3
                                 return@pos := type_err:6
                                 return@width := type_err:7}                              )
                            )
                          )
                        )
                      )
                    )
                  )
                )
                ,
                Weight(Base relation: 
                  {return := havoc:178
                   return@pos := type_err:181
                   return@width := type_err:182}                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:144
             return@pos := type_err:147
             return@width := type_err:148}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:112
       return@pos := type_err:115
       return@width := type_err:116}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:18
         param1 := param1:21
         param0@pos := type_err:163
         param1@pos := type_err:164
         param0@width := type_err:165
         param1@width := type_err:166}      )
      ,
      Project(
        Dot(
          Plus(
            Weight(Base relation: 
              {__cost := (__cost:0 + 1)
               x := param0:18
               y := param1:21
               when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                       /\ param0:18 <= param1:21)}            )
            ,
            Dot(
              Weight(Base relation: 
                {__cost := (__cost:0 + 1)
                 x := (param0:18 + -1)
                 y := param1:21
                 param0 := (param0:18 + -1)
                 param1 := param1:21
                 param0@pos := type_err:225
                 param1@pos := type_err:226
                 param0@width := type_err:227
                 param1@width := type_err:228
                 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                         /\ param1:21 < param0:18)}              )
              ,
              Detensor(
                Weight(Base relation: 
                  {__cost := phi___cost:252
                   return := havoc:253
                   param0 := phi_param0:248
                   param1 := phi_param1:247
                   return@pos := type_err:254
                   param0@pos := phi_param0@pos:244
                   param1@pos := phi_param1@pos:243
                   return@width := type_err:255
                   param0@width := phi_param0@width:240
                   param1@width := phi_param1@width:239
                   when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                            /\ param0:18 <= (param1:21 + 1)
                            /\ (__cost:0 + 1) = phi___cost:252
                            /\ param1:21 = phi_y:251
                            /\ return:250 = phi_return:249
                            /\ param0:18 = phi_param0:248
                            /\ param1:21 = phi_param1:247
                            /\ return@pos:246 = phi_return@pos:245
                            /\ param0@pos:17 = phi_param0@pos:244
                            /\ param1@pos:20 = phi_param1@pos:243
                            /\ return@width:242 = phi_return@width:241
                            /\ param0@width:16 = phi_param0@width:240
                            /\ param1@width:19 = phi_param1@width:239)
                           \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                 /\ (param1:21 + 1) < param0:18
                                 /\ 0 <= (__cost:0 + 1)
                                 /\ 0 <= ((__cost:0 + 1) + 1)
                                 /\ param0:18 <= (param1:21 + 2)
                                 /\ ((__cost:0 + 1) + 1) = phi___cost:252
                                 /\ (param1:21 + 2) = phi_y:251
                                 /\ havoc:236 = phi_return:249
                                 /\ param0:18 = phi_param0:248
                                 /\ (param1:21 + 2) = phi_param1:247
                                 /\ type_err:237 = phi_return@pos:245
                                 /\ type_err:229 = phi_param0@pos:244
                                 /\ type_err:230 = phi_param1@pos:243
                                 /\ type_err:238 = phi_return@width:241
                                 /\ type_err:231 = phi_param0@width:240
                                 /\ type_err:232 = phi_param1@width:239))}                )
                ,
                KleeneT( key=1
                  ProjectT(
                    DotT(
                      ProjectT(
                        Tensor(
                          Weight(Base relation: 
                            {__cost := (__cost:0 + 1)
                             x := (param0:18 + -1)
                             y := param1:21
                             param0 := (param0:18 + -1)
                             param1 := param1:21
                             param0@pos := type_err:225
                             param1@pos := type_err:226
                             param0@width := type_err:227
                             param1@width := type_err:228
                             when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                     /\ param1:21 < param0:18)}                          )
                          ,
                          Weight(Base relation: 
                            {return := havoc:178
                             return@pos := type_err:181
                             return@width := type_err:182}                          )
                        )
                      )
                      ,
                      Tensor(
                        Weight(Base relation: 
                          {__cost := (__cost:0 + 1)
                           x := param0:18
                           y := (param1:21 + 2)
                           param0 := param0:18
                           param1 := (param1:21 + 2)
                           param0@pos := type_err:229
                           param1@pos := type_err:230
                           param0@width := type_err:231
                           param1@width := type_err:232
                           when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                                   /\ (param1:21 + 1) < param0:18)}                        )
                        ,
                        Weight(Base relation: 
                          {return := havoc:3
                           return@pos := type_err:6
                           return@width := type_err:7}                        )
                      )
                    )
                  )
                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:178
             return@pos := type_err:181
             return@width := type_err:182}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:144
       return@pos := type_err:147
       return@width := type_err:148}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=27: 
Project(
  Dot(
    Plus(
      Weight(Base relation: 
        {__cost := (__cost:0 + 1)
         x := param0:18
         y := param1:21
         when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21)}      )
      ,
      Dot(
        Weight(Base relation: 
          {__cost := (__cost:0 + 1)
           x := (param0:18 + -1)
           y := param1:21
           param0 := (param0:18 + -1)
           param1 := param1:21
           param0@pos := type_err:225
           param1@pos := type_err:226
           param0@width := type_err:227
           param1@width := type_err:228
           when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                   /\ param1:21 < param0:18)}        )
        ,
        Detensor(
          Weight(Base relation: 
            {__cost := phi___cost:252
             return := havoc:253
             param0 := phi_param0:248
             param1 := phi_param1:247
             return@pos := type_err:254
             param0@pos := phi_param0@pos:244
             param1@pos := phi_param1@pos:243
             return@width := type_err:255
             param0@width := phi_param0@width:240
             param1@width := phi_param1@width:239
             when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                      /\ param0:18 <= (param1:21 + 1)
                      /\ (__cost:0 + 1) = phi___cost:252
                      /\ param1:21 = phi_y:251 /\ return:250 = phi_return:249
                      /\ param0:18 = phi_param0:248
                      /\ param1:21 = phi_param1:247
                      /\ return@pos:246 = phi_return@pos:245
                      /\ param0@pos:17 = phi_param0@pos:244
                      /\ param1@pos:20 = phi_param1@pos:243
                      /\ return@width:242 = phi_return@width:241
                      /\ param0@width:16 = phi_param0@width:240
                      /\ param1@width:19 = phi_param1@width:239)
                     \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                           /\ (param1:21 + 1) < param0:18
                           /\ 0 <= (__cost:0 + 1)
                           /\ 0 <= ((__cost:0 + 1) + 1)
                           /\ param0:18 <= (param1:21 + 2)
                           /\ ((__cost:0 + 1) + 1) = phi___cost:252
                           /\ (param1:21 + 2) = phi_y:251
                           /\ havoc:236 = phi_return:249
                           /\ param0:18 = phi_param0:248
                           /\ (param1:21 + 2) = phi_param1:247
                           /\ type_err:237 = phi_return@pos:245
                           /\ type_err:229 = phi_param0@pos:244
                           /\ type_err:230 = phi_param1@pos:243
                           /\ type_err:238 = phi_return@width:241
                           /\ type_err:231 = phi_param0@width:240
                           /\ type_err:232 = phi_param1@width:239))}          )
          ,
          KleeneT( key=1
            ProjectT(
              DotT(
                ProjectT(
                  Tensor(
                    Weight(Base relation: 
                      {__cost := (__cost:0 + 1)
                       x := (param0:18 + -1)
                       y := param1:21
                       param0 := (param0:18 + -1)
                       param1 := param1:21
                       param0@pos := type_err:225
                       param1@pos := type_err:226
                       param0@width := type_err:227
                       param1@width := type_err:228
                       when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                               /\ param1:21 < param0:18)}                    )
                    ,
                    Weight(Base relation: 
                      {return := havoc:178
                       return@pos := type_err:181
                       return@width := type_err:182}                    )
                  )
                )
                ,
                Tensor(
                  Weight(Base relation: 
                    {__cost := (__cost:0 + 1)
                     x := param0:18
                     y := (param1:21 + 2)
                     param0 := param0:18
                     param1 := (param1:21 + 2)
                     param0@pos := type_err:229
                     param1@pos := type_err:230
                     param0@width := type_err:231
                     param1@width := type_err:232
                     when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                             /\ (param1:21 + 1) < param0:18)}                  )
                  ,
                  Weight(Base relation: 
                    {return := havoc:3
                     return@pos := type_err:6
                     return@width := type_err:7}                  )
                )
              )
            )
          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:178
       return@pos := type_err:181
       return@width := type_err:182}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=34: 
Detensor(
  Weight(Base relation: 
    {__cost := phi___cost:252
     return := havoc:253
     param0 := phi_param0:248
     param1 := phi_param1:247
     return@pos := type_err:254
     param0@pos := phi_param0@pos:244
     param1@pos := phi_param1@pos:243
     return@width := type_err:255
     param0@width := phi_param0@width:240
     param1@width := phi_param1@width:239
     when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
              /\ param0:18 <= (param1:21 + 1)
              /\ (__cost:0 + 1) = phi___cost:252 /\ param1:21 = phi_y:251
              /\ return:250 = phi_return:249 /\ param0:18 = phi_param0:248
              /\ param1:21 = phi_param1:247
              /\ return@pos:246 = phi_return@pos:245
              /\ param0@pos:17 = phi_param0@pos:244
              /\ param1@pos:20 = phi_param1@pos:243
              /\ return@width:242 = phi_return@width:241
              /\ param0@width:16 = phi_param0@width:240
              /\ param1@width:19 = phi_param1@width:239)
             \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                   /\ (param1:21 + 1) < param0:18 /\ 0 <= (__cost:0 + 1)
                   /\ 0 <= ((__cost:0 + 1) + 1)
                   /\ param0:18 <= (param1:21 + 2)
                   /\ ((__cost:0 + 1) + 1) = phi___cost:252
                   /\ (param1:21 + 2) = phi_y:251
                   /\ havoc:236 = phi_return:249
                   /\ param0:18 = phi_param0:248
                   /\ (param1:21 + 2) = phi_param1:247
                   /\ type_err:237 = phi_return@pos:245
                   /\ type_err:229 = phi_param0@pos:244
                   /\ type_err:230 = phi_param1@pos:243
                   /\ type_err:238 = phi_return@width:241
                   /\ type_err:231 = phi_param0@width:240
                   /\ type_err:232 = phi_param1@width:239))}  )
  ,
  KleeneT( key=1
    ProjectT(
      DotT(
        ProjectT(
          Tensor(
            Weight(Base relation: 
              {__cost := (__cost:0 + 1)
               x := (param0:18 + -1)
               y := param1:21
               param0 := (param0:18 + -1)
               param1 := param1:21
               param0@pos := type_err:225
               param1@pos := type_err:226
               param0@width := type_err:227
               param1@width := type_err:228
               when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                       /\ param1:21 < param0:18)}            )
            ,
            Weight(Base relation: 
              {return := havoc:178
               return@pos := type_err:181
               return@width := type_err:182}            )
          )
        )
        ,
        Tensor(
          Weight(Base relation: 
            {__cost := (__cost:0 + 1)
             x := param0:18
             y := (param1:21 + 2)
             param0 := param0:18
             param1 := (param1:21 + 2)
             param0@pos := type_err:229
             param1@pos := type_err:230
             param0@width := type_err:231
             param1@width := type_err:232
             when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
                     /\ (param1:21 + 1) < param0:18)}          )
          ,
          Weight(Base relation: 
            {return := havoc:3
             return@pos := type_err:6
             return@width := type_err:7}          )
        )
      )
    )
  )
)


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:289
 (NewtonDomain.Left param0) := fresh_param0:291
 (NewtonDomain.Left param1) := fresh_param1:290
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:298
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:299
 (NewtonDomain.Left param0@width) := fresh_param0@width:300
 (NewtonDomain.Left param1@width) := fresh_param1@width:301
 (NewtonDomain.Right return) := havoc:302
 (NewtonDomain.Right return@pos) := type_err:303
 (NewtonDomain.Right return@width) := type_err:304
 when (0 <= fresh___cost:256 /\ 0 <= (fresh___cost:256 + 1)
         /\ fresh_param1:260 < fresh_param0:259
         /\ (NewtonDomain.Left __cost):265 = (fresh___cost:256 + 1)
         /\ (NewtonDomain.Right x):276 = (fresh_param0:259 + -1)
         /\ (NewtonDomain.Right y):277 = fresh_param1:260
         /\ (NewtonDomain.Left param0):268 = (fresh_param0:259 + -1)
         /\ (NewtonDomain.Left param1):269 = fresh_param1:260
         /\ (NewtonDomain.Left param0@pos):270 = type_err:225
         /\ (NewtonDomain.Left param1@pos):271 = type_err:226
         /\ (NewtonDomain.Left param0@width):272 = type_err:227
         /\ (NewtonDomain.Left param1@width):273 = type_err:228
         /\ 0 <= fresh___cost:289 /\ 0 <= (fresh___cost:289 + 1)
         /\ (fresh_param1:290 + 1) < fresh_param0:291
         /\ fresh___cost:256 = (fresh___cost:289 + 1)
         /\ (NewtonDomain.Right x):307 = fresh_param0:291
         /\ (NewtonDomain.Right y):308 = (fresh_param1:290 + 2)
         /\ fresh_param0:259 = fresh_param0:291
         /\ fresh_param1:260 = (fresh_param1:290 + 2)
         /\ fresh_param0@pos:261 = type_err:292
         /\ fresh_param1@pos:262 = type_err:293
         /\ fresh_param0@width:263 = type_err:294
         /\ fresh_param1@width:264 = type_err:295)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':310) = (1)*((NewtonDomain.Left param0):268)
                                                 + 1
           ((NewtonDomain.Left param1)':311) = (1)*((NewtonDomain.Left param1):269)
                                                + (-2)*1
           ((NewtonDomain.Left __cost)':309) = (1)*((NewtonDomain.Left __cost):265)
                                                + (-2)*1
           }
          pre:
            [|(NewtonDomain.Left __cost):265-2>=0;
              (NewtonDomain.Left param0):268-(NewtonDomain.Left param1):269>=0|]
          post:
            [|(NewtonDomain.Left __cost)':309>=0;
              (NewtonDomain.Left param0)':310-(NewtonDomain.Left param1)':311
              -3>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':309
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':310
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':311
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':312
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':313
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':314
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':315
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':317
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':319
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':321
   when ((!(0 <= K:346)
            \/ mid_(NewtonDomain.Left param0):356 = ((NewtonDomain.Left param0):268
                                                       + K:346))
           /\ (!(0 <= K:346)
                 \/ mid_(NewtonDomain.Left param1):355 = ((NewtonDomain.Left param1):269
                                                            + (-2 * K:346)))
           /\ (!(0 <= K:346)
                 \/ mid_(NewtonDomain.Left __cost):357 = ((NewtonDomain.Left __cost):265
                                                            + (-2 * K:346)))
           /\ ((K:346 = 0
                  /\ (NewtonDomain.Right return@width):320 = mid_(NewtonDomain.Right return@width):348
                  /\ (NewtonDomain.Right return@pos):318 = mid_(NewtonDomain.Right return@pos):349
                  /\ (NewtonDomain.Right return):316 = mid_(NewtonDomain.Right return):350
                  /\ (NewtonDomain.Left param1@width):273 = mid_(NewtonDomain.Left param1@width):351
                  /\ (NewtonDomain.Left param0@width):272 = mid_(NewtonDomain.Left param0@width):352
                  /\ (NewtonDomain.Left param1@pos):271 = mid_(NewtonDomain.Left param1@pos):353
                  /\ (NewtonDomain.Left param0@pos):270 = mid_(NewtonDomain.Left param0@pos):354
                  /\ (NewtonDomain.Left param1):269 = mid_(NewtonDomain.Left param1):355
                  /\ (NewtonDomain.Left param0):268 = mid_(NewtonDomain.Left param0):356
                  /\ (NewtonDomain.Left __cost):265 = mid_(NewtonDomain.Left __cost):357)
                 \/ (1 <= K:346 /\ 0 <= (-2 + (NewtonDomain.Left __cost):265)
                       /\ 0 <= ((NewtonDomain.Left param0):268
                                  + -(NewtonDomain.Left param1):269)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):357
                       /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):356
                                  + -mid_(NewtonDomain.Left param1):355)))
           /\ K:347 = 0
           /\ mid_(NewtonDomain.Right return@width):348 = (NewtonDomain.Right return@width)':321
           /\ mid_(NewtonDomain.Right return@pos):349 = (NewtonDomain.Right return@pos)':319
           /\ mid_(NewtonDomain.Right return):350 = (NewtonDomain.Right return)':317
           /\ mid_(NewtonDomain.Left param1@width):351 = (NewtonDomain.Left param1@width)':315
           /\ mid_(NewtonDomain.Left param0@width):352 = (NewtonDomain.Left param0@width)':314
           /\ mid_(NewtonDomain.Left param1@pos):353 = (NewtonDomain.Left param1@pos)':313
           /\ mid_(NewtonDomain.Left param0@pos):354 = (NewtonDomain.Left param0@pos)':312
           /\ mid_(NewtonDomain.Left param1):355 = (NewtonDomain.Left param1)':311
           /\ mid_(NewtonDomain.Left param0):356 = (NewtonDomain.Left param0)':310
           /\ mid_(NewtonDomain.Left __cost):357 = (NewtonDomain.Left __cost)':309
           /\ 0 = K:347 /\ (K:346 + K:347) = K:345 /\ 0 <= K:345)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:608
 return := 0
 param0 := phi_param0:611
 param1 := phi_param1:612
 return@pos := type_err:682
 param0@pos := phi_param0@pos:615
 param1@pos := phi_param1@pos:617
 return@width := type_err:683
 param0@width := phi_param0@width:620
 param1@width := phi_param1@width:622
 when (((havoc:83 <= havoc:84 /\ 1 = phi___cost:608 /\ havoc:83 = phi_x:609
           /\ return:250 = phi_return:610 /\ havoc:83 = phi_param0:611
           /\ havoc:84 = phi_param1:612
           /\ return@pos:246 = phi_return@pos:613
           /\ type_err:614 = phi_param0@pos:615
           /\ type_err:616 = phi_param1@pos:617
           /\ return@width:242 = phi_return@width:618
           /\ type_err:619 = phi_param0@width:620
           /\ type_err:621 = phi_param1@width:622)
          \/ (havoc:84 < havoc:83
                /\ ((0 <= fresh___cost:623 /\ 0 <= (fresh___cost:623 + 1)
                       /\ fresh_param0:624 <= (fresh_param1:625 + 1)
                       /\ (fresh___cost:623 + 1) = phi___cost:626
                       /\ fresh_param1:625 = phi_y:627
                       /\ return:250 = phi_return:628
                       /\ fresh_param0:624 = phi_param0:629
                       /\ fresh_param1:625 = phi_param1:630
                       /\ return@pos:246 = phi_return@pos:631
                       /\ fresh_param0@pos:632 = phi_param0@pos:633
                       /\ fresh_param1@pos:634 = phi_param1@pos:635
                       /\ return@width:242 = phi_return@width:636
                       /\ fresh_param0@width:637 = phi_param0@width:638
                       /\ fresh_param1@width:639 = phi_param1@width:640)
                      \/ (0 <= fresh___cost:623
                            /\ 0 <= (fresh___cost:623 + 1)
                            /\ (fresh_param1:625 + 1) < fresh_param0:624
                            /\ 0 <= (fresh___cost:623 + 1)
                            /\ 0 <= ((fresh___cost:623 + 1) + 1)
                            /\ fresh_param0:624 <= (fresh_param1:625 + 2)
                            /\ ((fresh___cost:623 + 1) + 1) = phi___cost:626
                            /\ (fresh_param1:625 + 2) = phi_y:627
                            /\ havoc:641 = phi_return:628
                            /\ fresh_param0:624 = phi_param0:629
                            /\ (fresh_param1:625 + 2) = phi_param1:630
                            /\ type_err:642 = phi_return@pos:631
                            /\ type_err:643 = phi_param0@pos:633
                            /\ type_err:644 = phi_param1@pos:635
                            /\ type_err:645 = phi_return@width:636
                            /\ type_err:646 = phi_param0@width:638
                            /\ type_err:647 = phi_param1@width:640))
                /\ (!(0 <= K:648)
                      \/ mid_(NewtonDomain.Left param0):649 = (fresh_param0:624
                                                                 + K:648))
                /\ (!(0 <= K:648)
                      \/ mid_(NewtonDomain.Left param1):650 = (fresh_param1:625
                                                                 + (-2
                                                                    * K:648)))
                /\ (!(0 <= K:648)
                      \/ mid_(NewtonDomain.Left __cost):651 = (fresh___cost:623
                                                                 + (-2
                                                                    * K:648)))
                /\ ((K:648 = 0
                       /\ type_err:652 = mid_(NewtonDomain.Right return@width):653
                       /\ type_err:654 = mid_(NewtonDomain.Right return@pos):655
                       /\ havoc:656 = mid_(NewtonDomain.Right return):657
                       /\ fresh_param1@width:639 = mid_(NewtonDomain.Left param1@width):658
                       /\ fresh_param0@width:637 = mid_(NewtonDomain.Left param0@width):659
                       /\ fresh_param1@pos:634 = mid_(NewtonDomain.Left param1@pos):660
                       /\ fresh_param0@pos:632 = mid_(NewtonDomain.Left param0@pos):661
                       /\ fresh_param1:625 = mid_(NewtonDomain.Left param1):650
                       /\ fresh_param0:624 = mid_(NewtonDomain.Left param0):649
                       /\ fresh___cost:623 = mid_(NewtonDomain.Left __cost):651)
                      \/ (1 <= K:648 /\ 0 <= (-2 + fresh___cost:623)
                            /\ 0 <= (fresh_param0:624 + -fresh_param1:625)
                            /\ 0 <= mid_(NewtonDomain.Left __cost):651
                            /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):649
                                       + -mid_(NewtonDomain.Left param1):650)))
                /\ K:662 = 0
                /\ mid_(NewtonDomain.Right return@width):653 = (NewtonDomain.Right return@width)':663
                /\ mid_(NewtonDomain.Right return@pos):655 = (NewtonDomain.Right return@pos)':664
                /\ mid_(NewtonDomain.Right return):657 = (NewtonDomain.Right return)':665
                /\ mid_(NewtonDomain.Left param1@width):658 = (NewtonDomain.Left param1@width)':666
                /\ mid_(NewtonDomain.Left param0@width):659 = (NewtonDomain.Left param0@width)':667
                /\ mid_(NewtonDomain.Left param1@pos):660 = (NewtonDomain.Left param1@pos)':668
                /\ mid_(NewtonDomain.Left param0@pos):661 = (NewtonDomain.Left param0@pos)':669
                /\ mid_(NewtonDomain.Left param1):650 = (NewtonDomain.Left param1)':670
                /\ mid_(NewtonDomain.Left param0):649 = (NewtonDomain.Left param0)':671
                /\ mid_(NewtonDomain.Left __cost):651 = (NewtonDomain.Left __cost)':672
                /\ 0 = K:662 /\ (K:648 + K:662) = K:673 /\ 0 <= K:673
                /\ type_err:674 = (NewtonDomain.Left param1@width)':666
                /\ type_err:675 = (NewtonDomain.Left param0@width)':667
                /\ type_err:676 = (NewtonDomain.Left param1@pos)':668
                /\ type_err:677 = (NewtonDomain.Left param0@pos)':669
                /\ havoc:84 = (NewtonDomain.Left param1)':670
                /\ (havoc:83 + -1) = (NewtonDomain.Left param0)':671
                /\ 1 = (NewtonDomain.Left __cost)':672
                /\ phi___cost:626 = phi___cost:608
                /\ (havoc:83 + -1) = phi_x:609
                /\ (NewtonDomain.Right return)':665 = phi_return:610
                /\ phi_param0:629 = phi_param0:611
                /\ phi_param1:630 = phi_param1:612
                /\ (NewtonDomain.Right return@pos)':664 = phi_return@pos:613
                /\ phi_param0@pos:633 = phi_param0@pos:615
                /\ phi_param1@pos:635 = phi_param1@pos:617
                /\ (NewtonDomain.Right return@width)':663 = phi_return@width:618
                /\ phi_param0@width:638 = phi_param0@width:620
                /\ phi_param1@width:640 = phi_param1@width:622))
         /\ ((havoc:84 < havoc:83 /\ (havoc:83 + -havoc:84) = phi_tmp___1:681)
               \/ (havoc:83 <= havoc:84 /\ 0 = phi_tmp___1:681)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:532
 return := havoc:605
 param0 := phi_param0:535
 param1 := phi_param1:536
 return@pos := type_err:606
 param0@pos := phi_param0@pos:539
 param1@pos := phi_param1@pos:541
 return@width := type_err:607
 param0@width := phi_param0@width:544
 param1@width := phi_param1@width:546
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:532 /\ param0:18 = phi_x:533
          /\ return:250 = phi_return:534 /\ param0:18 = phi_param0:535
          /\ param1:21 = phi_param1:536
          /\ return@pos:246 = phi_return@pos:537
          /\ type_err:538 = phi_param0@pos:539
          /\ type_err:540 = phi_param1@pos:541
          /\ return@width:242 = phi_return@width:542
          /\ type_err:543 = phi_param0@width:544
          /\ type_err:545 = phi_param1@width:546)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:547 /\ 0 <= (fresh___cost:547 + 1)
                      /\ fresh_param0:548 <= (fresh_param1:549 + 1)
                      /\ (fresh___cost:547 + 1) = phi___cost:550
                      /\ fresh_param1:549 = phi_y:551
                      /\ return:250 = phi_return:552
                      /\ fresh_param0:548 = phi_param0:553
                      /\ fresh_param1:549 = phi_param1:554
                      /\ return@pos:246 = phi_return@pos:555
                      /\ fresh_param0@pos:556 = phi_param0@pos:557
                      /\ fresh_param1@pos:558 = phi_param1@pos:559
                      /\ return@width:242 = phi_return@width:560
                      /\ fresh_param0@width:561 = phi_param0@width:562
                      /\ fresh_param1@width:563 = phi_param1@width:564)
                     \/ (0 <= fresh___cost:547 /\ 0 <= (fresh___cost:547 + 1)
                           /\ (fresh_param1:549 + 1) < fresh_param0:548
                           /\ 0 <= (fresh___cost:547 + 1)
                           /\ 0 <= ((fresh___cost:547 + 1) + 1)
                           /\ fresh_param0:548 <= (fresh_param1:549 + 2)
                           /\ ((fresh___cost:547 + 1) + 1) = phi___cost:550
                           /\ (fresh_param1:549 + 2) = phi_y:551
                           /\ havoc:565 = phi_return:552
                           /\ fresh_param0:548 = phi_param0:553
                           /\ (fresh_param1:549 + 2) = phi_param1:554
                           /\ type_err:566 = phi_return@pos:555
                           /\ type_err:567 = phi_param0@pos:557
                           /\ type_err:568 = phi_param1@pos:559
                           /\ type_err:569 = phi_return@width:560
                           /\ type_err:570 = phi_param0@width:562
                           /\ type_err:571 = phi_param1@width:564))
               /\ (!(0 <= K:572)
                     \/ mid_(NewtonDomain.Left param0):573 = (fresh_param0:548
                                                                + K:572))
               /\ (!(0 <= K:572)
                     \/ mid_(NewtonDomain.Left param1):574 = (fresh_param1:549
                                                                + (-2 * K:572)))
               /\ (!(0 <= K:572)
                     \/ mid_(NewtonDomain.Left __cost):575 = (fresh___cost:547
                                                                + (-2 * K:572)))
               /\ ((K:572 = 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_param1@width:563 = mid_(NewtonDomain.Left param1@width):582
                      /\ fresh_param0@width:561 = mid_(NewtonDomain.Left param0@width):583
                      /\ fresh_param1@pos:558 = mid_(NewtonDomain.Left param1@pos):584
                      /\ fresh_param0@pos:556 = mid_(NewtonDomain.Left param0@pos):585
                      /\ fresh_param1:549 = mid_(NewtonDomain.Left param1):574
                      /\ fresh_param0:548 = mid_(NewtonDomain.Left param0):573
                      /\ fresh___cost:547 = mid_(NewtonDomain.Left __cost):575)
                     \/ (1 <= K:572 /\ 0 <= (-2 + fresh___cost:547)
                           /\ 0 <= (fresh_param0:548 + -fresh_param1:549)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):575
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):573
                                      + -mid_(NewtonDomain.Left param1):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 param1@width):582 = (NewtonDomain.Left param1@width)':590
               /\ mid_(NewtonDomain.Left param0@width):583 = (NewtonDomain.Left param0@width)':591
               /\ mid_(NewtonDomain.Left param1@pos):584 = (NewtonDomain.Left param1@pos)':592
               /\ mid_(NewtonDomain.Left param0@pos):585 = (NewtonDomain.Left param0@pos)':593
               /\ mid_(NewtonDomain.Left param1):574 = (NewtonDomain.Left param1)':594
               /\ mid_(NewtonDomain.Left param0):573 = (NewtonDomain.Left param0)':595
               /\ mid_(NewtonDomain.Left __cost):575 = (NewtonDomain.Left __cost)':596
               /\ 0 = K:586 /\ (K:572 + K:586) = K:597 /\ 0 <= K:597
               /\ type_err:598 = (NewtonDomain.Left param1@width)':590
               /\ type_err:599 = (NewtonDomain.Left param0@width)':591
               /\ type_err:600 = (NewtonDomain.Left param1@pos)':592
               /\ type_err:601 = (NewtonDomain.Left param0@pos)':593
               /\ param1:21 = (NewtonDomain.Left param1)':594
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':595
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':596
               /\ phi___cost:550 = phi___cost:532
               /\ (param0:18 + -1) = phi_x:533
               /\ (NewtonDomain.Right return)':589 = phi_return:534
               /\ phi_param0:553 = phi_param0:535
               /\ phi_param1:554 = phi_param1:536
               /\ (NewtonDomain.Right return@pos)':588 = phi_return@pos:537
               /\ phi_param0@pos:557 = phi_param0@pos:539
               /\ phi_param1@pos:559 = phi_param1@pos:541
               /\ (NewtonDomain.Right return@width)':587 = phi_return@width:542
               /\ phi_param0@width:562 = phi_param0@width:544
               /\ phi_param1@width:564 = phi_param1@width:546))}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:460
 return := havoc:529
 param0 := phi_param0:463
 param1 := phi_param1:464
 return@pos := type_err:530
 param0@pos := phi_param0@pos:466
 param1@pos := phi_param1@pos:467
 return@width := type_err:531
 param0@width := phi_param0@width:469
 param1@width := phi_param1@width:470
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:460 /\ param0:18 = phi_x:461
          /\ return:250 = phi_return:462 /\ param0:18 = phi_param0:463
          /\ param1:21 = phi_param1:464
          /\ return@pos:246 = phi_return@pos:465
          /\ type_err:163 = phi_param0@pos:466
          /\ type_err:164 = phi_param1@pos:467
          /\ return@width:242 = phi_return@width:468
          /\ type_err:165 = phi_param0@width:469
          /\ type_err:166 = phi_param1@width:470)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:471 /\ 0 <= (fresh___cost:471 + 1)
                      /\ fresh_param0:472 <= (fresh_param1:473 + 1)
                      /\ (fresh___cost:471 + 1) = phi___cost:474
                      /\ fresh_param1:473 = phi_y:475
                      /\ return:250 = phi_return:476
                      /\ fresh_param0:472 = phi_param0:477
                      /\ fresh_param1:473 = phi_param1:478
                      /\ return@pos:246 = phi_return@pos:479
                      /\ fresh_param0@pos:480 = phi_param0@pos:481
                      /\ fresh_param1@pos:482 = phi_param1@pos:483
                      /\ return@width:242 = phi_return@width:484
                      /\ fresh_param0@width:485 = phi_param0@width:486
                      /\ fresh_param1@width:487 = phi_param1@width:488)
                     \/ (0 <= fresh___cost:471 /\ 0 <= (fresh___cost:471 + 1)
                           /\ (fresh_param1:473 + 1) < fresh_param0:472
                           /\ 0 <= (fresh___cost:471 + 1)
                           /\ 0 <= ((fresh___cost:471 + 1) + 1)
                           /\ fresh_param0:472 <= (fresh_param1:473 + 2)
                           /\ ((fresh___cost:471 + 1) + 1) = phi___cost:474
                           /\ (fresh_param1:473 + 2) = phi_y:475
                           /\ havoc:489 = phi_return:476
                           /\ fresh_param0:472 = phi_param0:477
                           /\ (fresh_param1:473 + 2) = phi_param1:478
                           /\ type_err:490 = phi_return@pos:479
                           /\ type_err:491 = phi_param0@pos:481
                           /\ type_err:492 = phi_param1@pos:483
                           /\ type_err:493 = phi_return@width:484
                           /\ type_err:494 = phi_param0@width:486
                           /\ type_err:495 = phi_param1@width:488))
               /\ (!(0 <= K:496)
                     \/ mid_(NewtonDomain.Left param0):497 = (fresh_param0:472
                                                                + K:496))
               /\ (!(0 <= K:496)
                     \/ mid_(NewtonDomain.Left param1):498 = (fresh_param1:473
                                                                + (-2 * K:496)))
               /\ (!(0 <= K:496)
                     \/ mid_(NewtonDomain.Left __cost):499 = (fresh___cost:471
                                                                + (-2 * K:496)))
               /\ ((K:496 = 0
                      /\ type_err:500 = mid_(NewtonDomain.Right return@width):501
                      /\ type_err:502 = mid_(NewtonDomain.Right return@pos):503
                      /\ havoc:504 = mid_(NewtonDomain.Right return):505
                      /\ fresh_param1@width:487 = mid_(NewtonDomain.Left param1@width):506
                      /\ fresh_param0@width:485 = mid_(NewtonDomain.Left param0@width):507
                      /\ fresh_param1@pos:482 = mid_(NewtonDomain.Left param1@pos):508
                      /\ fresh_param0@pos:480 = mid_(NewtonDomain.Left param0@pos):509
                      /\ fresh_param1:473 = mid_(NewtonDomain.Left param1):498
                      /\ fresh_param0:472 = mid_(NewtonDomain.Left param0):497
                      /\ fresh___cost:471 = mid_(NewtonDomain.Left __cost):499)
                     \/ (1 <= K:496 /\ 0 <= (-2 + fresh___cost:471)
                           /\ 0 <= (fresh_param0:472 + -fresh_param1:473)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):499
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):497
                                      + -mid_(NewtonDomain.Left param1):498)))
               /\ K:510 = 0
               /\ mid_(NewtonDomain.Right return@width):501 = (NewtonDomain.Right return@width)':511
               /\ mid_(NewtonDomain.Right return@pos):503 = (NewtonDomain.Right return@pos)':512
               /\ mid_(NewtonDomain.Right return):505 = (NewtonDomain.Right return)':513
               /\ mid_(NewtonDomain.Left param1@width):506 = (NewtonDomain.Left param1@width)':514
               /\ mid_(NewtonDomain.Left param0@width):507 = (NewtonDomain.Left param0@width)':515
               /\ mid_(NewtonDomain.Left param1@pos):508 = (NewtonDomain.Left param1@pos)':516
               /\ mid_(NewtonDomain.Left param0@pos):509 = (NewtonDomain.Left param0@pos)':517
               /\ mid_(NewtonDomain.Left param1):498 = (NewtonDomain.Left param1)':518
               /\ mid_(NewtonDomain.Left param0):497 = (NewtonDomain.Left param0)':519
               /\ mid_(NewtonDomain.Left __cost):499 = (NewtonDomain.Left __cost)':520
               /\ 0 = K:510 /\ (K:496 + K:510) = K:521 /\ 0 <= K:521
               /\ type_err:522 = (NewtonDomain.Left param1@width)':514
               /\ type_err:523 = (NewtonDomain.Left param0@width)':515
               /\ type_err:524 = (NewtonDomain.Left param1@pos)':516
               /\ type_err:525 = (NewtonDomain.Left param0@pos)':517
               /\ param1:21 = (NewtonDomain.Left param1)':518
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':519
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':520
               /\ phi___cost:474 = phi___cost:460
               /\ (param0:18 + -1) = phi_x:461
               /\ (NewtonDomain.Right return)':513 = phi_return:462
               /\ phi_param0:477 = phi_param0:463
               /\ phi_param1:478 = phi_param1:464
               /\ (NewtonDomain.Right return@pos)':512 = phi_return@pos:465
               /\ phi_param0@pos:481 = phi_param0@pos:466
               /\ phi_param1@pos:483 = phi_param1@pos:467
               /\ (NewtonDomain.Right return@width)':511 = phi_return@width:468
               /\ phi_param0@width:486 = phi_param0@width:469
               /\ phi_param1@width:488 = phi_param1@width:470))}

Evaluating variable number 27 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:456
 return := havoc:457
 param0 := phi_param0:453
 param1 := phi_param1:452
 return@pos := type_err:458
 param0@pos := phi_param0@pos:450
 param1@pos := phi_param1@pos:449
 return@width := type_err:459
 param0@width := phi_param0@width:447
 param1@width := phi_param1@width:446
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:456 /\ param0:18 = phi_x:455
          /\ return:250 = phi_return:454 /\ param0:18 = phi_param0:453
          /\ param1:21 = phi_param1:452
          /\ return@pos:246 = phi_return@pos:451
          /\ param0@pos:17 = phi_param0@pos:450
          /\ param1@pos:20 = phi_param1@pos:449
          /\ return@width:242 = phi_return@width:448
          /\ param0@width:16 = phi_param0@width:447
          /\ param1@width:19 = phi_param1@width:446)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:395 /\ 0 <= (fresh___cost:395 + 1)
                      /\ fresh_param0:396 <= (fresh_param1:397 + 1)
                      /\ (fresh___cost:395 + 1) = phi___cost:398
                      /\ fresh_param1:397 = phi_y:399
                      /\ return:250 = phi_return:400
                      /\ fresh_param0:396 = phi_param0:401
                      /\ fresh_param1:397 = phi_param1:402
                      /\ return@pos:246 = phi_return@pos:403
                      /\ fresh_param0@pos:404 = phi_param0@pos:405
                      /\ fresh_param1@pos:406 = phi_param1@pos:407
                      /\ return@width:242 = phi_return@width:408
                      /\ fresh_param0@width:409 = phi_param0@width:410
                      /\ fresh_param1@width:411 = phi_param1@width:412)
                     \/ (0 <= fresh___cost:395 /\ 0 <= (fresh___cost:395 + 1)
                           /\ (fresh_param1:397 + 1) < fresh_param0:396
                           /\ 0 <= (fresh___cost:395 + 1)
                           /\ 0 <= ((fresh___cost:395 + 1) + 1)
                           /\ fresh_param0:396 <= (fresh_param1:397 + 2)
                           /\ ((fresh___cost:395 + 1) + 1) = phi___cost:398
                           /\ (fresh_param1:397 + 2) = phi_y:399
                           /\ havoc:413 = phi_return:400
                           /\ fresh_param0:396 = phi_param0:401
                           /\ (fresh_param1:397 + 2) = phi_param1:402
                           /\ type_err:414 = phi_return@pos:403
                           /\ type_err:415 = phi_param0@pos:405
                           /\ type_err:416 = phi_param1@pos:407
                           /\ type_err:417 = phi_return@width:408
                           /\ type_err:418 = phi_param0@width:410
                           /\ type_err:419 = phi_param1@width:412))
               /\ (!(0 <= K:420)
                     \/ mid_(NewtonDomain.Left param0):421 = (fresh_param0:396
                                                                + K:420))
               /\ (!(0 <= K:420)
                     \/ mid_(NewtonDomain.Left param1):422 = (fresh_param1:397
                                                                + (-2 * K:420)))
               /\ (!(0 <= K:420)
                     \/ mid_(NewtonDomain.Left __cost):423 = (fresh___cost:395
                                                                + (-2 * K:420)))
               /\ ((K:420 = 0
                      /\ type_err:424 = mid_(NewtonDomain.Right return@width):425
                      /\ type_err:426 = mid_(NewtonDomain.Right return@pos):427
                      /\ havoc:428 = mid_(NewtonDomain.Right return):429
                      /\ fresh_param1@width:411 = mid_(NewtonDomain.Left param1@width):430
                      /\ fresh_param0@width:409 = mid_(NewtonDomain.Left param0@width):431
                      /\ fresh_param1@pos:406 = mid_(NewtonDomain.Left param1@pos):432
                      /\ fresh_param0@pos:404 = mid_(NewtonDomain.Left param0@pos):433
                      /\ fresh_param1:397 = mid_(NewtonDomain.Left param1):422
                      /\ fresh_param0:396 = mid_(NewtonDomain.Left param0):421
                      /\ fresh___cost:395 = mid_(NewtonDomain.Left __cost):423)
                     \/ (1 <= K:420 /\ 0 <= (-2 + fresh___cost:395)
                           /\ 0 <= (fresh_param0:396 + -fresh_param1:397)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):423
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):421
                                      + -mid_(NewtonDomain.Left param1):422)))
               /\ K:434 = 0
               /\ mid_(NewtonDomain.Right return@width):425 = (NewtonDomain.Right return@width)':435
               /\ mid_(NewtonDomain.Right return@pos):427 = (NewtonDomain.Right return@pos)':436
               /\ mid_(NewtonDomain.Right return):429 = (NewtonDomain.Right return)':437
               /\ mid_(NewtonDomain.Left param1@width):430 = (NewtonDomain.Left param1@width)':438
               /\ mid_(NewtonDomain.Left param0@width):431 = (NewtonDomain.Left param0@width)':439
               /\ mid_(NewtonDomain.Left param1@pos):432 = (NewtonDomain.Left param1@pos)':440
               /\ mid_(NewtonDomain.Left param0@pos):433 = (NewtonDomain.Left param0@pos)':441
               /\ mid_(NewtonDomain.Left param1):422 = (NewtonDomain.Left param1)':442
               /\ mid_(NewtonDomain.Left param0):421 = (NewtonDomain.Left param0)':443
               /\ mid_(NewtonDomain.Left __cost):423 = (NewtonDomain.Left __cost)':444
               /\ 0 = K:434 /\ (K:420 + K:434) = K:445 /\ 0 <= K:445
               /\ type_err:228 = (NewtonDomain.Left param1@width)':438
               /\ type_err:227 = (NewtonDomain.Left param0@width)':439
               /\ type_err:226 = (NewtonDomain.Left param1@pos)':440
               /\ type_err:225 = (NewtonDomain.Left param0@pos)':441
               /\ param1:21 = (NewtonDomain.Left param1)':442
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':443
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':444
               /\ phi___cost:398 = phi___cost:456
               /\ (param0:18 + -1) = phi_x:455
               /\ (NewtonDomain.Right return)':437 = phi_return:454
               /\ phi_param0:401 = phi_param0:453
               /\ phi_param1:402 = phi_param1:452
               /\ (NewtonDomain.Right return@pos)':436 = phi_return@pos:451
               /\ phi_param0@pos:405 = phi_param0@pos:450
               /\ phi_param1@pos:407 = phi_param1@pos:449
               /\ (NewtonDomain.Right return@width)':435 = phi_return@width:448
               /\ phi_param0@width:410 = phi_param0@width:447
               /\ phi_param1@width:412 = phi_param1@width:446))}

Evaluating variable number 34 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:252
 return := (NewtonDomain.Right return)':379
 param0 := phi_param0:248
 param1 := phi_param1:247
 return@pos := (NewtonDomain.Right return@pos)':378
 param0@pos := phi_param0@pos:244
 param1@pos := phi_param1@pos:243
 return@width := (NewtonDomain.Right return@width)':377
 param0@width := phi_param0@width:240
 param1@width := phi_param1@width:239
 when (((0 <= fresh___cost:388 /\ 0 <= (fresh___cost:388 + 1)
           /\ fresh_param0:389 <= (fresh_param1:390 + 1)
           /\ (fresh___cost:388 + 1) = phi___cost:252
           /\ fresh_param1:390 = phi_y:251 /\ return:250 = phi_return:249
           /\ fresh_param0:389 = phi_param0:248
           /\ fresh_param1:390 = phi_param1:247
           /\ return@pos:246 = phi_return@pos:245
           /\ fresh_param0@pos:391 = phi_param0@pos:244
           /\ fresh_param1@pos:392 = phi_param1@pos:243
           /\ return@width:242 = phi_return@width:241
           /\ fresh_param0@width:393 = phi_param0@width:240
           /\ fresh_param1@width:394 = phi_param1@width:239)
          \/ (0 <= fresh___cost:388 /\ 0 <= (fresh___cost:388 + 1)
                /\ (fresh_param1:390 + 1) < fresh_param0:389
                /\ 0 <= (fresh___cost:388 + 1)
                /\ 0 <= ((fresh___cost:388 + 1) + 1)
                /\ fresh_param0:389 <= (fresh_param1:390 + 2)
                /\ ((fresh___cost:388 + 1) + 1) = phi___cost:252
                /\ (fresh_param1:390 + 2) = phi_y:251
                /\ havoc:236 = phi_return:249
                /\ fresh_param0:389 = phi_param0:248
                /\ (fresh_param1:390 + 2) = phi_param1:247
                /\ type_err:237 = phi_return@pos:245
                /\ type_err:229 = phi_param0@pos:244
                /\ type_err:230 = phi_param1@pos:243
                /\ type_err:238 = phi_return@width:241
                /\ type_err:231 = phi_param0@width:240
                /\ type_err:232 = phi_param1@width:239))
         /\ (!(0 <= K:365)
               \/ mid_(NewtonDomain.Left param0):366 = (fresh_param0:389
                                                          + K:365))
         /\ (!(0 <= K:365)
               \/ mid_(NewtonDomain.Left param1):367 = (fresh_param1:390
                                                          + (-2 * K:365)))
         /\ (!(0 <= K:365)
               \/ mid_(NewtonDomain.Left __cost):368 = (fresh___cost:388
                                                          + (-2 * K:365)))
         /\ ((K:365 = 0
                /\ type_err:255 = mid_(NewtonDomain.Right return@width):369
                /\ type_err:254 = mid_(NewtonDomain.Right return@pos):370
                /\ havoc:253 = mid_(NewtonDomain.Right return):371
                /\ fresh_param1@width:394 = mid_(NewtonDomain.Left param1@width):372
                /\ fresh_param0@width:393 = mid_(NewtonDomain.Left param0@width):373
                /\ fresh_param1@pos:392 = mid_(NewtonDomain.Left param1@pos):374
                /\ fresh_param0@pos:391 = mid_(NewtonDomain.Left param0@pos):375
                /\ fresh_param1:390 = mid_(NewtonDomain.Left param1):367
                /\ fresh_param0:389 = mid_(NewtonDomain.Left param0):366
                /\ fresh___cost:388 = mid_(NewtonDomain.Left __cost):368)
               \/ (1 <= K:365 /\ 0 <= (-2 + fresh___cost:388)
                     /\ 0 <= (fresh_param0:389 + -fresh_param1:390)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):368
                     /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):366
                                + -mid_(NewtonDomain.Left param1):367)))
         /\ K:376 = 0
         /\ mid_(NewtonDomain.Right return@width):369 = (NewtonDomain.Right return@width)':377
         /\ mid_(NewtonDomain.Right return@pos):370 = (NewtonDomain.Right return@pos)':378
         /\ mid_(NewtonDomain.Right return):371 = (NewtonDomain.Right return)':379
         /\ mid_(NewtonDomain.Left param1@width):372 = (NewtonDomain.Left param1@width)':380
         /\ mid_(NewtonDomain.Left param0@width):373 = (NewtonDomain.Left param0@width)':381
         /\ mid_(NewtonDomain.Left param1@pos):374 = (NewtonDomain.Left param1@pos)':382
         /\ mid_(NewtonDomain.Left param0@pos):375 = (NewtonDomain.Left param0@pos)':383
         /\ mid_(NewtonDomain.Left param1):367 = (NewtonDomain.Left param1)':384
         /\ mid_(NewtonDomain.Left param0):366 = (NewtonDomain.Left param0)':385
         /\ mid_(NewtonDomain.Left __cost):368 = (NewtonDomain.Left __cost)':386
         /\ 0 = K:376 /\ (K:365 + K:376) = K:387 /\ 0 <= K:387
         /\ param1@width:19 = (NewtonDomain.Left param1@width)':380
         /\ param0@width:16 = (NewtonDomain.Left param0@width)':381
         /\ param1@pos:20 = (NewtonDomain.Left param1@pos)':382
         /\ param0@pos:17 = (NewtonDomain.Left param0@pos)':383
         /\ param1:21 = (NewtonDomain.Left param1)':384
         /\ param0:18 = (NewtonDomain.Left param0)':385
         /\ __cost:0 = (NewtonDomain.Left __cost)':386)}

    (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:704
 (NewtonDomain.Left param0) := fresh_param0:706
 (NewtonDomain.Left param1) := fresh_param1:705
 (NewtonDomain.Left param0@pos) := fresh_param0@pos:713
 (NewtonDomain.Left param1@pos) := fresh_param1@pos:714
 (NewtonDomain.Left param0@width) := fresh_param0@width:715
 (NewtonDomain.Left param1@width) := fresh_param1@width:716
 (NewtonDomain.Right return) := havoc:717
 (NewtonDomain.Right return@pos) := type_err:718
 (NewtonDomain.Right return@width) := type_err:719
 when (0 <= fresh___cost:684 /\ 0 <= (fresh___cost:684 + 1)
         /\ fresh_param1:688 < fresh_param0:687
         /\ (NewtonDomain.Left __cost):265 = (fresh___cost:684 + 1)
         /\ (NewtonDomain.Right x):693 = (fresh_param0:687 + -1)
         /\ (NewtonDomain.Right y):694 = fresh_param1:688
         /\ (NewtonDomain.Left param0):268 = (fresh_param0:687 + -1)
         /\ (NewtonDomain.Left param1):269 = fresh_param1:688
         /\ (NewtonDomain.Left param0@pos):270 = type_err:225
         /\ (NewtonDomain.Left param1@pos):271 = type_err:226
         /\ (NewtonDomain.Left param0@width):272 = type_err:227
         /\ (NewtonDomain.Left param1@width):273 = type_err:228
         /\ 0 <= fresh___cost:704 /\ 0 <= (fresh___cost:704 + 1)
         /\ (fresh_param1:705 + 1) < fresh_param0:706
         /\ fresh___cost:684 = (fresh___cost:704 + 1)
         /\ (NewtonDomain.Right x):720 = fresh_param0:706
         /\ (NewtonDomain.Right y):721 = (fresh_param1:705 + 2)
         /\ fresh_param0:687 = fresh_param0:706
         /\ fresh_param1:688 = (fresh_param1:705 + 2)
         /\ fresh_param0@pos:689 = type_err:707
         /\ fresh_param1@pos:690 = type_err:708
         /\ fresh_param0@width:691 = type_err:709
         /\ fresh_param1@width:692 = type_err:710)}
**** alpha hat: 
  {<Split [true
            ((NewtonDomain.Left param0)':310) = (1)*((NewtonDomain.Left param0):268)
                                                 + 1
           ((NewtonDomain.Left param1)':311) = (1)*((NewtonDomain.Left param1):269)
                                                + (-2)*1
           ((NewtonDomain.Left __cost)':309) = (1)*((NewtonDomain.Left __cost):265)
                                                + (-2)*1
           }
          pre:
            [|(NewtonDomain.Left __cost):265-2>=0;
              (NewtonDomain.Left param0):268-(NewtonDomain.Left param1):269>=0|]
          post:
            [|(NewtonDomain.Left __cost)':309>=0;
              (NewtonDomain.Left param0)':310-(NewtonDomain.Left param1)':311
              -3>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {(NewtonDomain.Left __cost) := (NewtonDomain.Left __cost)':309
   (NewtonDomain.Left param0) := (NewtonDomain.Left param0)':310
   (NewtonDomain.Left param1) := (NewtonDomain.Left param1)':311
   (NewtonDomain.Left param0@pos) := (NewtonDomain.Left param0@pos)':312
   (NewtonDomain.Left param1@pos) := (NewtonDomain.Left param1@pos)':313
   (NewtonDomain.Left param0@width) := (NewtonDomain.Left param0@width)':314
   (NewtonDomain.Left param1@width) := (NewtonDomain.Left param1@width)':315
   (NewtonDomain.Right return) := (NewtonDomain.Right return)':317
   (NewtonDomain.Right return@pos) := (NewtonDomain.Right return@pos)':319
   (NewtonDomain.Right return@width) := (NewtonDomain.Right return@width)':321
   when ((!(0 <= K:746)
            \/ mid_(NewtonDomain.Left param0):756 = ((NewtonDomain.Left param0):268
                                                       + K:746))
           /\ (!(0 <= K:746)
                 \/ mid_(NewtonDomain.Left param1):755 = ((NewtonDomain.Left param1):269
                                                            + (-2 * K:746)))
           /\ (!(0 <= K:746)
                 \/ mid_(NewtonDomain.Left __cost):757 = ((NewtonDomain.Left __cost):265
                                                            + (-2 * K:746)))
           /\ ((K:746 = 0
                  /\ (NewtonDomain.Right return@width):320 = mid_(NewtonDomain.Right return@width):748
                  /\ (NewtonDomain.Right return@pos):318 = mid_(NewtonDomain.Right return@pos):749
                  /\ (NewtonDomain.Right return):316 = mid_(NewtonDomain.Right return):750
                  /\ (NewtonDomain.Left param1@width):273 = mid_(NewtonDomain.Left param1@width):751
                  /\ (NewtonDomain.Left param0@width):272 = mid_(NewtonDomain.Left param0@width):752
                  /\ (NewtonDomain.Left param1@pos):271 = mid_(NewtonDomain.Left param1@pos):753
                  /\ (NewtonDomain.Left param0@pos):270 = mid_(NewtonDomain.Left param0@pos):754
                  /\ (NewtonDomain.Left param1):269 = mid_(NewtonDomain.Left param1):755
                  /\ (NewtonDomain.Left param0):268 = mid_(NewtonDomain.Left param0):756
                  /\ (NewtonDomain.Left __cost):265 = mid_(NewtonDomain.Left __cost):757)
                 \/ (1 <= K:746 /\ 0 <= (-2 + (NewtonDomain.Left __cost):265)
                       /\ 0 <= ((NewtonDomain.Left param0):268
                                  + -(NewtonDomain.Left param1):269)
                       /\ 0 <= mid_(NewtonDomain.Left __cost):757
                       /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):756
                                  + -mid_(NewtonDomain.Left param1):755)))
           /\ K:747 = 0
           /\ mid_(NewtonDomain.Right return@width):748 = (NewtonDomain.Right return@width)':321
           /\ mid_(NewtonDomain.Right return@pos):749 = (NewtonDomain.Right return@pos)':319
           /\ mid_(NewtonDomain.Right return):750 = (NewtonDomain.Right return)':317
           /\ mid_(NewtonDomain.Left param1@width):751 = (NewtonDomain.Left param1@width)':315
           /\ mid_(NewtonDomain.Left param0@width):752 = (NewtonDomain.Left param0@width)':314
           /\ mid_(NewtonDomain.Left param1@pos):753 = (NewtonDomain.Left param1@pos)':313
           /\ mid_(NewtonDomain.Left param0@pos):754 = (NewtonDomain.Left param0@pos)':312
           /\ mid_(NewtonDomain.Left param1):755 = (NewtonDomain.Left param1)':311
           /\ mid_(NewtonDomain.Left param0):756 = (NewtonDomain.Left param0)':310
           /\ mid_(NewtonDomain.Left __cost):757 = (NewtonDomain.Left __cost)':309
           /\ 0 = K:747 /\ (K:746 + K:747) = K:745 /\ 0 <= K:745)}
}

  The IRE-evaluated value on this round is: 

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

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:925
 return := havoc:998
 param0 := phi_param0:928
 param1 := phi_param1:929
 return@pos := type_err:999
 param0@pos := phi_param0@pos:932
 param1@pos := phi_param1@pos:934
 return@width := type_err:1000
 param0@width := phi_param0@width:937
 param1@width := phi_param1@width:939
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:925 /\ param0:18 = phi_x:926
          /\ return:250 = phi_return:927 /\ param0:18 = phi_param0:928
          /\ param1:21 = phi_param1:929
          /\ return@pos:246 = phi_return@pos:930
          /\ type_err:931 = phi_param0@pos:932
          /\ type_err:933 = phi_param1@pos:934
          /\ return@width:242 = phi_return@width:935
          /\ type_err:936 = phi_param0@width:937
          /\ type_err:938 = phi_param1@width:939)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:940 /\ 0 <= (fresh___cost:940 + 1)
                      /\ fresh_param0:941 <= (fresh_param1:942 + 1)
                      /\ (fresh___cost:940 + 1) = phi___cost:943
                      /\ fresh_param1:942 = phi_y:944
                      /\ return:250 = phi_return:945
                      /\ fresh_param0:941 = phi_param0:946
                      /\ fresh_param1:942 = phi_param1:947
                      /\ return@pos:246 = phi_return@pos:948
                      /\ fresh_param0@pos:949 = phi_param0@pos:950
                      /\ fresh_param1@pos:951 = phi_param1@pos:952
                      /\ return@width:242 = phi_return@width:953
                      /\ fresh_param0@width:954 = phi_param0@width:955
                      /\ fresh_param1@width:956 = phi_param1@width:957)
                     \/ (0 <= fresh___cost:940 /\ 0 <= (fresh___cost:940 + 1)
                           /\ (fresh_param1:942 + 1) < fresh_param0:941
                           /\ 0 <= (fresh___cost:940 + 1)
                           /\ 0 <= ((fresh___cost:940 + 1) + 1)
                           /\ fresh_param0:941 <= (fresh_param1:942 + 2)
                           /\ ((fresh___cost:940 + 1) + 1) = phi___cost:943
                           /\ (fresh_param1:942 + 2) = phi_y:944
                           /\ havoc:958 = phi_return:945
                           /\ fresh_param0:941 = phi_param0:946
                           /\ (fresh_param1:942 + 2) = phi_param1:947
                           /\ type_err:959 = phi_return@pos:948
                           /\ type_err:960 = phi_param0@pos:950
                           /\ type_err:961 = phi_param1@pos:952
                           /\ type_err:962 = phi_return@width:953
                           /\ type_err:963 = phi_param0@width:955
                           /\ type_err:964 = phi_param1@width:957))
               /\ (!(0 <= K:965)
                     \/ mid_(NewtonDomain.Left param0):966 = (fresh_param0:941
                                                                + K:965))
               /\ (!(0 <= K:965)
                     \/ mid_(NewtonDomain.Left param1):967 = (fresh_param1:942
                                                                + (-2 * K:965)))
               /\ (!(0 <= K:965)
                     \/ mid_(NewtonDomain.Left __cost):968 = (fresh___cost:940
                                                                + (-2 * K:965)))
               /\ ((K:965 = 0
                      /\ type_err:969 = mid_(NewtonDomain.Right return@width):970
                      /\ type_err:971 = mid_(NewtonDomain.Right return@pos):972
                      /\ havoc:973 = mid_(NewtonDomain.Right return):974
                      /\ fresh_param1@width:956 = mid_(NewtonDomain.Left param1@width):975
                      /\ fresh_param0@width:954 = mid_(NewtonDomain.Left param0@width):976
                      /\ fresh_param1@pos:951 = mid_(NewtonDomain.Left param1@pos):977
                      /\ fresh_param0@pos:949 = mid_(NewtonDomain.Left param0@pos):978
                      /\ fresh_param1:942 = mid_(NewtonDomain.Left param1):967
                      /\ fresh_param0:941 = mid_(NewtonDomain.Left param0):966
                      /\ fresh___cost:940 = mid_(NewtonDomain.Left __cost):968)
                     \/ (1 <= K:965 /\ 0 <= (-2 + fresh___cost:940)
                           /\ 0 <= (fresh_param0:941 + -fresh_param1:942)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):968
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):966
                                      + -mid_(NewtonDomain.Left param1):967)))
               /\ K:979 = 0
               /\ mid_(NewtonDomain.Right return@width):970 = (NewtonDomain.Right return@width)':980
               /\ mid_(NewtonDomain.Right return@pos):972 = (NewtonDomain.Right return@pos)':981
               /\ mid_(NewtonDomain.Right return):974 = (NewtonDomain.Right return)':982
               /\ mid_(NewtonDomain.Left param1@width):975 = (NewtonDomain.Left param1@width)':983
               /\ mid_(NewtonDomain.Left param0@width):976 = (NewtonDomain.Left param0@width)':984
               /\ mid_(NewtonDomain.Left param1@pos):977 = (NewtonDomain.Left param1@pos)':985
               /\ mid_(NewtonDomain.Left param0@pos):978 = (NewtonDomain.Left param0@pos)':986
               /\ mid_(NewtonDomain.Left param1):967 = (NewtonDomain.Left param1)':987
               /\ mid_(NewtonDomain.Left param0):966 = (NewtonDomain.Left param0)':988
               /\ mid_(NewtonDomain.Left __cost):968 = (NewtonDomain.Left __cost)':989
               /\ 0 = K:979 /\ (K:965 + K:979) = K:990 /\ 0 <= K:990
               /\ type_err:991 = (NewtonDomain.Left param1@width)':983
               /\ type_err:992 = (NewtonDomain.Left param0@width)':984
               /\ type_err:993 = (NewtonDomain.Left param1@pos)':985
               /\ type_err:994 = (NewtonDomain.Left param0@pos)':986
               /\ param1:21 = (NewtonDomain.Left param1)':987
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':988
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':989
               /\ phi___cost:943 = phi___cost:925
               /\ (param0:18 + -1) = phi_x:926
               /\ (NewtonDomain.Right return)':982 = phi_return:927
               /\ phi_param0:946 = phi_param0:928
               /\ phi_param1:947 = phi_param1:929
               /\ (NewtonDomain.Right return@pos)':981 = phi_return@pos:930
               /\ phi_param0@pos:950 = phi_param0@pos:932
               /\ phi_param1@pos:952 = phi_param1@pos:934
               /\ (NewtonDomain.Right return@width)':980 = phi_return@width:935
               /\ phi_param0@width:955 = phi_param0@width:937
               /\ phi_param1@width:957 = phi_param1@width:939))}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:853
 return := havoc:922
 param0 := phi_param0:856
 param1 := phi_param1:857
 return@pos := type_err:923
 param0@pos := phi_param0@pos:859
 param1@pos := phi_param1@pos:860
 return@width := type_err:924
 param0@width := phi_param0@width:862
 param1@width := phi_param1@width:863
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:853 /\ param0:18 = phi_x:854
          /\ return:250 = phi_return:855 /\ param0:18 = phi_param0:856
          /\ param1:21 = phi_param1:857
          /\ return@pos:246 = phi_return@pos:858
          /\ type_err:163 = phi_param0@pos:859
          /\ type_err:164 = phi_param1@pos:860
          /\ return@width:242 = phi_return@width:861
          /\ type_err:165 = phi_param0@width:862
          /\ type_err:166 = phi_param1@width:863)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:864 /\ 0 <= (fresh___cost:864 + 1)
                      /\ fresh_param0:865 <= (fresh_param1:866 + 1)
                      /\ (fresh___cost:864 + 1) = phi___cost:867
                      /\ fresh_param1:866 = phi_y:868
                      /\ return:250 = phi_return:869
                      /\ fresh_param0:865 = phi_param0:870
                      /\ fresh_param1:866 = phi_param1:871
                      /\ return@pos:246 = phi_return@pos:872
                      /\ fresh_param0@pos:873 = phi_param0@pos:874
                      /\ fresh_param1@pos:875 = phi_param1@pos:876
                      /\ return@width:242 = phi_return@width:877
                      /\ fresh_param0@width:878 = phi_param0@width:879
                      /\ fresh_param1@width:880 = phi_param1@width:881)
                     \/ (0 <= fresh___cost:864 /\ 0 <= (fresh___cost:864 + 1)
                           /\ (fresh_param1:866 + 1) < fresh_param0:865
                           /\ 0 <= (fresh___cost:864 + 1)
                           /\ 0 <= ((fresh___cost:864 + 1) + 1)
                           /\ fresh_param0:865 <= (fresh_param1:866 + 2)
                           /\ ((fresh___cost:864 + 1) + 1) = phi___cost:867
                           /\ (fresh_param1:866 + 2) = phi_y:868
                           /\ havoc:882 = phi_return:869
                           /\ fresh_param0:865 = phi_param0:870
                           /\ (fresh_param1:866 + 2) = phi_param1:871
                           /\ type_err:883 = phi_return@pos:872
                           /\ type_err:884 = phi_param0@pos:874
                           /\ type_err:885 = phi_param1@pos:876
                           /\ type_err:886 = phi_return@width:877
                           /\ type_err:887 = phi_param0@width:879
                           /\ type_err:888 = phi_param1@width:881))
               /\ (!(0 <= K:889)
                     \/ mid_(NewtonDomain.Left param0):890 = (fresh_param0:865
                                                                + K:889))
               /\ (!(0 <= K:889)
                     \/ mid_(NewtonDomain.Left param1):891 = (fresh_param1:866
                                                                + (-2 * K:889)))
               /\ (!(0 <= K:889)
                     \/ mid_(NewtonDomain.Left __cost):892 = (fresh___cost:864
                                                                + (-2 * K:889)))
               /\ ((K:889 = 0
                      /\ type_err:893 = mid_(NewtonDomain.Right return@width):894
                      /\ type_err:895 = mid_(NewtonDomain.Right return@pos):896
                      /\ havoc:897 = mid_(NewtonDomain.Right return):898
                      /\ fresh_param1@width:880 = mid_(NewtonDomain.Left param1@width):899
                      /\ fresh_param0@width:878 = mid_(NewtonDomain.Left param0@width):900
                      /\ fresh_param1@pos:875 = mid_(NewtonDomain.Left param1@pos):901
                      /\ fresh_param0@pos:873 = mid_(NewtonDomain.Left param0@pos):902
                      /\ fresh_param1:866 = mid_(NewtonDomain.Left param1):891
                      /\ fresh_param0:865 = mid_(NewtonDomain.Left param0):890
                      /\ fresh___cost:864 = mid_(NewtonDomain.Left __cost):892)
                     \/ (1 <= K:889 /\ 0 <= (-2 + fresh___cost:864)
                           /\ 0 <= (fresh_param0:865 + -fresh_param1:866)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):892
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):890
                                      + -mid_(NewtonDomain.Left param1):891)))
               /\ K:903 = 0
               /\ mid_(NewtonDomain.Right return@width):894 = (NewtonDomain.Right return@width)':904
               /\ mid_(NewtonDomain.Right return@pos):896 = (NewtonDomain.Right return@pos)':905
               /\ mid_(NewtonDomain.Right return):898 = (NewtonDomain.Right return)':906
               /\ mid_(NewtonDomain.Left param1@width):899 = (NewtonDomain.Left param1@width)':907
               /\ mid_(NewtonDomain.Left param0@width):900 = (NewtonDomain.Left param0@width)':908
               /\ mid_(NewtonDomain.Left param1@pos):901 = (NewtonDomain.Left param1@pos)':909
               /\ mid_(NewtonDomain.Left param0@pos):902 = (NewtonDomain.Left param0@pos)':910
               /\ mid_(NewtonDomain.Left param1):891 = (NewtonDomain.Left param1)':911
               /\ mid_(NewtonDomain.Left param0):890 = (NewtonDomain.Left param0)':912
               /\ mid_(NewtonDomain.Left __cost):892 = (NewtonDomain.Left __cost)':913
               /\ 0 = K:903 /\ (K:889 + K:903) = K:914 /\ 0 <= K:914
               /\ type_err:915 = (NewtonDomain.Left param1@width)':907
               /\ type_err:916 = (NewtonDomain.Left param0@width)':908
               /\ type_err:917 = (NewtonDomain.Left param1@pos)':909
               /\ type_err:918 = (NewtonDomain.Left param0@pos)':910
               /\ param1:21 = (NewtonDomain.Left param1)':911
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':912
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':913
               /\ phi___cost:867 = phi___cost:853
               /\ (param0:18 + -1) = phi_x:854
               /\ (NewtonDomain.Right return)':906 = phi_return:855
               /\ phi_param0:870 = phi_param0:856
               /\ phi_param1:871 = phi_param1:857
               /\ (NewtonDomain.Right return@pos)':905 = phi_return@pos:858
               /\ phi_param0@pos:874 = phi_param0@pos:859
               /\ phi_param1@pos:876 = phi_param1@pos:860
               /\ (NewtonDomain.Right return@width)':904 = phi_return@width:861
               /\ phi_param0@width:879 = phi_param0@width:862
               /\ phi_param1@width:881 = phi_param1@width:863))}

Evaluating variable number 27 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:849
 return := havoc:850
 param0 := phi_param0:846
 param1 := phi_param1:845
 return@pos := type_err:851
 param0@pos := phi_param0@pos:843
 param1@pos := phi_param1@pos:842
 return@width := type_err:852
 param0@width := phi_param0@width:840
 param1@width := phi_param1@width:839
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:849 /\ param0:18 = phi_x:848
          /\ return:250 = phi_return:847 /\ param0:18 = phi_param0:846
          /\ param1:21 = phi_param1:845
          /\ return@pos:246 = phi_return@pos:844
          /\ param0@pos:17 = phi_param0@pos:843
          /\ param1@pos:20 = phi_param1@pos:842
          /\ return@width:242 = phi_return@width:841
          /\ param0@width:16 = phi_param0@width:840
          /\ param1@width:19 = phi_param1@width:839)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:788 /\ 0 <= (fresh___cost:788 + 1)
                      /\ fresh_param0:789 <= (fresh_param1:790 + 1)
                      /\ (fresh___cost:788 + 1) = phi___cost:791
                      /\ fresh_param1:790 = phi_y:792
                      /\ return:250 = phi_return:793
                      /\ fresh_param0:789 = phi_param0:794
                      /\ fresh_param1:790 = phi_param1:795
                      /\ return@pos:246 = phi_return@pos:796
                      /\ fresh_param0@pos:797 = phi_param0@pos:798
                      /\ fresh_param1@pos:799 = phi_param1@pos:800
                      /\ return@width:242 = phi_return@width:801
                      /\ fresh_param0@width:802 = phi_param0@width:803
                      /\ fresh_param1@width:804 = phi_param1@width:805)
                     \/ (0 <= fresh___cost:788 /\ 0 <= (fresh___cost:788 + 1)
                           /\ (fresh_param1:790 + 1) < fresh_param0:789
                           /\ 0 <= (fresh___cost:788 + 1)
                           /\ 0 <= ((fresh___cost:788 + 1) + 1)
                           /\ fresh_param0:789 <= (fresh_param1:790 + 2)
                           /\ ((fresh___cost:788 + 1) + 1) = phi___cost:791
                           /\ (fresh_param1:790 + 2) = phi_y:792
                           /\ havoc:806 = phi_return:793
                           /\ fresh_param0:789 = phi_param0:794
                           /\ (fresh_param1:790 + 2) = phi_param1:795
                           /\ type_err:807 = phi_return@pos:796
                           /\ type_err:808 = phi_param0@pos:798
                           /\ type_err:809 = phi_param1@pos:800
                           /\ type_err:810 = phi_return@width:801
                           /\ type_err:811 = phi_param0@width:803
                           /\ type_err:812 = phi_param1@width:805))
               /\ (!(0 <= K:813)
                     \/ mid_(NewtonDomain.Left param0):814 = (fresh_param0:789
                                                                + K:813))
               /\ (!(0 <= K:813)
                     \/ mid_(NewtonDomain.Left param1):815 = (fresh_param1:790
                                                                + (-2 * K:813)))
               /\ (!(0 <= K:813)
                     \/ mid_(NewtonDomain.Left __cost):816 = (fresh___cost:788
                                                                + (-2 * K:813)))
               /\ ((K:813 = 0
                      /\ type_err:817 = mid_(NewtonDomain.Right return@width):818
                      /\ type_err:819 = mid_(NewtonDomain.Right return@pos):820
                      /\ havoc:821 = mid_(NewtonDomain.Right return):822
                      /\ fresh_param1@width:804 = mid_(NewtonDomain.Left param1@width):823
                      /\ fresh_param0@width:802 = mid_(NewtonDomain.Left param0@width):824
                      /\ fresh_param1@pos:799 = mid_(NewtonDomain.Left param1@pos):825
                      /\ fresh_param0@pos:797 = mid_(NewtonDomain.Left param0@pos):826
                      /\ fresh_param1:790 = mid_(NewtonDomain.Left param1):815
                      /\ fresh_param0:789 = mid_(NewtonDomain.Left param0):814
                      /\ fresh___cost:788 = mid_(NewtonDomain.Left __cost):816)
                     \/ (1 <= K:813 /\ 0 <= (-2 + fresh___cost:788)
                           /\ 0 <= (fresh_param0:789 + -fresh_param1:790)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):816
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):814
                                      + -mid_(NewtonDomain.Left param1):815)))
               /\ K:827 = 0
               /\ mid_(NewtonDomain.Right return@width):818 = (NewtonDomain.Right return@width)':828
               /\ mid_(NewtonDomain.Right return@pos):820 = (NewtonDomain.Right return@pos)':829
               /\ mid_(NewtonDomain.Right return):822 = (NewtonDomain.Right return)':830
               /\ mid_(NewtonDomain.Left param1@width):823 = (NewtonDomain.Left param1@width)':831
               /\ mid_(NewtonDomain.Left param0@width):824 = (NewtonDomain.Left param0@width)':832
               /\ mid_(NewtonDomain.Left param1@pos):825 = (NewtonDomain.Left param1@pos)':833
               /\ mid_(NewtonDomain.Left param0@pos):826 = (NewtonDomain.Left param0@pos)':834
               /\ mid_(NewtonDomain.Left param1):815 = (NewtonDomain.Left param1)':835
               /\ mid_(NewtonDomain.Left param0):814 = (NewtonDomain.Left param0)':836
               /\ mid_(NewtonDomain.Left __cost):816 = (NewtonDomain.Left __cost)':837
               /\ 0 = K:827 /\ (K:813 + K:827) = K:838 /\ 0 <= K:838
               /\ type_err:228 = (NewtonDomain.Left param1@width)':831
               /\ type_err:227 = (NewtonDomain.Left param0@width)':832
               /\ type_err:226 = (NewtonDomain.Left param1@pos)':833
               /\ type_err:225 = (NewtonDomain.Left param0@pos)':834
               /\ param1:21 = (NewtonDomain.Left param1)':835
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':836
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':837
               /\ phi___cost:791 = phi___cost:849
               /\ (param0:18 + -1) = phi_x:848
               /\ (NewtonDomain.Right return)':830 = phi_return:847
               /\ phi_param0:794 = phi_param0:846
               /\ phi_param1:795 = phi_param1:845
               /\ (NewtonDomain.Right return@pos)':829 = phi_return@pos:844
               /\ phi_param0@pos:798 = phi_param0@pos:843
               /\ phi_param1@pos:800 = phi_param1@pos:842
               /\ (NewtonDomain.Right return@width)':828 = phi_return@width:841
               /\ phi_param0@width:803 = phi_param0@width:840
               /\ phi_param1@width:805 = phi_param1@width:839))}

Evaluating variable number 34 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := phi___cost:252
 return := (NewtonDomain.Right return)':772
 param0 := phi_param0:248
 param1 := phi_param1:247
 return@pos := (NewtonDomain.Right return@pos)':771
 param0@pos := phi_param0@pos:244
 param1@pos := phi_param1@pos:243
 return@width := (NewtonDomain.Right return@width)':770
 param0@width := phi_param0@width:240
 param1@width := phi_param1@width:239
 when (((0 <= fresh___cost:781 /\ 0 <= (fresh___cost:781 + 1)
           /\ fresh_param0:782 <= (fresh_param1:783 + 1)
           /\ (fresh___cost:781 + 1) = phi___cost:252
           /\ fresh_param1:783 = phi_y:251 /\ return:250 = phi_return:249
           /\ fresh_param0:782 = phi_param0:248
           /\ fresh_param1:783 = phi_param1:247
           /\ return@pos:246 = phi_return@pos:245
           /\ fresh_param0@pos:784 = phi_param0@pos:244
           /\ fresh_param1@pos:785 = phi_param1@pos:243
           /\ return@width:242 = phi_return@width:241
           /\ fresh_param0@width:786 = phi_param0@width:240
           /\ fresh_param1@width:787 = phi_param1@width:239)
          \/ (0 <= fresh___cost:781 /\ 0 <= (fresh___cost:781 + 1)
                /\ (fresh_param1:783 + 1) < fresh_param0:782
                /\ 0 <= (fresh___cost:781 + 1)
                /\ 0 <= ((fresh___cost:781 + 1) + 1)
                /\ fresh_param0:782 <= (fresh_param1:783 + 2)
                /\ ((fresh___cost:781 + 1) + 1) = phi___cost:252
                /\ (fresh_param1:783 + 2) = phi_y:251
                /\ havoc:236 = phi_return:249
                /\ fresh_param0:782 = phi_param0:248
                /\ (fresh_param1:783 + 2) = phi_param1:247
                /\ type_err:237 = phi_return@pos:245
                /\ type_err:229 = phi_param0@pos:244
                /\ type_err:230 = phi_param1@pos:243
                /\ type_err:238 = phi_return@width:241
                /\ type_err:231 = phi_param0@width:240
                /\ type_err:232 = phi_param1@width:239))
         /\ (!(0 <= K:758)
               \/ mid_(NewtonDomain.Left param0):759 = (fresh_param0:782
                                                          + K:758))
         /\ (!(0 <= K:758)
               \/ mid_(NewtonDomain.Left param1):760 = (fresh_param1:783
                                                          + (-2 * K:758)))
         /\ (!(0 <= K:758)
               \/ mid_(NewtonDomain.Left __cost):761 = (fresh___cost:781
                                                          + (-2 * K:758)))
         /\ ((K:758 = 0
                /\ type_err:255 = mid_(NewtonDomain.Right return@width):762
                /\ type_err:254 = mid_(NewtonDomain.Right return@pos):763
                /\ havoc:253 = mid_(NewtonDomain.Right return):764
                /\ fresh_param1@width:787 = mid_(NewtonDomain.Left param1@width):765
                /\ fresh_param0@width:786 = mid_(NewtonDomain.Left param0@width):766
                /\ fresh_param1@pos:785 = mid_(NewtonDomain.Left param1@pos):767
                /\ fresh_param0@pos:784 = mid_(NewtonDomain.Left param0@pos):768
                /\ fresh_param1:783 = mid_(NewtonDomain.Left param1):760
                /\ fresh_param0:782 = mid_(NewtonDomain.Left param0):759
                /\ fresh___cost:781 = mid_(NewtonDomain.Left __cost):761)
               \/ (1 <= K:758 /\ 0 <= (-2 + fresh___cost:781)
                     /\ 0 <= (fresh_param0:782 + -fresh_param1:783)
                     /\ 0 <= mid_(NewtonDomain.Left __cost):761
                     /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):759
                                + -mid_(NewtonDomain.Left param1):760)))
         /\ K:769 = 0
         /\ mid_(NewtonDomain.Right return@width):762 = (NewtonDomain.Right return@width)':770
         /\ mid_(NewtonDomain.Right return@pos):763 = (NewtonDomain.Right return@pos)':771
         /\ mid_(NewtonDomain.Right return):764 = (NewtonDomain.Right return)':772
         /\ mid_(NewtonDomain.Left param1@width):765 = (NewtonDomain.Left param1@width)':773
         /\ mid_(NewtonDomain.Left param0@width):766 = (NewtonDomain.Left param0@width)':774
         /\ mid_(NewtonDomain.Left param1@pos):767 = (NewtonDomain.Left param1@pos)':775
         /\ mid_(NewtonDomain.Left param0@pos):768 = (NewtonDomain.Left param0@pos)':776
         /\ mid_(NewtonDomain.Left param1):760 = (NewtonDomain.Left param1)':777
         /\ mid_(NewtonDomain.Left param0):759 = (NewtonDomain.Left param0)':778
         /\ mid_(NewtonDomain.Left __cost):761 = (NewtonDomain.Left __cost)':779
         /\ 0 = K:769 /\ (K:758 + K:769) = K:780 /\ 0 <= K:780
         /\ param1@width:19 = (NewtonDomain.Left param1@width)':773
         /\ param0@width:16 = (NewtonDomain.Left param0@width)':774
         /\ param1@pos:20 = (NewtonDomain.Left param1@pos)':775
         /\ param0@pos:17 = (NewtonDomain.Left param0@pos)':776
         /\ param1:21 = (NewtonDomain.Left param1)':777
         /\ param0:18 = (NewtonDomain.Left param0)':778
         /\ __cost:0 = (NewtonDomain.Left __cost)':779)}

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

NumRnds: 2

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,75)_g1> -> <__pstate, (Unique State Name,69)_g1>	Base relation: 
{param0 := param0:18
 param1 := param1:21
 param0@pos := type_err:131
 param1@pos := type_err:132
 param0@width := type_err:133
 param1@width := type_err:134}	
<__pstate, (Unique State Name,69)_g1> -> <__pstate, (Unique State Name,57)_g1>	Base relation: 
{param0 := param0:18
 param1 := param1:21
 param0@pos := type_err:163
 param1@pos := type_err:164
 param0@width := type_err:165
 param1@width := type_err:166}	
<__pstate, (Unique State Name,63)_g1> -> <__pstate, (Unique State Name,57)_g1>	Base relation: 
{__cost := (__cost:0 + 1)
 x := param0:18
 y := (param1:21 + 2)
 param0 := param0:18
 param1 := (param1:21 + 2)
 param0@pos := type_err:229
 param1@pos := type_err:230
 param0@width := type_err:231
 param1@width := type_err:232
 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ (param1:21 + 1) < param0:18)}	
<__pstate, (Unique State Name,57)_g1> -> <__pstate, (Unique State Name,63)_g1>	Base relation: 
{__cost := (__cost:0 + 1)
 x := (param0:18 + -1)
 y := param1:21
 param0 := (param0:18 + -1)
 param1 := param1:21
 param0@pos := type_err:225
 param1@pos := type_err:226
 param0@width := type_err:227
 param1@width := type_err:228
 when (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18)}	
<__pstate, accept> -> <__pstate, (Unique State Name,75)_g1>	Base relation: 
{__cost := 0
 y := havoc:83
 z := havoc:84
 param0 := havoc:83
 param1 := havoc:84
 param0@pos := type_err:88
 param1@pos := type_err:90
 param0@width := type_err:89
 param1@width := type_err:91}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x44650d0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x4b3a550: 
	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,75)_g1 , __done )	Base relation: 
{__cost := 0
 y := havoc:83
 z := havoc:84
 param0 := havoc:83
 param1 := havoc:84
 param0@pos := type_err:88
 param1@pos := type_err:90
 param0@width := type_err:89
 param1@width := type_err:91}
    ( __pstate , (Unique State Name,57)_g1 , __done )	Base relation: 
{__cost := __cost':1538
 y := havoc:83
 z := havoc:84
 x := x':1537
 y := y':1536
 x := x':1535
 y := y':1534
 param0 := param0':1533
 param1 := param1':1532
 param0@pos := param0@pos':1531
 param1@pos := param1@pos':1530
 param0@width := param0@width':1529
 param1@width := param1@width':1528
 when ((!(0 <= K:1515) \/ mid_param0:1516 = (havoc:83 + -K:1515))
         /\ (!(0 <= K:1515) \/ mid_param1:1517 = (havoc:84 + (2 * K:1515)))
         /\ (!((0 <= K:1515 /\ K:1515 <= 0))
               \/ mid_y:1518 = (y:1 + (2 * K:1515)))
         /\ (!(1 <= K:1515) \/ mid_y:1518 = (havoc:84 + (2 * K:1515)))
         /\ (!((0 <= K:1515 /\ K:1515 <= 0))
               \/ mid_y:1519 = (y:177 + (2 * K:1515)))
         /\ (!(1 <= K:1515) \/ mid_y:1519 = (-2 + havoc:84 + (2 * K:1515)))
         /\ (!(0 <= K:1515) \/ mid___cost:1520 = (2 * K:1515))
         /\ (!((0 <= K:1515 /\ K:1515 <= 0))
               \/ mid_x:1521 = (x:176 + -K:1515))
         /\ (!(1 <= K:1515) \/ mid_x:1521 = (havoc:83 + -K:1515))
         /\ (!((0 <= K:1515 /\ K:1515 <= 0)) \/ mid_x:1522 = (x:2 + -K:1515))
         /\ (!(1 <= K:1515) \/ mid_x:1522 = (havoc:83 + -K:1515))
         /\ ((K:1515 = 0 /\ type_err:1456 = mid_param1@width:1523
                /\ type_err:1455 = mid_param0@width:1524
                /\ type_err:1454 = mid_param1@pos:1525
                /\ type_err:1453 = mid_param0@pos:1526
                /\ havoc:84 = mid_param1:1517 /\ havoc:83 = mid_param0:1516
                /\ y:177 = mid_y:1519 /\ x:176 = mid_x:1521
                /\ y:1 = mid_y:1518 /\ x:2 = mid_x:1522
                /\ 0 = mid___cost:1520)
               \/ (1 <= K:1515 /\ 0 <= (-3 + -havoc:84 + havoc:83)
                     /\ (-2 + -mid_y:1519 + mid_param1:1517) = 0
                     /\ (-2 + -mid_y:1519 + mid_y:1518) = 0
                     /\ (-mid_x:1522 + mid_param0:1516) = 0
                     /\ (-mid_x:1522 + mid_x:1521) = 0
                     /\ 0 <= (-2 + -mid_y:1519 + mid_x:1522)
                     /\ 0 <= (-2 + mid___cost:1520))) /\ K:1527 = 0
         /\ mid_param1@width:1523 = param1@width':1528
         /\ mid_param0@width:1524 = param0@width':1529
         /\ mid_param1@pos:1525 = param1@pos':1530
         /\ mid_param0@pos:1526 = param0@pos':1531
         /\ mid_param1:1517 = param1':1532 /\ mid_param0:1516 = param0':1533
         /\ mid_y:1519 = y':1534 /\ mid_x:1521 = x':1535
         /\ mid_y:1518 = y':1536 /\ mid_x:1522 = x':1537
         /\ mid___cost:1520 = __cost':1538 /\ 0 = K:1527
         /\ (K:1515 + K:1527) = K:1539 /\ 0 <= K:1539)}
    ( __pstate , (Unique State Name,63)_g1 , __done )	Base relation: 
{__cost := (__cost':1618 + 1)
 y := havoc:83
 z := havoc:84
 x := x':1617
 y := y':1616
 x := (param0':1613 + -1)
 y := param1':1612
 param0 := (param0':1613 + -1)
 param1 := param1':1612
 param0@pos := type_err:1620
 param1@pos := type_err:1621
 param0@width := type_err:1622
 param1@width := type_err:1623
 when ((!(0 <= K:1595) \/ mid_param0:1596 = (havoc:83 + -K:1595))
         /\ (!(0 <= K:1595) \/ mid_param1:1597 = (havoc:84 + (2 * K:1595)))
         /\ (!((0 <= K:1595 /\ K:1595 <= 0))
               \/ mid_y:1598 = (y:1 + (2 * K:1595)))
         /\ (!(1 <= K:1595) \/ mid_y:1598 = (havoc:84 + (2 * K:1595)))
         /\ (!((0 <= K:1595 /\ K:1595 <= 0))
               \/ mid_y:1599 = (y:177 + (2 * K:1595)))
         /\ (!(1 <= K:1595) \/ mid_y:1599 = (-2 + havoc:84 + (2 * K:1595)))
         /\ (!(0 <= K:1595) \/ mid___cost:1600 = (2 * K:1595))
         /\ (!((0 <= K:1595 /\ K:1595 <= 0))
               \/ mid_x:1601 = (x:176 + -K:1595))
         /\ (!(1 <= K:1595) \/ mid_x:1601 = (havoc:83 + -K:1595))
         /\ (!((0 <= K:1595 /\ K:1595 <= 0)) \/ mid_x:1602 = (x:2 + -K:1595))
         /\ (!(1 <= K:1595) \/ mid_x:1602 = (havoc:83 + -K:1595))
         /\ ((K:1595 = 0 /\ type_err:1547 = mid_param1@width:1603
                /\ type_err:1546 = mid_param0@width:1604
                /\ type_err:1545 = mid_param1@pos:1605
                /\ type_err:1544 = mid_param0@pos:1606
                /\ havoc:84 = mid_param1:1597 /\ havoc:83 = mid_param0:1596
                /\ y:177 = mid_y:1599 /\ x:176 = mid_x:1601
                /\ y:1 = mid_y:1598 /\ x:2 = mid_x:1602
                /\ 0 = mid___cost:1600)
               \/ (1 <= K:1595 /\ 0 <= (-3 + -havoc:84 + havoc:83)
                     /\ (-2 + -mid_y:1599 + mid_param1:1597) = 0
                     /\ (-2 + -mid_y:1599 + mid_y:1598) = 0
                     /\ (-mid_x:1602 + mid_param0:1596) = 0
                     /\ (-mid_x:1602 + mid_x:1601) = 0
                     /\ 0 <= (-2 + -mid_y:1599 + mid_x:1602)
                     /\ 0 <= (-2 + mid___cost:1600))) /\ K:1607 = 0
         /\ mid_param1@width:1603 = param1@width':1608
         /\ mid_param0@width:1604 = param0@width':1609
         /\ mid_param1@pos:1605 = param1@pos':1610
         /\ mid_param0@pos:1606 = param0@pos':1611
         /\ mid_param1:1597 = param1':1612 /\ mid_param0:1596 = param0':1613
         /\ mid_y:1599 = y':1614 /\ mid_x:1601 = x':1615
         /\ mid_y:1598 = y':1616 /\ mid_x:1602 = x':1617
         /\ mid___cost:1600 = __cost':1618 /\ 0 = K:1607
         /\ (K:1595 + K:1607) = K:1619 /\ 0 <= K:1619 /\ 0 <= __cost':1618
         /\ 0 <= (__cost':1618 + 1) /\ param1':1612 < param0':1613)}
    ( __pstate , (Unique State Name,69)_g1 , __done )	Base relation: 
{__cost := 0
 y := havoc:83
 z := havoc:84
 param0 := havoc:83
 param1 := havoc:84
 param0@pos := type_err:1624
 param1@pos := type_err:1625
 param0@width := type_err:1626
 param1@width := type_err:1627}

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

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

Base relation: 
{__cost := phi___cost:1290
 x := phi_x:1289
 y := param1:21
 return := havoc:1291
 param0 := phi_param0:1287
 param1 := phi_param1:1286
 return@pos := type_err:1292
 param0@pos := phi_param0@pos:1284
 param1@pos := phi_param1@pos:1283
 return@width := type_err:1293
 param0@width := phi_param0@width:1281
 param1@width := phi_param1@width:1280
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:1290 /\ param0:18 = phi_x:1289
          /\ return:250 = phi_return:1288 /\ param0:18 = phi_param0:1287
          /\ param1:21 = phi_param1:1286
          /\ return@pos:246 = phi_return@pos:1285
          /\ param0@pos:17 = phi_param0@pos:1284
          /\ param1@pos:20 = phi_param1@pos:1283
          /\ return@width:242 = phi_return@width:1282
          /\ param0@width:16 = phi_param0@width:1281
          /\ param1@width:19 = phi_param1@width:1280)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:1229 /\ 0 <= (fresh___cost:1229 + 1)
                      /\ fresh_param0:1230 <= (fresh_param1:1231 + 1)
                      /\ (fresh___cost:1229 + 1) = phi___cost:1232
                      /\ fresh_param1:1231 = phi_y:1233
                      /\ return:250 = phi_return:1234
                      /\ fresh_param0:1230 = phi_param0:1235
                      /\ fresh_param1:1231 = phi_param1:1236
                      /\ return@pos:246 = phi_return@pos:1237
                      /\ fresh_param0@pos:1238 = phi_param0@pos:1239
                      /\ fresh_param1@pos:1240 = phi_param1@pos:1241
                      /\ return@width:242 = phi_return@width:1242
                      /\ fresh_param0@width:1243 = phi_param0@width:1244
                      /\ fresh_param1@width:1245 = phi_param1@width:1246)
                     \/ (0 <= fresh___cost:1229
                           /\ 0 <= (fresh___cost:1229 + 1)
                           /\ (fresh_param1:1231 + 1) < fresh_param0:1230
                           /\ 0 <= (fresh___cost:1229 + 1)
                           /\ 0 <= ((fresh___cost:1229 + 1) + 1)
                           /\ fresh_param0:1230 <= (fresh_param1:1231 + 2)
                           /\ ((fresh___cost:1229 + 1) + 1) = phi___cost:1232
                           /\ (fresh_param1:1231 + 2) = phi_y:1233
                           /\ havoc:1247 = phi_return:1234
                           /\ fresh_param0:1230 = phi_param0:1235
                           /\ (fresh_param1:1231 + 2) = phi_param1:1236
                           /\ type_err:1248 = phi_return@pos:1237
                           /\ type_err:1249 = phi_param0@pos:1239
                           /\ type_err:1250 = phi_param1@pos:1241
                           /\ type_err:1251 = phi_return@width:1242
                           /\ type_err:1252 = phi_param0@width:1244
                           /\ type_err:1253 = phi_param1@width:1246))
               /\ (!(0 <= K:1254)
                     \/ mid_(NewtonDomain.Left param0):1255 = (fresh_param0:1230
                                                                 + K:1254))
               /\ (!(0 <= K:1254)
                     \/ mid_(NewtonDomain.Left param1):1256 = (fresh_param1:1231
                                                                 + (-2
                                                                    * K:1254)))
               /\ (!(0 <= K:1254)
                     \/ mid_(NewtonDomain.Left __cost):1257 = (fresh___cost:1229
                                                                 + (-2
                                                                    * K:1254)))
               /\ ((K:1254 = 0
                      /\ type_err:1258 = mid_(NewtonDomain.Right return@width):1259
                      /\ type_err:1260 = mid_(NewtonDomain.Right return@pos):1261
                      /\ havoc:1262 = mid_(NewtonDomain.Right return):1263
                      /\ fresh_param1@width:1245 = mid_(NewtonDomain.Left param1@width):1264
                      /\ fresh_param0@width:1243 = mid_(NewtonDomain.Left param0@width):1265
                      /\ fresh_param1@pos:1240 = mid_(NewtonDomain.Left param1@pos):1266
                      /\ fresh_param0@pos:1238 = mid_(NewtonDomain.Left param0@pos):1267
                      /\ fresh_param1:1231 = mid_(NewtonDomain.Left param1):1256
                      /\ fresh_param0:1230 = mid_(NewtonDomain.Left param0):1255
                      /\ fresh___cost:1229 = mid_(NewtonDomain.Left __cost):1257)
                     \/ (1 <= K:1254 /\ 0 <= (-2 + fresh___cost:1229)
                           /\ 0 <= (fresh_param0:1230 + -fresh_param1:1231)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1257
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):1255
                                      + -mid_(NewtonDomain.Left param1):1256)))
               /\ K:1268 = 0
               /\ mid_(NewtonDomain.Right return@width):1259 = (NewtonDomain.Right return@width)':1269
               /\ mid_(NewtonDomain.Right return@pos):1261 = (NewtonDomain.Right return@pos)':1270
               /\ mid_(NewtonDomain.Right return):1263 = (NewtonDomain.Right return)':1271
               /\ mid_(NewtonDomain.Left param1@width):1264 = (NewtonDomain.Left param1@width)':1272
               /\ mid_(NewtonDomain.Left param0@width):1265 = (NewtonDomain.Left param0@width)':1273
               /\ mid_(NewtonDomain.Left param1@pos):1266 = (NewtonDomain.Left param1@pos)':1274
               /\ mid_(NewtonDomain.Left param0@pos):1267 = (NewtonDomain.Left param0@pos)':1275
               /\ mid_(NewtonDomain.Left param1):1256 = (NewtonDomain.Left param1)':1276
               /\ mid_(NewtonDomain.Left param0):1255 = (NewtonDomain.Left param0)':1277
               /\ mid_(NewtonDomain.Left __cost):1257 = (NewtonDomain.Left __cost)':1278
               /\ 0 = K:1268 /\ (K:1254 + K:1268) = K:1279 /\ 0 <= K:1279
               /\ type_err:228 = (NewtonDomain.Left param1@width)':1272
               /\ type_err:227 = (NewtonDomain.Left param0@width)':1273
               /\ type_err:226 = (NewtonDomain.Left param1@pos)':1274
               /\ type_err:225 = (NewtonDomain.Left param0@pos)':1275
               /\ param1:21 = (NewtonDomain.Left param1)':1276
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':1277
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':1278
               /\ phi___cost:1232 = phi___cost:1290
               /\ (param0:18 + -1) = phi_x:1289
               /\ (NewtonDomain.Right return)':1271 = phi_return:1288
               /\ phi_param0:1235 = phi_param0:1287
               /\ phi_param1:1236 = phi_param1:1286
               /\ (NewtonDomain.Right return@pos)':1270 = phi_return@pos:1285
               /\ phi_param0@pos:1239 = phi_param0@pos:1284
               /\ phi_param1@pos:1241 = phi_param1@pos:1283
               /\ (NewtonDomain.Right return@width)':1269 = phi_return@width:1282
               /\ phi_param0@width:1244 = phi_param0@width:1281
               /\ phi_param1@width:1246 = phi_param1@width:1280))}

------------------------------------------------
Procedure summary for count_up

Base relation: 
{__cost := phi___cost:1373
 x := param0:18
 y := phi_y:1372
 return := havoc:1374
 param0 := phi_param0:1370
 param1 := phi_param1:1369
 return@pos := type_err:1375
 param0@pos := phi_param0@pos:1367
 param1@pos := phi_param1@pos:1366
 return@width := type_err:1376
 param0@width := phi_param0@width:1364
 param1@width := phi_param1@width:1363
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= (param1:21 + 1)
          /\ (__cost:0 + 1) = phi___cost:1373 /\ param1:21 = phi_y:1372
          /\ return:250 = phi_return:1371 /\ param0:18 = phi_param0:1370
          /\ param1:21 = phi_param1:1369
          /\ return@pos:246 = phi_return@pos:1368
          /\ param0@pos:17 = phi_param0@pos:1367
          /\ param1@pos:20 = phi_param1@pos:1366
          /\ return@width:242 = phi_return@width:1365
          /\ param0@width:16 = phi_param0@width:1364
          /\ param1@width:19 = phi_param1@width:1363)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1)
               /\ (param1:21 + 1) < param0:18
               /\ ((0 <= (__cost:0 + 1) /\ 0 <= ((__cost:0 + 1) + 1)
                      /\ param0:18 <= (param1:21 + 2)
                      /\ ((__cost:0 + 1) + 1) = phi___cost:1294
                      /\ param0:18 = phi_x:1295
                      /\ return:250 = phi_return:1296
                      /\ param0:18 = phi_param0:1297
                      /\ (param1:21 + 2) = phi_param1:1298
                      /\ return@pos:246 = phi_return@pos:1299
                      /\ type_err:229 = phi_param0@pos:1300
                      /\ type_err:230 = phi_param1@pos:1301
                      /\ return@width:242 = phi_return@width:1302
                      /\ type_err:231 = phi_param0@width:1303
                      /\ type_err:232 = phi_param1@width:1304)
                     \/ (0 <= (__cost:0 + 1) /\ 0 <= ((__cost:0 + 1) + 1)
                           /\ (param1:21 + 2) < param0:18
                           /\ ((0 <= fresh___cost:1305
                                  /\ 0 <= (fresh___cost:1305 + 1)
                                  /\ fresh_param0:1306 <= (fresh_param1:1307
                                                             + 1)
                                  /\ (fresh___cost:1305 + 1) = phi___cost:1308
                                  /\ fresh_param1:1307 = phi_y:1309
                                  /\ return:250 = phi_return:1310
                                  /\ fresh_param0:1306 = phi_param0:1311
                                  /\ fresh_param1:1307 = phi_param1:1312
                                  /\ return@pos:246 = phi_return@pos:1313
                                  /\ fresh_param0@pos:1314 = phi_param0@pos:1315
                                  /\ fresh_param1@pos:1316 = phi_param1@pos:1317
                                  /\ return@width:242 = phi_return@width:1318
                                  /\ fresh_param0@width:1319 = phi_param0@width:1320
                                  /\ fresh_param1@width:1321 = phi_param1@width:1322)
                                 \/ (0 <= fresh___cost:1305
                                       /\ 0 <= (fresh___cost:1305 + 1)
                                       /\ (fresh_param1:1307 + 1) < fresh_param0:1306
                                       /\ 0 <= (fresh___cost:1305 + 1)
                                       /\ 0 <= ((fresh___cost:1305 + 1) + 1)
                                       /\ fresh_param0:1306 <= (fresh_param1:1307
                                                                  + 2)
                                       /\ ((fresh___cost:1305 + 1) + 1) = phi___cost:1308
                                       /\ (fresh_param1:1307 + 2) = phi_y:1309
                                       /\ havoc:1323 = phi_return:1310
                                       /\ fresh_param0:1306 = phi_param0:1311
                                       /\ (fresh_param1:1307 + 2) = phi_param1:1312
                                       /\ type_err:1324 = phi_return@pos:1313
                                       /\ type_err:1325 = phi_param0@pos:1315
                                       /\ type_err:1326 = phi_param1@pos:1317
                                       /\ type_err:1327 = phi_return@width:1318
                                       /\ type_err:1328 = phi_param0@width:1320
                                       /\ type_err:1329 = phi_param1@width:1322))
                           /\ (!(0 <= K:1330)
                                 \/ mid_(NewtonDomain.Left param0):1331 = (
                                    fresh_param0:1306 + K:1330))
                           /\ (!(0 <= K:1330)
                                 \/ mid_(NewtonDomain.Left param1):1332 = (
                                    fresh_param1:1307 + (-2 * K:1330)))
                           /\ (!(0 <= K:1330)
                                 \/ mid_(NewtonDomain.Left __cost):1333 = (
                                    fresh___cost:1305 + (-2 * K:1330)))
                           /\ ((K:1330 = 0
                                  /\ type_err:1334 = mid_(NewtonDomain.Right return@width):1335
                                  /\ type_err:1336 = mid_(NewtonDomain.Right return@pos):1337
                                  /\ havoc:1338 = mid_(NewtonDomain.Right return):1339
                                  /\ fresh_param1@width:1321 = mid_(NewtonDomain.Left param1@width):1340
                                  /\ fresh_param0@width:1319 = mid_(NewtonDomain.Left param0@width):1341
                                  /\ fresh_param1@pos:1316 = mid_(NewtonDomain.Left param1@pos):1342
                                  /\ fresh_param0@pos:1314 = mid_(NewtonDomain.Left param0@pos):1343
                                  /\ fresh_param1:1307 = mid_(NewtonDomain.Left param1):1332
                                  /\ fresh_param0:1306 = mid_(NewtonDomain.Left param0):1331
                                  /\ fresh___cost:1305 = mid_(NewtonDomain.Left __cost):1333)
                                 \/ (1 <= K:1330
                                       /\ 0 <= (-2 + fresh___cost:1305)
                                       /\ 0 <= (fresh_param0:1306
                                                  + -fresh_param1:1307)
                                       /\ 0 <= mid_(NewtonDomain.Left __cost):1333
                                       /\ 0 <= (-3
                                                  + mid_(NewtonDomain.Left param0):1331
                                                  + -mid_(NewtonDomain.Left param1):1332)))
                           /\ K:1344 = 0
                           /\ mid_(NewtonDomain.Right return@width):1335 = (NewtonDomain.Right return@width)':1345
                           /\ mid_(NewtonDomain.Right return@pos):1337 = (NewtonDomain.Right return@pos)':1346
                           /\ mid_(NewtonDomain.Right return):1339 = (NewtonDomain.Right return)':1347
                           /\ mid_(NewtonDomain.Left param1@width):1340 = (NewtonDomain.Left param1@width)':1348
                           /\ mid_(NewtonDomain.Left param0@width):1341 = (NewtonDomain.Left param0@width)':1349
                           /\ mid_(NewtonDomain.Left param1@pos):1342 = (NewtonDomain.Left param1@pos)':1350
                           /\ mid_(NewtonDomain.Left param0@pos):1343 = (NewtonDomain.Left param0@pos)':1351
                           /\ mid_(NewtonDomain.Left param1):1332 = (NewtonDomain.Left param1)':1352
                           /\ mid_(NewtonDomain.Left param0):1331 = (NewtonDomain.Left param0)':1353
                           /\ mid_(NewtonDomain.Left __cost):1333 = (NewtonDomain.Left __cost)':1354
                           /\ 0 = K:1344 /\ (K:1330 + K:1344) = K:1355
                           /\ 0 <= K:1355
                           /\ type_err:1356 = (NewtonDomain.Left param1@width)':1348
                           /\ type_err:1357 = (NewtonDomain.Left param0@width)':1349
                           /\ type_err:1358 = (NewtonDomain.Left param1@pos)':1350
                           /\ type_err:1359 = (NewtonDomain.Left param0@pos)':1351
                           /\ (param1:21 + 2) = (NewtonDomain.Left param1)':1352
                           /\ (param0:18 + -1) = (NewtonDomain.Left param0)':1353
                           /\ ((__cost:0 + 1) + 1) = (NewtonDomain.Left __cost)':1354
                           /\ phi___cost:1308 = phi___cost:1294
                           /\ (param0:18 + -1) = phi_x:1295
                           /\ (NewtonDomain.Right return)':1347 = phi_return:1296
                           /\ phi_param0:1311 = phi_param0:1297
                           /\ phi_param1:1312 = phi_param1:1298
                           /\ (NewtonDomain.Right return@pos)':1346 = phi_return@pos:1299
                           /\ phi_param0@pos:1315 = phi_param0@pos:1300
                           /\ phi_param1@pos:1317 = phi_param1@pos:1301
                           /\ (NewtonDomain.Right return@width)':1345 = phi_return@width:1302
                           /\ phi_param0@width:1320 = phi_param0@width:1303
                           /\ phi_param1@width:1322 = phi_param1@width:1304))
               /\ phi___cost:1294 = phi___cost:1373
               /\ (param1:21 + 2) = phi_y:1372
               /\ havoc:1360 = phi_return:1371
               /\ phi_param0:1297 = phi_param0:1370
               /\ phi_param1:1298 = phi_param1:1369
               /\ type_err:1361 = phi_return@pos:1368
               /\ phi_param0@pos:1300 = phi_param0@pos:1367
               /\ phi_param1@pos:1301 = phi_param1@pos:1366
               /\ type_err:1362 = phi_return@width:1365
               /\ phi_param0@width:1303 = phi_param0@width:1364
               /\ phi_param1@width:1304 = phi_param1@width:1363))}

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

Base relation: 
{__cost := phi___cost:1077
 y := havoc:83
 z := havoc:84
 return := 0
 param0 := phi_param0:1080
 param1 := phi_param1:1081
 return@pos := type_err:1151
 param0@pos := phi_param0@pos:1084
 param1@pos := phi_param1@pos:1086
 return@width := type_err:1152
 param0@width := phi_param0@width:1089
 param1@width := phi_param1@width:1091
 when (((havoc:83 <= havoc:84 /\ 1 = phi___cost:1077 /\ havoc:83 = phi_x:1078
           /\ return:250 = phi_return:1079 /\ havoc:83 = phi_param0:1080
           /\ havoc:84 = phi_param1:1081
           /\ return@pos:246 = phi_return@pos:1082
           /\ type_err:1083 = phi_param0@pos:1084
           /\ type_err:1085 = phi_param1@pos:1086
           /\ return@width:242 = phi_return@width:1087
           /\ type_err:1088 = phi_param0@width:1089
           /\ type_err:1090 = phi_param1@width:1091)
          \/ (havoc:84 < havoc:83
                /\ ((0 <= fresh___cost:1092 /\ 0 <= (fresh___cost:1092 + 1)
                       /\ fresh_param0:1093 <= (fresh_param1:1094 + 1)
                       /\ (fresh___cost:1092 + 1) = phi___cost:1095
                       /\ fresh_param1:1094 = phi_y:1096
                       /\ return:250 = phi_return:1097
                       /\ fresh_param0:1093 = phi_param0:1098
                       /\ fresh_param1:1094 = phi_param1:1099
                       /\ return@pos:246 = phi_return@pos:1100
                       /\ fresh_param0@pos:1101 = phi_param0@pos:1102
                       /\ fresh_param1@pos:1103 = phi_param1@pos:1104
                       /\ return@width:242 = phi_return@width:1105
                       /\ fresh_param0@width:1106 = phi_param0@width:1107
                       /\ fresh_param1@width:1108 = phi_param1@width:1109)
                      \/ (0 <= fresh___cost:1092
                            /\ 0 <= (fresh___cost:1092 + 1)
                            /\ (fresh_param1:1094 + 1) < fresh_param0:1093
                            /\ 0 <= (fresh___cost:1092 + 1)
                            /\ 0 <= ((fresh___cost:1092 + 1) + 1)
                            /\ fresh_param0:1093 <= (fresh_param1:1094 + 2)
                            /\ ((fresh___cost:1092 + 1) + 1) = phi___cost:1095
                            /\ (fresh_param1:1094 + 2) = phi_y:1096
                            /\ havoc:1110 = phi_return:1097
                            /\ fresh_param0:1093 = phi_param0:1098
                            /\ (fresh_param1:1094 + 2) = phi_param1:1099
                            /\ type_err:1111 = phi_return@pos:1100
                            /\ type_err:1112 = phi_param0@pos:1102
                            /\ type_err:1113 = phi_param1@pos:1104
                            /\ type_err:1114 = phi_return@width:1105
                            /\ type_err:1115 = phi_param0@width:1107
                            /\ type_err:1116 = phi_param1@width:1109))
                /\ (!(0 <= K:1117)
                      \/ mid_(NewtonDomain.Left param0):1118 = (fresh_param0:1093
                                                                  + K:1117))
                /\ (!(0 <= K:1117)
                      \/ mid_(NewtonDomain.Left param1):1119 = (fresh_param1:1094
                                                                  + (
                                                                  -2 * K:1117)))
                /\ (!(0 <= K:1117)
                      \/ mid_(NewtonDomain.Left __cost):1120 = (fresh___cost:1092
                                                                  + (
                                                                  -2 * K:1117)))
                /\ ((K:1117 = 0
                       /\ type_err:1121 = mid_(NewtonDomain.Right return@width):1122
                       /\ type_err:1123 = mid_(NewtonDomain.Right return@pos):1124
                       /\ havoc:1125 = mid_(NewtonDomain.Right return):1126
                       /\ fresh_param1@width:1108 = mid_(NewtonDomain.Left param1@width):1127
                       /\ fresh_param0@width:1106 = mid_(NewtonDomain.Left param0@width):1128
                       /\ fresh_param1@pos:1103 = mid_(NewtonDomain.Left param1@pos):1129
                       /\ fresh_param0@pos:1101 = mid_(NewtonDomain.Left param0@pos):1130
                       /\ fresh_param1:1094 = mid_(NewtonDomain.Left param1):1119
                       /\ fresh_param0:1093 = mid_(NewtonDomain.Left param0):1118
                       /\ fresh___cost:1092 = mid_(NewtonDomain.Left __cost):1120)
                      \/ (1 <= K:1117 /\ 0 <= (-2 + fresh___cost:1092)
                            /\ 0 <= (fresh_param0:1093 + -fresh_param1:1094)
                            /\ 0 <= mid_(NewtonDomain.Left __cost):1120
                            /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):1118
                                       + -mid_(NewtonDomain.Left param1):1119)))
                /\ K:1131 = 0
                /\ mid_(NewtonDomain.Right return@width):1122 = (NewtonDomain.Right return@width)':1132
                /\ mid_(NewtonDomain.Right return@pos):1124 = (NewtonDomain.Right return@pos)':1133
                /\ mid_(NewtonDomain.Right return):1126 = (NewtonDomain.Right return)':1134
                /\ mid_(NewtonDomain.Left param1@width):1127 = (NewtonDomain.Left param1@width)':1135
                /\ mid_(NewtonDomain.Left param0@width):1128 = (NewtonDomain.Left param0@width)':1136
                /\ mid_(NewtonDomain.Left param1@pos):1129 = (NewtonDomain.Left param1@pos)':1137
                /\ mid_(NewtonDomain.Left param0@pos):1130 = (NewtonDomain.Left param0@pos)':1138
                /\ mid_(NewtonDomain.Left param1):1119 = (NewtonDomain.Left param1)':1139
                /\ mid_(NewtonDomain.Left param0):1118 = (NewtonDomain.Left param0)':1140
                /\ mid_(NewtonDomain.Left __cost):1120 = (NewtonDomain.Left __cost)':1141
                /\ 0 = K:1131 /\ (K:1117 + K:1131) = K:1142 /\ 0 <= K:1142
                /\ type_err:1143 = (NewtonDomain.Left param1@width)':1135
                /\ type_err:1144 = (NewtonDomain.Left param0@width)':1136
                /\ type_err:1145 = (NewtonDomain.Left param1@pos)':1137
                /\ type_err:1146 = (NewtonDomain.Left param0@pos)':1138
                /\ havoc:84 = (NewtonDomain.Left param1)':1139
                /\ (havoc:83 + -1) = (NewtonDomain.Left param0)':1140
                /\ 1 = (NewtonDomain.Left __cost)':1141
                /\ phi___cost:1095 = phi___cost:1077
                /\ (havoc:83 + -1) = phi_x:1078
                /\ (NewtonDomain.Right return)':1134 = phi_return:1079
                /\ phi_param0:1098 = phi_param0:1080
                /\ phi_param1:1099 = phi_param1:1081
                /\ (NewtonDomain.Right return@pos)':1133 = phi_return@pos:1082
                /\ phi_param0@pos:1102 = phi_param0@pos:1084
                /\ phi_param1@pos:1104 = phi_param1@pos:1086
                /\ (NewtonDomain.Right return@width)':1132 = phi_return@width:1087
                /\ phi_param0@width:1107 = phi_param0@width:1089
                /\ phi_param1@width:1109 = phi_param1@width:1091))
         /\ ((havoc:84 < havoc:83
                /\ (havoc:83 + -havoc:84) = phi_tmp___1:1150)
               \/ (havoc:83 <= havoc:84 /\ 0 = phi_tmp___1:1150)))}

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

Base relation: 
{__cost := phi___cost:1153
 return := havoc:1226
 param0 := phi_param0:1156
 param1 := phi_param1:1157
 return@pos := type_err:1227
 param0@pos := phi_param0@pos:1160
 param1@pos := phi_param1@pos:1162
 return@width := type_err:1228
 param0@width := phi_param0@width:1165
 param1@width := phi_param1@width:1167
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:1153 /\ param0:18 = phi_x:1154
          /\ return:250 = phi_return:1155 /\ param0:18 = phi_param0:1156
          /\ param1:21 = phi_param1:1157
          /\ return@pos:246 = phi_return@pos:1158
          /\ type_err:1159 = phi_param0@pos:1160
          /\ type_err:1161 = phi_param1@pos:1162
          /\ return@width:242 = phi_return@width:1163
          /\ type_err:1164 = phi_param0@width:1165
          /\ type_err:1166 = phi_param1@width:1167)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:1168 /\ 0 <= (fresh___cost:1168 + 1)
                      /\ fresh_param0:1169 <= (fresh_param1:1170 + 1)
                      /\ (fresh___cost:1168 + 1) = phi___cost:1171
                      /\ fresh_param1:1170 = phi_y:1172
                      /\ return:250 = phi_return:1173
                      /\ fresh_param0:1169 = phi_param0:1174
                      /\ fresh_param1:1170 = phi_param1:1175
                      /\ return@pos:246 = phi_return@pos:1176
                      /\ fresh_param0@pos:1177 = phi_param0@pos:1178
                      /\ fresh_param1@pos:1179 = phi_param1@pos:1180
                      /\ return@width:242 = phi_return@width:1181
                      /\ fresh_param0@width:1182 = phi_param0@width:1183
                      /\ fresh_param1@width:1184 = phi_param1@width:1185)
                     \/ (0 <= fresh___cost:1168
                           /\ 0 <= (fresh___cost:1168 + 1)
                           /\ (fresh_param1:1170 + 1) < fresh_param0:1169
                           /\ 0 <= (fresh___cost:1168 + 1)
                           /\ 0 <= ((fresh___cost:1168 + 1) + 1)
                           /\ fresh_param0:1169 <= (fresh_param1:1170 + 2)
                           /\ ((fresh___cost:1168 + 1) + 1) = phi___cost:1171
                           /\ (fresh_param1:1170 + 2) = phi_y:1172
                           /\ havoc:1186 = phi_return:1173
                           /\ fresh_param0:1169 = phi_param0:1174
                           /\ (fresh_param1:1170 + 2) = phi_param1:1175
                           /\ type_err:1187 = phi_return@pos:1176
                           /\ type_err:1188 = phi_param0@pos:1178
                           /\ type_err:1189 = phi_param1@pos:1180
                           /\ type_err:1190 = phi_return@width:1181
                           /\ type_err:1191 = phi_param0@width:1183
                           /\ type_err:1192 = phi_param1@width:1185))
               /\ (!(0 <= K:1193)
                     \/ mid_(NewtonDomain.Left param0):1194 = (fresh_param0:1169
                                                                 + K:1193))
               /\ (!(0 <= K:1193)
                     \/ mid_(NewtonDomain.Left param1):1195 = (fresh_param1:1170
                                                                 + (-2
                                                                    * K:1193)))
               /\ (!(0 <= K:1193)
                     \/ mid_(NewtonDomain.Left __cost):1196 = (fresh___cost:1168
                                                                 + (-2
                                                                    * K:1193)))
               /\ ((K:1193 = 0
                      /\ type_err:1197 = mid_(NewtonDomain.Right return@width):1198
                      /\ type_err:1199 = mid_(NewtonDomain.Right return@pos):1200
                      /\ havoc:1201 = mid_(NewtonDomain.Right return):1202
                      /\ fresh_param1@width:1184 = mid_(NewtonDomain.Left param1@width):1203
                      /\ fresh_param0@width:1182 = mid_(NewtonDomain.Left param0@width):1204
                      /\ fresh_param1@pos:1179 = mid_(NewtonDomain.Left param1@pos):1205
                      /\ fresh_param0@pos:1177 = mid_(NewtonDomain.Left param0@pos):1206
                      /\ fresh_param1:1170 = mid_(NewtonDomain.Left param1):1195
                      /\ fresh_param0:1169 = mid_(NewtonDomain.Left param0):1194
                      /\ fresh___cost:1168 = mid_(NewtonDomain.Left __cost):1196)
                     \/ (1 <= K:1193 /\ 0 <= (-2 + fresh___cost:1168)
                           /\ 0 <= (fresh_param0:1169 + -fresh_param1:1170)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1196
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):1194
                                      + -mid_(NewtonDomain.Left param1):1195)))
               /\ K:1207 = 0
               /\ mid_(NewtonDomain.Right return@width):1198 = (NewtonDomain.Right return@width)':1208
               /\ mid_(NewtonDomain.Right return@pos):1200 = (NewtonDomain.Right return@pos)':1209
               /\ mid_(NewtonDomain.Right return):1202 = (NewtonDomain.Right return)':1210
               /\ mid_(NewtonDomain.Left param1@width):1203 = (NewtonDomain.Left param1@width)':1211
               /\ mid_(NewtonDomain.Left param0@width):1204 = (NewtonDomain.Left param0@width)':1212
               /\ mid_(NewtonDomain.Left param1@pos):1205 = (NewtonDomain.Left param1@pos)':1213
               /\ mid_(NewtonDomain.Left param0@pos):1206 = (NewtonDomain.Left param0@pos)':1214
               /\ mid_(NewtonDomain.Left param1):1195 = (NewtonDomain.Left param1)':1215
               /\ mid_(NewtonDomain.Left param0):1194 = (NewtonDomain.Left param0)':1216
               /\ mid_(NewtonDomain.Left __cost):1196 = (NewtonDomain.Left __cost)':1217
               /\ 0 = K:1207 /\ (K:1193 + K:1207) = K:1218 /\ 0 <= K:1218
               /\ type_err:1219 = (NewtonDomain.Left param1@width)':1211
               /\ type_err:1220 = (NewtonDomain.Left param0@width)':1212
               /\ type_err:1221 = (NewtonDomain.Left param1@pos)':1213
               /\ type_err:1222 = (NewtonDomain.Left param0@pos)':1214
               /\ param1:21 = (NewtonDomain.Left param1)':1215
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':1216
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':1217
               /\ phi___cost:1171 = phi___cost:1153
               /\ (param0:18 + -1) = phi_x:1154
               /\ (NewtonDomain.Right return)':1210 = phi_return:1155
               /\ phi_param0:1174 = phi_param0:1156
               /\ phi_param1:1175 = phi_param1:1157
               /\ (NewtonDomain.Right return@pos)':1209 = phi_return@pos:1158
               /\ phi_param0@pos:1178 = phi_param0@pos:1160
               /\ phi_param1@pos:1180 = phi_param1@pos:1162
               /\ (NewtonDomain.Right return@width)':1208 = phi_return@width:1163
               /\ phi_param0@width:1183 = phi_param0@width:1165
               /\ phi_param1@width:1185 = phi_param1@width:1167))}

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

Base relation: 
{__cost := phi___cost:1377
 return := havoc:1446
 param0 := phi_param0:1380
 param1 := phi_param1:1381
 return@pos := type_err:1447
 param0@pos := phi_param0@pos:1383
 param1@pos := phi_param1@pos:1384
 return@width := type_err:1448
 param0@width := phi_param0@width:1386
 param1@width := phi_param1@width:1387
 when ((0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param0:18 <= param1:21
          /\ (__cost:0 + 1) = phi___cost:1377 /\ param0:18 = phi_x:1378
          /\ return:250 = phi_return:1379 /\ param0:18 = phi_param0:1380
          /\ param1:21 = phi_param1:1381
          /\ return@pos:246 = phi_return@pos:1382
          /\ type_err:163 = phi_param0@pos:1383
          /\ type_err:164 = phi_param1@pos:1384
          /\ return@width:242 = phi_return@width:1385
          /\ type_err:165 = phi_param0@width:1386
          /\ type_err:166 = phi_param1@width:1387)
         \/ (0 <= __cost:0 /\ 0 <= (__cost:0 + 1) /\ param1:21 < param0:18
               /\ ((0 <= fresh___cost:1388 /\ 0 <= (fresh___cost:1388 + 1)
                      /\ fresh_param0:1389 <= (fresh_param1:1390 + 1)
                      /\ (fresh___cost:1388 + 1) = phi___cost:1391
                      /\ fresh_param1:1390 = phi_y:1392
                      /\ return:250 = phi_return:1393
                      /\ fresh_param0:1389 = phi_param0:1394
                      /\ fresh_param1:1390 = phi_param1:1395
                      /\ return@pos:246 = phi_return@pos:1396
                      /\ fresh_param0@pos:1397 = phi_param0@pos:1398
                      /\ fresh_param1@pos:1399 = phi_param1@pos:1400
                      /\ return@width:242 = phi_return@width:1401
                      /\ fresh_param0@width:1402 = phi_param0@width:1403
                      /\ fresh_param1@width:1404 = phi_param1@width:1405)
                     \/ (0 <= fresh___cost:1388
                           /\ 0 <= (fresh___cost:1388 + 1)
                           /\ (fresh_param1:1390 + 1) < fresh_param0:1389
                           /\ 0 <= (fresh___cost:1388 + 1)
                           /\ 0 <= ((fresh___cost:1388 + 1) + 1)
                           /\ fresh_param0:1389 <= (fresh_param1:1390 + 2)
                           /\ ((fresh___cost:1388 + 1) + 1) = phi___cost:1391
                           /\ (fresh_param1:1390 + 2) = phi_y:1392
                           /\ havoc:1406 = phi_return:1393
                           /\ fresh_param0:1389 = phi_param0:1394
                           /\ (fresh_param1:1390 + 2) = phi_param1:1395
                           /\ type_err:1407 = phi_return@pos:1396
                           /\ type_err:1408 = phi_param0@pos:1398
                           /\ type_err:1409 = phi_param1@pos:1400
                           /\ type_err:1410 = phi_return@width:1401
                           /\ type_err:1411 = phi_param0@width:1403
                           /\ type_err:1412 = phi_param1@width:1405))
               /\ (!(0 <= K:1413)
                     \/ mid_(NewtonDomain.Left param0):1414 = (fresh_param0:1389
                                                                 + K:1413))
               /\ (!(0 <= K:1413)
                     \/ mid_(NewtonDomain.Left param1):1415 = (fresh_param1:1390
                                                                 + (-2
                                                                    * K:1413)))
               /\ (!(0 <= K:1413)
                     \/ mid_(NewtonDomain.Left __cost):1416 = (fresh___cost:1388
                                                                 + (-2
                                                                    * K:1413)))
               /\ ((K:1413 = 0
                      /\ type_err:1417 = mid_(NewtonDomain.Right return@width):1418
                      /\ type_err:1419 = mid_(NewtonDomain.Right return@pos):1420
                      /\ havoc:1421 = mid_(NewtonDomain.Right return):1422
                      /\ fresh_param1@width:1404 = mid_(NewtonDomain.Left param1@width):1423
                      /\ fresh_param0@width:1402 = mid_(NewtonDomain.Left param0@width):1424
                      /\ fresh_param1@pos:1399 = mid_(NewtonDomain.Left param1@pos):1425
                      /\ fresh_param0@pos:1397 = mid_(NewtonDomain.Left param0@pos):1426
                      /\ fresh_param1:1390 = mid_(NewtonDomain.Left param1):1415
                      /\ fresh_param0:1389 = mid_(NewtonDomain.Left param0):1414
                      /\ fresh___cost:1388 = mid_(NewtonDomain.Left __cost):1416)
                     \/ (1 <= K:1413 /\ 0 <= (-2 + fresh___cost:1388)
                           /\ 0 <= (fresh_param0:1389 + -fresh_param1:1390)
                           /\ 0 <= mid_(NewtonDomain.Left __cost):1416
                           /\ 0 <= (-3 + mid_(NewtonDomain.Left param0):1414
                                      + -mid_(NewtonDomain.Left param1):1415)))
               /\ K:1427 = 0
               /\ mid_(NewtonDomain.Right return@width):1418 = (NewtonDomain.Right return@width)':1428
               /\ mid_(NewtonDomain.Right return@pos):1420 = (NewtonDomain.Right return@pos)':1429
               /\ mid_(NewtonDomain.Right return):1422 = (NewtonDomain.Right return)':1430
               /\ mid_(NewtonDomain.Left param1@width):1423 = (NewtonDomain.Left param1@width)':1431
               /\ mid_(NewtonDomain.Left param0@width):1424 = (NewtonDomain.Left param0@width)':1432
               /\ mid_(NewtonDomain.Left param1@pos):1425 = (NewtonDomain.Left param1@pos)':1433
               /\ mid_(NewtonDomain.Left param0@pos):1426 = (NewtonDomain.Left param0@pos)':1434
               /\ mid_(NewtonDomain.Left param1):1415 = (NewtonDomain.Left param1)':1435
               /\ mid_(NewtonDomain.Left param0):1414 = (NewtonDomain.Left param0)':1436
               /\ mid_(NewtonDomain.Left __cost):1416 = (NewtonDomain.Left __cost)':1437
               /\ 0 = K:1427 /\ (K:1413 + K:1427) = K:1438 /\ 0 <= K:1438
               /\ type_err:1439 = (NewtonDomain.Left param1@width)':1431
               /\ type_err:1440 = (NewtonDomain.Left param0@width)':1432
               /\ type_err:1441 = (NewtonDomain.Left param1@pos)':1433
               /\ type_err:1442 = (NewtonDomain.Left param0@pos)':1434
               /\ param1:21 = (NewtonDomain.Left param1)':1435
               /\ (param0:18 + -1) = (NewtonDomain.Left param0)':1436
               /\ (__cost:0 + 1) = (NewtonDomain.Left __cost)':1437
               /\ phi___cost:1391 = phi___cost:1377
               /\ (param0:18 + -1) = phi_x:1378
               /\ (NewtonDomain.Right return)':1430 = phi_return:1379
               /\ phi_param0:1394 = phi_param0:1380
               /\ phi_param1:1395 = phi_param1:1381
               /\ (NewtonDomain.Right return@pos)':1429 = phi_return@pos:1382
               /\ phi_param0@pos:1398 = phi_param0@pos:1383
               /\ phi_param1@pos:1400 = phi_param1@pos:1384
               /\ (NewtonDomain.Right return@width)':1428 = phi_return@width:1385
               /\ phi_param0@width:1403 = phi_param0@width:1386
               /\ phi_param1@width:1405 = phi_param1@width:1387))}

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

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

Variable bounds at line 32 in run

min(min(min(min((3 + __cost), (1 + __cost)), (2 + __cost)),
        max((2/3 + (-2/3 * z) + (2/3 * y) + __cost), (4 + __cost))),
    max((1 + (-2/3 * z) + (2/3 * y) + __cost), (5 + __cost))) <= __cost
__cost is o(1)
__cost <= max(max(max(max((3 + __cost), (1 + __cost)), (2 + __cost)),
                  (4/3 + (-2/3 * z) + (2/3 * y) + __cost)),
              (5/3 + (-2/3 * z) + (2/3 * y) + __cost))
__cost is O(n)

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