/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, 72> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 73>	Base relation: 
{return := havoc:54
 return@pos := type_err:57
 return@width := type_err:58}	
<Unique State Name, 17> -> <Unique State Name, 71>	Base relation: 
{__cost := 0
 n := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}	
<Unique State Name, 26> -> <Unique State Name, 76>	Base relation: 
{when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93)}	
<Unique State Name, 75> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 70> -> <Unique State Name, 74>	Base relation: 
{return := 0
 return@pos := type_err:29
 return@width := type_err:30
 when ((0 < n:4 /\ n:4 = phi_tmp___1:22) \/ (n:4 <= 0 /\ 0 = phi_tmp___1:22))}	
<Unique State Name, 66> -> <Unique State Name, 65>	Base relation: 
{param0 := param0:71
 param1 := param1:74
 param0@pos := type_err:79
 param1@pos := type_err:80
 param0@width := type_err:81
 param1@width := type_err:82}	
<Unique State Name, 74> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 64> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 37> -> <Unique State Name, 53>	Base relation: 
{when va:95 <= 0}	
<Unique State Name, 37> -> <Unique State Name, 59>	Base relation: 
{when 0 < va:95}	
<Unique State Name, 58> -> <Unique State Name, 33>	Base relation: 
{tmp := havoc:103}	
<Unique State Name, 73> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 75 58>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 65> -> <Unique State Name, 60 64>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 60> -> <Unique State Name, 26>	Base relation: 
{va := param0:71
 vb := 0
 m := param1:74
 when 0 < param1:74}	
<Unique State Name, 76> -> <Unique State Name, 37>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, 66 70>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 53> -> <Unique State Name, 72>	Base relation: 
{return := havoc:98
 return@pos := type_err:101
 return@width := type_err:102}	
<Unique State Name, 33> -> <Unique State Name, 26>	Base relation: 
{__cost := (__cost:96 + 1)
 va := phi_va:106
 vb := phi_vb:107
 when (!(tmp:94 = 0) /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:106
                /\ (vb:97 + 1) = phi_vb:107)
               \/ (m:93 <= vb:97 /\ va:95 = phi_va:106 /\ 0 = phi_vb:107)))}	
<Unique State Name, 33> -> <Unique State Name, 53>	Base relation: 
{when tmp:94 = 0}	
#################################################################
           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  24  26  


New-style (IRE) regular expression in IREregExpMap for reID=6: 
Dot(
  Dot(
    Weight(Base relation: 
      {__cost := 0
       n := havoc:20
       param0 := havoc:20
       param1 := havoc:21
       param0@pos := type_err:25
       param1@pos := type_err:27
       param0@width := type_err:26
       param1@width := type_err:28}    )
    ,
    Var(13)
  )
  ,
  Weight(Base relation: 
    {return := 0
     return@pos := type_err:29
     return@width := type_err:30
     when ((0 < n:4 /\ n:4 = phi_tmp___1:22)
             \/ (n:4 <= 0 /\ 0 = phi_tmp___1:22))}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=13: 
Dot(
  Dot(
    Weight(Base relation: 
      {param0 := param0:71
       param1 := param1:74
       param0@pos := type_err:79
       param1@pos := type_err:80
       param0@width := type_err:81
       param1@width := type_err:82}    )
    ,
    Var(24)
  )
  ,
  Weight(Base relation: 
    {return := havoc:54
     return@pos := type_err:57
     return@width := type_err:58}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=24: 
Dot(
  Plus(
    Dot(
      Dot(
        Weight(Base relation: 
          {va := param0:71
           vb := 0
           m := param1:74
           when 0 < param1:74}        )
        ,
        Kleene( key=1
          Dot(
            Dot(
              Weight(Base relation: 
                {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}              )
              ,
              Var(26)
            )
            ,
            Weight(Base relation: 
              {__cost := (__cost:96 + 1)
               va := phi_va:276
               vb := phi_vb:277
               tmp := havoc:103
               when (!(havoc:103 = 0) /\ 0 <= __cost:96
                       /\ 0 <= (__cost:96 + 1)
                       /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                              /\ (vb:97 + 1) = phi_vb:277)
                             \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                   /\ 0 = phi_vb:277)))}            )
          )
        )
      )
      ,
      Weight(Base relation: 
        {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ va:95 <= 0)}      )
    )
    ,
    Dot(
      Dot(
        Dot(
          Weight(Base relation: 
            {va := param0:71
             vb := 0
             m := param1:74
             when 0 < param1:74}          )
          ,
          Kleene( key=1
            Dot(
              Dot(
                Weight(Base relation: 
                  {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}                )
                ,
                Var(26)
              )
              ,
              Weight(Base relation: 
                {__cost := (__cost:96 + 1)
                 va := phi_va:276
                 vb := phi_vb:277
                 tmp := havoc:103
                 when (!(havoc:103 = 0) /\ 0 <= __cost:96
                         /\ 0 <= (__cost:96 + 1)
                         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                /\ (vb:97 + 1) = phi_vb:277)
                               \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                     /\ 0 = phi_vb:277)))}              )
            )
          )
        )
        ,
        Dot(
          Dot(
            Weight(Base relation: 
              {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}            )
            ,
            Var(26)
          )
          ,
          Weight(Base relation: 
            {tmp := havoc:103}          )
        )
      )
      ,
      Weight(Base relation: 
        {when tmp:94 = 0}      )
    )
  )
  ,
  Weight(Base relation: 
    {return := havoc:98
     return@pos := type_err:101
     return@width := type_err:102}  )
)


New-style (IRE) regular expression in IREregExpMap for reID=26: 
One()



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
         n := havoc:20
         param0 := havoc:20
         param1 := havoc:21
         param0@pos := type_err:25
         param1@pos := type_err:27
         param0@width := type_err:26
         param1@width := type_err:28}      )
      ,
      Var(13)
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:29
       return@width := type_err:30
       when ((0 < n:4 /\ n:4 = phi_tmp___1:22)
               \/ (n:4 <= 0 /\ 0 = phi_tmp___1:22))}    )
  )
)



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

Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:71
         param1 := param1:74
         param0@pos := type_err:79
         param1@pos := type_err:80
         param0@width := type_err:81
         param1@width := type_err:82}      )
      ,
      Var(24)
    )
    ,
    Weight(Base relation: 
      {return := havoc:54
       return@pos := type_err:57
       return@width := type_err:58}    )
  )
)



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

Project(
  Dot(
    Plus(
      Dot(
        Dot(
          Weight(Base relation: 
            {va := param0:71
             vb := 0
             m := param1:74
             when 0 < param1:74}          )
          ,
          Kleene( key=1
            Dot(
              Dot(
                Weight(Base relation: 
                  {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}                )
                ,
                Var(26)
              )
              ,
              Weight(Base relation: 
                {__cost := (__cost:96 + 1)
                 va := phi_va:276
                 vb := phi_vb:277
                 tmp := havoc:103
                 when (!(havoc:103 = 0) /\ 0 <= __cost:96
                         /\ 0 <= (__cost:96 + 1)
                         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                /\ (vb:97 + 1) = phi_vb:277)
                               \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                     /\ 0 = phi_vb:277)))}              )
            )
          )
        )
        ,
        Weight(Base relation: 
          {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ va:95 <= 0)}        )
      )
      ,
      Dot(
        Dot(
          Dot(
            Weight(Base relation: 
              {va := param0:71
               vb := 0
               m := param1:74
               when 0 < param1:74}            )
            ,
            Kleene( key=1
              Dot(
                Dot(
                  Weight(Base relation: 
                    {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}                  )
                  ,
                  Var(26)
                )
                ,
                Weight(Base relation: 
                  {__cost := (__cost:96 + 1)
                   va := phi_va:276
                   vb := phi_vb:277
                   tmp := havoc:103
                   when (!(havoc:103 = 0) /\ 0 <= __cost:96
                           /\ 0 <= (__cost:96 + 1)
                           /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                  /\ (vb:97 + 1) = phi_vb:277)
                                 \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                       /\ 0 = phi_vb:277)))}                )
              )
            )
          )
          ,
          Dot(
            Dot(
              Weight(Base relation: 
                {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}              )
              ,
              Var(26)
            )
            ,
            Weight(Base relation: 
              {tmp := havoc:103}            )
          )
        )
        ,
        Weight(Base relation: 
          {when tmp:94 = 0}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:98
       return@pos := type_err:101
       return@width := type_err:102}    )
  )
)



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

One()



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {__cost := 0
         n := havoc:20
         param0 := havoc:20
         param1 := havoc:21
         param0@pos := type_err:25
         param1@pos := type_err:27
         param0@width := type_err:26
         param1@width := type_err:28}      )
      ,
      Project(
        Dot(
          Dot(
            Weight(Base relation: 
              {param0 := param0:71
               param1 := param1:74
               param0@pos := type_err:79
               param1@pos := type_err:80
               param0@width := type_err:81
               param1@width := type_err:82}            )
            ,
            Project(
              Dot(
                Plus(
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {va := param0:71
                         vb := 0
                         m := param1:74
                         when 0 < param1:74}                      )
                      ,
                      Kleene( key=1
                        Dot(
                          Dot(
                            Weight(Base relation: 
                              {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93
                                       /\ 0 < va:95)}                            )
                            ,
                            Var(26)
                          )
                          ,
                          Weight(Base relation: 
                            {__cost := (__cost:96 + 1)
                             va := phi_va:276
                             vb := phi_vb:277
                             tmp := havoc:103
                             when (!(havoc:103 = 0) /\ 0 <= __cost:96
                                     /\ 0 <= (__cost:96 + 1)
                                     /\ ((vb:97 < m:93
                                            /\ (va:95 + -1) = phi_va:276
                                            /\ (vb:97 + 1) = phi_vb:277)
                                           \/ (m:93 <= vb:97
                                                 /\ va:95 = phi_va:276
                                                 /\ 0 = phi_vb:277)))}                          )
                        )
                      )
                    )
                    ,
                    Weight(Base relation: 
                      {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ va:95 <= 0)}                    )
                  )
                  ,
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {va := param0:71
                         vb := 0
                         m := param1:74
                         when 0 < param1:74}                      )
                      ,
                      Kleene( key=1
                        Dot(
                          Dot(
                            Weight(Base relation: 
                              {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93
                                       /\ 0 < va:95)}                            )
                            ,
                            Var(26)
                          )
                          ,
                          Weight(Base relation: 
                            {__cost := (__cost:96 + 1)
                             va := phi_va:276
                             vb := phi_vb:277
                             tmp := havoc:103
                             when (!(havoc:103 = 0) /\ 0 <= __cost:96
                                     /\ 0 <= (__cost:96 + 1)
                                     /\ ((vb:97 < m:93
                                            /\ (va:95 + -1) = phi_va:276
                                            /\ (vb:97 + 1) = phi_vb:277)
                                           \/ (m:93 <= vb:97
                                                 /\ va:95 = phi_va:276
                                                 /\ 0 = phi_vb:277)))}                          )
                        )
                      )
                    )
                    ,
                    Weight(Base relation: 
                      {tmp := havoc:278
                       when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95
                               /\ havoc:278 = 0)}                    )
                  )
                )
                ,
                Weight(Base relation: 
                  {return := havoc:98
                   return@pos := type_err:101
                   return@width := type_err:102}                )
              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:54
             return@pos := type_err:57
             return@width := type_err:58}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := 0
       return@pos := type_err:29
       return@width := type_err:30
       when ((0 < n:4 /\ n:4 = phi_tmp___1:22)
               \/ (n:4 <= 0 /\ 0 = phi_tmp___1:22))}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Project(
  Dot(
    Dot(
      Weight(Base relation: 
        {param0 := param0:71
         param1 := param1:74
         param0@pos := type_err:79
         param1@pos := type_err:80
         param0@width := type_err:81
         param1@width := type_err:82}      )
      ,
      Project(
        Dot(
          Plus(
            Dot(
              Dot(
                Weight(Base relation: 
                  {va := param0:71
                   vb := 0
                   m := param1:74
                   when 0 < param1:74}                )
                ,
                Kleene( key=1
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93
                                 /\ 0 < va:95)}                      )
                      ,
                      Var(26)
                    )
                    ,
                    Weight(Base relation: 
                      {__cost := (__cost:96 + 1)
                       va := phi_va:276
                       vb := phi_vb:277
                       tmp := havoc:103
                       when (!(havoc:103 = 0) /\ 0 <= __cost:96
                               /\ 0 <= (__cost:96 + 1)
                               /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                      /\ (vb:97 + 1) = phi_vb:277)
                                     \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                           /\ 0 = phi_vb:277)))}                    )
                  )
                )
              )
              ,
              Weight(Base relation: 
                {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ va:95 <= 0)}              )
            )
            ,
            Dot(
              Dot(
                Weight(Base relation: 
                  {va := param0:71
                   vb := 0
                   m := param1:74
                   when 0 < param1:74}                )
                ,
                Kleene( key=1
                  Dot(
                    Dot(
                      Weight(Base relation: 
                        {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93
                                 /\ 0 < va:95)}                      )
                      ,
                      Var(26)
                    )
                    ,
                    Weight(Base relation: 
                      {__cost := (__cost:96 + 1)
                       va := phi_va:276
                       vb := phi_vb:277
                       tmp := havoc:103
                       when (!(havoc:103 = 0) /\ 0 <= __cost:96
                               /\ 0 <= (__cost:96 + 1)
                               /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                      /\ (vb:97 + 1) = phi_vb:277)
                                     \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                           /\ 0 = phi_vb:277)))}                    )
                  )
                )
              )
              ,
              Weight(Base relation: 
                {tmp := havoc:279
                 when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95
                         /\ havoc:279 = 0)}              )
            )
          )
          ,
          Weight(Base relation: 
            {return := havoc:98
             return@pos := type_err:101
             return@width := type_err:102}          )
        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:54
       return@pos := type_err:57
       return@width := type_err:58}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=24: 
Project(
  Dot(
    Plus(
      Dot(
        Dot(
          Weight(Base relation: 
            {va := param0:71
             vb := 0
             m := param1:74
             when 0 < param1:74}          )
          ,
          Kleene( key=1
            Dot(
              Dot(
                Weight(Base relation: 
                  {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}                )
                ,
                Var(26)
              )
              ,
              Weight(Base relation: 
                {__cost := (__cost:96 + 1)
                 va := phi_va:276
                 vb := phi_vb:277
                 tmp := havoc:103
                 when (!(havoc:103 = 0) /\ 0 <= __cost:96
                         /\ 0 <= (__cost:96 + 1)
                         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                /\ (vb:97 + 1) = phi_vb:277)
                               \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                     /\ 0 = phi_vb:277)))}              )
            )
          )
        )
        ,
        Weight(Base relation: 
          {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ va:95 <= 0)}        )
      )
      ,
      Dot(
        Dot(
          Weight(Base relation: 
            {va := param0:71
             vb := 0
             m := param1:74
             when 0 < param1:74}          )
          ,
          Kleene( key=1
            Dot(
              Dot(
                Weight(Base relation: 
                  {when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95)}                )
                ,
                Var(26)
              )
              ,
              Weight(Base relation: 
                {__cost := (__cost:96 + 1)
                 va := phi_va:276
                 vb := phi_vb:277
                 tmp := havoc:103
                 when (!(havoc:103 = 0) /\ 0 <= __cost:96
                         /\ 0 <= (__cost:96 + 1)
                         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:276
                                /\ (vb:97 + 1) = phi_vb:277)
                               \/ (m:93 <= vb:97 /\ va:95 = phi_va:276
                                     /\ 0 = phi_vb:277)))}              )
            )
          )
        )
        ,
        Weight(Base relation: 
          {tmp := havoc:280
           when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95
                   /\ havoc:280 = 0)}        )
      )
    )
    ,
    Weight(Base relation: 
      {return := havoc:98
       return@pos := type_err:101
       return@width := type_err:102}    )
  )
)


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=26: 
One()


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{when false}
**** alpha hat: 
  {<Split [true
            }
          pre:
            bottom
          post:
            bottom
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {when (K:282 = 0 /\ K:283 = 0 /\ 0 = K:283 /\ (K:282 + K:283) = K:281
           /\ 0 <= K:281)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := 0
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:319
 param0@pos := type_err:313
 param1@pos := type_err:314
 return@width := type_err:320
 param0@width := type_err:316
 param1@width := type_err:317
 when (((0 < havoc:21 /\ K:305 = 0 /\ K:306 = 0 /\ 0 = K:306
           /\ (K:305 + K:306) = K:307 /\ 0 <= K:307 /\ 1 <= havoc:21
           /\ 0 < havoc:21 /\ havoc:20 <= 0 /\ tmp:308 = phi_tmp:309)
          \/ (0 < havoc:21 /\ K:305 = 0 /\ K:306 = 0 /\ 0 = K:306
                /\ (K:305 + K:306) = K:307 /\ 0 <= K:307 /\ 1 <= havoc:21
                /\ 0 < havoc:21 /\ 0 < havoc:20 /\ havoc:310 = 0
                /\ havoc:310 = phi_tmp:309))
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:318)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:318)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := havoc:336
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:337
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:338
 param0@width := type_err:81
 param1@width := type_err:82
 when ((0 < param1:74 /\ K:327 = 0 /\ K:328 = 0 /\ 0 = K:328
          /\ (K:327 + K:328) = K:329 /\ 0 <= K:329 /\ 1 <= param1:74
          /\ 0 < param1:74 /\ param0:71 <= 0 /\ tmp:330 = phi_tmp:331)
         \/ (0 < param1:74 /\ K:327 = 0 /\ K:328 = 0 /\ 0 = K:328
               /\ (K:327 + K:328) = K:329 /\ 0 <= K:329 /\ 1 <= param1:74
               /\ 0 < param1:74 /\ 0 < param0:71 /\ havoc:332 = 0
               /\ havoc:332 = phi_tmp:331))}

Evaluating variable number 24 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{return := havoc:341
 return@pos := type_err:342
 return@width := type_err:343
 when ((0 < param1:74 /\ K:284 = 0 /\ K:285 = 0 /\ 0 = K:285
          /\ (K:284 + K:285) = K:286 /\ 0 <= K:286 /\ 1 <= param1:74
          /\ 0 < param1:74 /\ param0:71 <= 0 /\ tmp:344 = phi_tmp:340)
         \/ (0 < param1:74 /\ K:284 = 0 /\ K:285 = 0 /\ 0 = K:285
               /\ (K:284 + K:285) = K:286 /\ 0 <= K:286 /\ 1 <= param1:74
               /\ 0 < param1:74 /\ 0 < param0:71 /\ havoc:339 = 0
               /\ havoc:339 = phi_tmp:340))}

Evaluating variable number 26 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

    (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: Base relation: 
{__cost := (__cost:96 + 1)
 va := phi_va:346
 vb := phi_vb:347
 tmp := havoc:345
 when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95 /\ !(havoc:345 = 0)
         /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:346
                /\ (vb:97 + 1) = phi_vb:347)
               \/ (m:93 <= vb:97 /\ va:95 = phi_va:346 /\ 0 = phi_vb:347)))}
**** alpha hat: 
  {<Split [true
            (__cost':348) = (1)*(__cost:96) + 1
           (((2 * va':349) + vb':350)) <= (1)*(((2 * va:95) + vb:97))
                                           + (-1)*1
           (va':349) <= (1)*(va:95) + 0
           (-va':349) <= (1)*(-va:95) + 1
           }
          pre:
            [|vb:97>=0; m:93-1>=0; va:95-1>=0; __cost:96>=0|]
          post:
            [|-vb':350+m:93>=0; m:93-1>=0; vb':350>=0; va':349>=0;
              va':349+vb':350-1>=0; __cost':348-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':348
   va := va':349
   vb := vb':350
   tmp := tmp':351
   when ((!(0 <= K:363) \/ mid___cost:368 = (__cost:96 + K:363))
           /\ (!(0 <= K:363)
                 \/ ((2 * mid_va:367) + mid_vb:366) <= (((2 * va:95) + vb:97)
                                                          + -K:363))
           /\ (!(0 <= K:363) \/ mid_va:367 <= va:95)
           /\ (!(0 <= K:363) \/ -mid_va:367 <= (-va:95 + K:363))
           /\ ((K:363 = 0 /\ tmp:94 = mid_tmp:365 /\ vb:97 = mid_vb:366
                  /\ va:95 = mid_va:367 /\ __cost:96 = mid___cost:368)
                 \/ (1 <= K:363 /\ 0 <= vb:97 /\ 0 <= (-1 + m:93)
                       /\ 0 <= (-1 + va:95) /\ 0 <= __cost:96
                       /\ 0 <= (-mid_vb:366 + m:93) /\ 0 <= (-1 + m:93)
                       /\ 0 <= mid_vb:366 /\ 0 <= mid_va:367
                       /\ 0 <= (-1 + mid_va:367 + mid_vb:366)
                       /\ 0 <= (-1 + mid___cost:368))) /\ K:364 = 0
           /\ mid_tmp:365 = tmp':351 /\ mid_vb:366 = vb':350
           /\ mid_va:367 = va':349 /\ mid___cost:368 = __cost':348
           /\ 0 = K:364 /\ (K:363 + K:364) = K:362 /\ 0 <= K:362)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':416
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:428
 param0@pos := type_err:422
 param1@pos := type_err:423
 return@width := type_err:429
 param0@width := type_err:425
 param1@width := type_err:426
 when (((0 < havoc:21 /\ (!(0 <= K:406) \/ mid___cost:407 = K:406)
           /\ (!(0 <= K:406)
                 \/ ((2 * mid_va:408) + mid_vb:409) <= ((2 * havoc:20)
                                                          + -K:406))
           /\ (!(0 <= K:406) \/ mid_va:408 <= havoc:20)
           /\ (!(0 <= K:406) \/ -mid_va:408 <= (-havoc:20 + K:406))
           /\ ((K:406 = 0 /\ tmp:410 = mid_tmp:411 /\ 0 = mid_vb:409
                  /\ havoc:20 = mid_va:408 /\ 0 = mid___cost:407)
                 \/ (1 <= K:406 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + havoc:20)
                       /\ 0 <= (-mid_vb:409 + havoc:21)
                       /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:409
                       /\ 0 <= mid_va:408
                       /\ 0 <= (-1 + mid_va:408 + mid_vb:409)
                       /\ 0 <= (-1 + mid___cost:407))) /\ K:412 = 0
           /\ mid_tmp:411 = tmp':413 /\ mid_vb:409 = vb':414
           /\ mid_va:408 = va':415 /\ mid___cost:407 = __cost':416
           /\ 0 = K:412 /\ (K:406 + K:412) = K:417 /\ 0 <= K:417
           /\ 1 <= havoc:21 /\ 0 <= vb':414 /\ 0 < havoc:21 /\ va':415 <= 0
           /\ tmp':413 = phi_tmp:418)
          \/ (0 < havoc:21 /\ (!(0 <= K:406) \/ mid___cost:407 = K:406)
                /\ (!(0 <= K:406)
                      \/ ((2 * mid_va:408) + mid_vb:409) <= ((2 * havoc:20)
                                                               + -K:406))
                /\ (!(0 <= K:406) \/ mid_va:408 <= havoc:20)
                /\ (!(0 <= K:406) \/ -mid_va:408 <= (-havoc:20 + K:406))
                /\ ((K:406 = 0 /\ tmp:410 = mid_tmp:411 /\ 0 = mid_vb:409
                       /\ havoc:20 = mid_va:408 /\ 0 = mid___cost:407)
                      \/ (1 <= K:406 /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= (-1 + havoc:20)
                            /\ 0 <= (-mid_vb:409 + havoc:21)
                            /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:409
                            /\ 0 <= mid_va:408
                            /\ 0 <= (-1 + mid_va:408 + mid_vb:409)
                            /\ 0 <= (-1 + mid___cost:407))) /\ K:412 = 0
                /\ mid_tmp:411 = tmp':413 /\ mid_vb:409 = vb':414
                /\ mid_va:408 = va':415 /\ mid___cost:407 = __cost':416
                /\ 0 = K:412 /\ (K:406 + K:412) = K:417 /\ 0 <= K:417
                /\ 1 <= havoc:21 /\ 0 <= vb':414 /\ 0 < havoc:21
                /\ 0 < va':415 /\ havoc:419 = 0 /\ havoc:419 = phi_tmp:418))
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:427)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:427)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':446
 return := havoc:453
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:454
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:455
 param0@width := type_err:81
 param1@width := type_err:82
 when ((0 < param1:74
          /\ (!(0 <= K:436) \/ mid___cost:437 = (__cost:96 + K:436))
          /\ (!(0 <= K:436)
                \/ ((2 * mid_va:438) + mid_vb:439) <= ((2 * param0:71)
                                                         + -K:436))
          /\ (!(0 <= K:436) \/ mid_va:438 <= param0:71)
          /\ (!(0 <= K:436) \/ -mid_va:438 <= (-param0:71 + K:436))
          /\ ((K:436 = 0 /\ tmp:440 = mid_tmp:441 /\ 0 = mid_vb:439
                 /\ param0:71 = mid_va:438 /\ __cost:96 = mid___cost:437)
                \/ (1 <= K:436 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:439 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:439
                      /\ 0 <= mid_va:438
                      /\ 0 <= (-1 + mid_va:438 + mid_vb:439)
                      /\ 0 <= (-1 + mid___cost:437))) /\ K:442 = 0
          /\ mid_tmp:441 = tmp':443 /\ mid_vb:439 = vb':444
          /\ mid_va:438 = va':445 /\ mid___cost:437 = __cost':446
          /\ 0 = K:442 /\ (K:436 + K:442) = K:447 /\ 0 <= K:447
          /\ 1 <= param1:74 /\ 0 <= vb':444 /\ 0 < param1:74 /\ va':445 <= 0
          /\ tmp':443 = phi_tmp:448)
         \/ (0 < param1:74
               /\ (!(0 <= K:436) \/ mid___cost:437 = (__cost:96 + K:436))
               /\ (!(0 <= K:436)
                     \/ ((2 * mid_va:438) + mid_vb:439) <= ((2 * param0:71)
                                                              + -K:436))
               /\ (!(0 <= K:436) \/ mid_va:438 <= param0:71)
               /\ (!(0 <= K:436) \/ -mid_va:438 <= (-param0:71 + K:436))
               /\ ((K:436 = 0 /\ tmp:440 = mid_tmp:441 /\ 0 = mid_vb:439
                      /\ param0:71 = mid_va:438 /\ __cost:96 = mid___cost:437)
                     \/ (1 <= K:436 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:439 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:439
                           /\ 0 <= mid_va:438
                           /\ 0 <= (-1 + mid_va:438 + mid_vb:439)
                           /\ 0 <= (-1 + mid___cost:437))) /\ K:442 = 0
               /\ mid_tmp:441 = tmp':443 /\ mid_vb:439 = vb':444
               /\ mid_va:438 = va':445 /\ mid___cost:437 = __cost':446
               /\ 0 = K:442 /\ (K:436 + K:442) = K:447 /\ 0 <= K:447
               /\ 1 <= param1:74 /\ 0 <= vb':444 /\ 0 < param1:74
               /\ 0 < va':445 /\ havoc:449 = 0 /\ havoc:449 = phi_tmp:448))}

Evaluating variable number 24 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':378
 return := havoc:458
 return@pos := type_err:459
 return@width := type_err:460
 when ((0 < param1:74
          /\ (!(0 <= K:369) \/ mid___cost:370 = (__cost:96 + K:369))
          /\ (!(0 <= K:369)
                \/ ((2 * mid_va:371) + mid_vb:372) <= ((2 * param0:71)
                                                         + -K:369))
          /\ (!(0 <= K:369) \/ mid_va:371 <= param0:71)
          /\ (!(0 <= K:369) \/ -mid_va:371 <= (-param0:71 + K:369))
          /\ ((K:369 = 0 /\ tmp:461 = mid_tmp:373 /\ 0 = mid_vb:372
                 /\ param0:71 = mid_va:371 /\ __cost:96 = mid___cost:370)
                \/ (1 <= K:369 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:372 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:372
                      /\ 0 <= mid_va:371
                      /\ 0 <= (-1 + mid_va:371 + mid_vb:372)
                      /\ 0 <= (-1 + mid___cost:370))) /\ K:374 = 0
          /\ mid_tmp:373 = tmp':375 /\ mid_vb:372 = vb':376
          /\ mid_va:371 = va':377 /\ mid___cost:370 = __cost':378
          /\ 0 = K:374 /\ (K:369 + K:374) = K:379 /\ 0 <= K:379
          /\ 1 <= param1:74 /\ 0 <= vb':376 /\ 0 < param1:74 /\ va':377 <= 0
          /\ tmp':375 = phi_tmp:457)
         \/ (0 < param1:74
               /\ (!(0 <= K:369) \/ mid___cost:370 = (__cost:96 + K:369))
               /\ (!(0 <= K:369)
                     \/ ((2 * mid_va:371) + mid_vb:372) <= ((2 * param0:71)
                                                              + -K:369))
               /\ (!(0 <= K:369) \/ mid_va:371 <= param0:71)
               /\ (!(0 <= K:369) \/ -mid_va:371 <= (-param0:71 + K:369))
               /\ ((K:369 = 0 /\ tmp:461 = mid_tmp:373 /\ 0 = mid_vb:372
                      /\ param0:71 = mid_va:371 /\ __cost:96 = mid___cost:370)
                     \/ (1 <= K:369 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:372 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:372
                           /\ 0 <= mid_va:371
                           /\ 0 <= (-1 + mid_va:371 + mid_vb:372)
                           /\ 0 <= (-1 + mid___cost:370))) /\ K:374 = 0
               /\ mid_tmp:373 = tmp':375 /\ mid_vb:372 = vb':376
               /\ mid_va:371 = va':377 /\ mid___cost:370 = __cost':378
               /\ 0 = K:374 /\ (K:369 + K:374) = K:379 /\ 0 <= K:379
               /\ 1 <= param1:74 /\ 0 <= vb':376 /\ 0 < param1:74
               /\ 0 < va':377 /\ havoc:456 = 0 /\ havoc:456 = phi_tmp:457))}

Evaluating variable number 26 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

    (IRE-tc) Checking termination condition.
    (IRE-tc)   >> Inequivalent star body; continuing loop.
-------------------------------------------------------------------------------
Round 2:
Evaluating variable number 6 (using IRE) 
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:96 + 1)
 va := phi_va:463
 vb := phi_vb:464
 tmp := havoc:462
 when (1 <= m:93 /\ 0 <= vb:97 /\ 0 < m:93 /\ 0 < va:95 /\ !(havoc:462 = 0)
         /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((vb:97 < m:93 /\ (va:95 + -1) = phi_va:463
                /\ (vb:97 + 1) = phi_vb:464)
               \/ (m:93 <= vb:97 /\ va:95 = phi_va:463 /\ 0 = phi_vb:464)))}
**** alpha hat: 
  {<Split [true
            (__cost':348) = (1)*(__cost:96) + 1
           (((2 * va':349) + vb':350)) <= (1)*(((2 * va:95) + vb:97))
                                           + (-1)*1
           (va':349) <= (1)*(va:95) + 0
           (-va':349) <= (1)*(-va:95) + 1
           }
          pre:
            [|vb:97>=0; m:93-1>=0; va:95-1>=0; __cost:96>=0|]
          post:
            [|-vb':350+m:93>=0; m:93-1>=0; vb':350>=0; va':349>=0;
              va':349+vb':350-1>=0; __cost':348-1>=0|]
           }
  pre:
    bottom
  post:
    bottom]>}
**** star transition: 
  {__cost := __cost':348
   va := va':349
   vb := vb':350
   tmp := tmp':351
   when ((!(0 <= K:476) \/ mid___cost:481 = (__cost:96 + K:476))
           /\ (!(0 <= K:476)
                 \/ ((2 * mid_va:480) + mid_vb:479) <= (((2 * va:95) + vb:97)
                                                          + -K:476))
           /\ (!(0 <= K:476) \/ mid_va:480 <= va:95)
           /\ (!(0 <= K:476) \/ -mid_va:480 <= (-va:95 + K:476))
           /\ ((K:476 = 0 /\ tmp:94 = mid_tmp:478 /\ vb:97 = mid_vb:479
                  /\ va:95 = mid_va:480 /\ __cost:96 = mid___cost:481)
                 \/ (1 <= K:476 /\ 0 <= vb:97 /\ 0 <= (-1 + m:93)
                       /\ 0 <= (-1 + va:95) /\ 0 <= __cost:96
                       /\ 0 <= (-mid_vb:479 + m:93) /\ 0 <= (-1 + m:93)
                       /\ 0 <= mid_vb:479 /\ 0 <= mid_va:480
                       /\ 0 <= (-1 + mid_va:480 + mid_vb:479)
                       /\ 0 <= (-1 + mid___cost:481))) /\ K:477 = 0
           /\ mid_tmp:478 = tmp':351 /\ mid_vb:479 = vb':350
           /\ mid_va:480 = va':349 /\ mid___cost:481 = __cost':348
           /\ 0 = K:477 /\ (K:476 + K:477) = K:475 /\ 0 <= K:475)}
}

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':529
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:541
 param0@pos := type_err:535
 param1@pos := type_err:536
 return@width := type_err:542
 param0@width := type_err:538
 param1@width := type_err:539
 when (((0 < havoc:21 /\ (!(0 <= K:519) \/ mid___cost:520 = K:519)
           /\ (!(0 <= K:519)
                 \/ ((2 * mid_va:521) + mid_vb:522) <= ((2 * havoc:20)
                                                          + -K:519))
           /\ (!(0 <= K:519) \/ mid_va:521 <= havoc:20)
           /\ (!(0 <= K:519) \/ -mid_va:521 <= (-havoc:20 + K:519))
           /\ ((K:519 = 0 /\ tmp:523 = mid_tmp:524 /\ 0 = mid_vb:522
                  /\ havoc:20 = mid_va:521 /\ 0 = mid___cost:520)
                 \/ (1 <= K:519 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + havoc:20)
                       /\ 0 <= (-mid_vb:522 + havoc:21)
                       /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:522
                       /\ 0 <= mid_va:521
                       /\ 0 <= (-1 + mid_va:521 + mid_vb:522)
                       /\ 0 <= (-1 + mid___cost:520))) /\ K:525 = 0
           /\ mid_tmp:524 = tmp':526 /\ mid_vb:522 = vb':527
           /\ mid_va:521 = va':528 /\ mid___cost:520 = __cost':529
           /\ 0 = K:525 /\ (K:519 + K:525) = K:530 /\ 0 <= K:530
           /\ 1 <= havoc:21 /\ 0 <= vb':527 /\ 0 < havoc:21 /\ va':528 <= 0
           /\ tmp':526 = phi_tmp:531)
          \/ (0 < havoc:21 /\ (!(0 <= K:519) \/ mid___cost:520 = K:519)
                /\ (!(0 <= K:519)
                      \/ ((2 * mid_va:521) + mid_vb:522) <= ((2 * havoc:20)
                                                               + -K:519))
                /\ (!(0 <= K:519) \/ mid_va:521 <= havoc:20)
                /\ (!(0 <= K:519) \/ -mid_va:521 <= (-havoc:20 + K:519))
                /\ ((K:519 = 0 /\ tmp:523 = mid_tmp:524 /\ 0 = mid_vb:522
                       /\ havoc:20 = mid_va:521 /\ 0 = mid___cost:520)
                      \/ (1 <= K:519 /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= (-1 + havoc:20)
                            /\ 0 <= (-mid_vb:522 + havoc:21)
                            /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:522
                            /\ 0 <= mid_va:521
                            /\ 0 <= (-1 + mid_va:521 + mid_vb:522)
                            /\ 0 <= (-1 + mid___cost:520))) /\ K:525 = 0
                /\ mid_tmp:524 = tmp':526 /\ mid_vb:522 = vb':527
                /\ mid_va:521 = va':528 /\ mid___cost:520 = __cost':529
                /\ 0 = K:525 /\ (K:519 + K:525) = K:530 /\ 0 <= K:530
                /\ 1 <= havoc:21 /\ 0 <= vb':527 /\ 0 < havoc:21
                /\ 0 < va':528 /\ havoc:532 = 0 /\ havoc:532 = phi_tmp:531))
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:540)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:540)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':559
 return := havoc:566
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:567
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:568
 param0@width := type_err:81
 param1@width := type_err:82
 when ((0 < param1:74
          /\ (!(0 <= K:549) \/ mid___cost:550 = (__cost:96 + K:549))
          /\ (!(0 <= K:549)
                \/ ((2 * mid_va:551) + mid_vb:552) <= ((2 * param0:71)
                                                         + -K:549))
          /\ (!(0 <= K:549) \/ mid_va:551 <= param0:71)
          /\ (!(0 <= K:549) \/ -mid_va:551 <= (-param0:71 + K:549))
          /\ ((K:549 = 0 /\ tmp:553 = mid_tmp:554 /\ 0 = mid_vb:552
                 /\ param0:71 = mid_va:551 /\ __cost:96 = mid___cost:550)
                \/ (1 <= K:549 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:552 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:552
                      /\ 0 <= mid_va:551
                      /\ 0 <= (-1 + mid_va:551 + mid_vb:552)
                      /\ 0 <= (-1 + mid___cost:550))) /\ K:555 = 0
          /\ mid_tmp:554 = tmp':556 /\ mid_vb:552 = vb':557
          /\ mid_va:551 = va':558 /\ mid___cost:550 = __cost':559
          /\ 0 = K:555 /\ (K:549 + K:555) = K:560 /\ 0 <= K:560
          /\ 1 <= param1:74 /\ 0 <= vb':557 /\ 0 < param1:74 /\ va':558 <= 0
          /\ tmp':556 = phi_tmp:561)
         \/ (0 < param1:74
               /\ (!(0 <= K:549) \/ mid___cost:550 = (__cost:96 + K:549))
               /\ (!(0 <= K:549)
                     \/ ((2 * mid_va:551) + mid_vb:552) <= ((2 * param0:71)
                                                              + -K:549))
               /\ (!(0 <= K:549) \/ mid_va:551 <= param0:71)
               /\ (!(0 <= K:549) \/ -mid_va:551 <= (-param0:71 + K:549))
               /\ ((K:549 = 0 /\ tmp:553 = mid_tmp:554 /\ 0 = mid_vb:552
                      /\ param0:71 = mid_va:551 /\ __cost:96 = mid___cost:550)
                     \/ (1 <= K:549 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:552 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:552
                           /\ 0 <= mid_va:551
                           /\ 0 <= (-1 + mid_va:551 + mid_vb:552)
                           /\ 0 <= (-1 + mid___cost:550))) /\ K:555 = 0
               /\ mid_tmp:554 = tmp':556 /\ mid_vb:552 = vb':557
               /\ mid_va:551 = va':558 /\ mid___cost:550 = __cost':559
               /\ 0 = K:555 /\ (K:549 + K:555) = K:560 /\ 0 <= K:560
               /\ 1 <= param1:74 /\ 0 <= vb':557 /\ 0 < param1:74
               /\ 0 < va':558 /\ havoc:562 = 0 /\ havoc:562 = phi_tmp:561))}

Evaluating variable number 24 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':491
 return := havoc:571
 return@pos := type_err:572
 return@width := type_err:573
 when ((0 < param1:74
          /\ (!(0 <= K:482) \/ mid___cost:483 = (__cost:96 + K:482))
          /\ (!(0 <= K:482)
                \/ ((2 * mid_va:484) + mid_vb:485) <= ((2 * param0:71)
                                                         + -K:482))
          /\ (!(0 <= K:482) \/ mid_va:484 <= param0:71)
          /\ (!(0 <= K:482) \/ -mid_va:484 <= (-param0:71 + K:482))
          /\ ((K:482 = 0 /\ tmp:574 = mid_tmp:486 /\ 0 = mid_vb:485
                 /\ param0:71 = mid_va:484 /\ __cost:96 = mid___cost:483)
                \/ (1 <= K:482 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:485 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:485
                      /\ 0 <= mid_va:484
                      /\ 0 <= (-1 + mid_va:484 + mid_vb:485)
                      /\ 0 <= (-1 + mid___cost:483))) /\ K:487 = 0
          /\ mid_tmp:486 = tmp':488 /\ mid_vb:485 = vb':489
          /\ mid_va:484 = va':490 /\ mid___cost:483 = __cost':491
          /\ 0 = K:487 /\ (K:482 + K:487) = K:492 /\ 0 <= K:492
          /\ 1 <= param1:74 /\ 0 <= vb':489 /\ 0 < param1:74 /\ va':490 <= 0
          /\ tmp':488 = phi_tmp:570)
         \/ (0 < param1:74
               /\ (!(0 <= K:482) \/ mid___cost:483 = (__cost:96 + K:482))
               /\ (!(0 <= K:482)
                     \/ ((2 * mid_va:484) + mid_vb:485) <= ((2 * param0:71)
                                                              + -K:482))
               /\ (!(0 <= K:482) \/ mid_va:484 <= param0:71)
               /\ (!(0 <= K:482) \/ -mid_va:484 <= (-param0:71 + K:482))
               /\ ((K:482 = 0 /\ tmp:574 = mid_tmp:486 /\ 0 = mid_vb:485
                      /\ param0:71 = mid_va:484 /\ __cost:96 = mid___cost:483)
                     \/ (1 <= K:482 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:485 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:485
                           /\ 0 <= mid_va:484
                           /\ 0 <= (-1 + mid_va:484 + mid_vb:485)
                           /\ 0 <= (-1 + mid___cost:483))) /\ K:487 = 0
               /\ mid_tmp:486 = tmp':488 /\ mid_vb:485 = vb':489
               /\ mid_va:484 = va':490 /\ mid___cost:483 = __cost':491
               /\ 0 = K:487 /\ (K:482 + K:487) = K:492 /\ 0 <= K:492
               /\ 1 <= param1:74 /\ 0 <= vb':489 /\ 0 < param1:74
               /\ 0 < va':490 /\ havoc:569 = 0 /\ havoc:569 = phi_tmp:570))}

Evaluating variable number 26 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{}

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

NumRnds: 3

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,60)_g1> -> <__pstate, (Unique State Name,75)_g1>	Base relation: 
{__cost := __cost':491
 va := va':490
 vb := vb':489
 tmp := tmp':488
 m := param1:74
 when (0 < param1:74
         /\ (!(0 <= K:482) \/ mid___cost:483 = (__cost:96 + K:482))
         /\ (!(0 <= K:482)
               \/ ((2 * mid_va:484) + mid_vb:485) <= ((2 * param0:71)
                                                        + -K:482))
         /\ (!(0 <= K:482) \/ mid_va:484 <= param0:71)
         /\ (!(0 <= K:482) \/ -mid_va:484 <= (-param0:71 + K:482))
         /\ ((K:482 = 0 /\ tmp:94 = mid_tmp:486 /\ 0 = mid_vb:485
                /\ param0:71 = mid_va:484 /\ __cost:96 = mid___cost:483)
               \/ (1 <= K:482 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                     /\ 0 <= (-mid_vb:485 + param1:74)
                     /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:485
                     /\ 0 <= mid_va:484
                     /\ 0 <= (-1 + mid_va:484 + mid_vb:485)
                     /\ 0 <= (-1 + mid___cost:483))) /\ K:487 = 0
         /\ mid_tmp:486 = tmp':488 /\ mid_vb:485 = vb':489
         /\ mid_va:484 = va':490 /\ mid___cost:483 = __cost':491 /\ 0 = K:487
         /\ (K:482 + K:487) = K:492 /\ 0 <= K:492 /\ 1 <= param1:74
         /\ 0 <= vb':489 /\ 0 < param1:74 /\ 0 < va':490)}	
<__pstate, accept> -> <__pstate, (Unique State Name,66)_g1>	Base relation: 
{__cost := 0
 n := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}	
<__pstate, (Unique State Name,66)_g1> -> <__pstate, (Unique State Name,60)_g1>	Base relation: 
{param0 := param0:71
 param1 := param1:74
 param0@pos := type_err:79
 param1@pos := type_err:80
 param0@width := type_err:81
 param1@width := type_err:82}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__pstate 0x8a82290: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{when false}
__done 0x8a82370: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
##### ANS
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}
    ( __pstate , (Unique State Name,75)_g1 , __done )	Base relation: 
{__cost := __cost':638
 n := havoc:20
 va := va':637
 vb := vb':636
 tmp := tmp':635
 m := havoc:21
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:625
 param1@pos := type_err:626
 param0@width := type_err:627
 param1@width := type_err:628
 when (0 < havoc:21 /\ (!(0 <= K:629) \/ mid___cost:630 = K:629)
         /\ (!(0 <= K:629)
               \/ ((2 * mid_va:631) + mid_vb:632) <= ((2 * havoc:20) + -K:629))
         /\ (!(0 <= K:629) \/ mid_va:631 <= havoc:20)
         /\ (!(0 <= K:629) \/ -mid_va:631 <= (-havoc:20 + K:629))
         /\ ((K:629 = 0 /\ tmp:94 = mid_tmp:633 /\ 0 = mid_vb:632
                /\ havoc:20 = mid_va:631 /\ 0 = mid___cost:630)
               \/ (1 <= K:629 /\ 0 <= (-1 + havoc:21) /\ 0 <= (-1 + havoc:20)
                     /\ 0 <= (-mid_vb:632 + havoc:21) /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= mid_vb:632 /\ 0 <= mid_va:631
                     /\ 0 <= (-1 + mid_va:631 + mid_vb:632)
                     /\ 0 <= (-1 + mid___cost:630))) /\ K:634 = 0
         /\ mid_tmp:633 = tmp':635 /\ mid_vb:632 = vb':636
         /\ mid_va:631 = va':637 /\ mid___cost:630 = __cost':638 /\ 0 = K:634
         /\ (K:629 + K:634) = K:639 /\ 0 <= K:639 /\ 1 <= havoc:21
         /\ 0 <= vb':636 /\ 0 < havoc:21 /\ 0 < va':637)}
    ( __pstate , (Unique State Name,66)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:25
 param1@pos := type_err:27
 param0@width := type_err:26
 param1@width := type_err:28}
    ( __pstate , (Unique State Name,60)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:640
 param1@pos := type_err:641
 param0@width := type_err:642
 param1@width := type_err:643}

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

------------------------------------------------
Procedure summary for __VERIFIER_nondet

Base relation: 
{}

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

Base relation: 
{__cost := __cost':585
 n := havoc:20
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:597
 param0@pos := type_err:591
 param1@pos := type_err:592
 return@width := type_err:598
 param0@width := type_err:594
 param1@width := type_err:595
 when (((0 < havoc:21 /\ (!(0 <= K:575) \/ mid___cost:576 = K:575)
           /\ (!(0 <= K:575)
                 \/ ((2 * mid_va:577) + mid_vb:578) <= ((2 * havoc:20)
                                                          + -K:575))
           /\ (!(0 <= K:575) \/ mid_va:577 <= havoc:20)
           /\ (!(0 <= K:575) \/ -mid_va:577 <= (-havoc:20 + K:575))
           /\ ((K:575 = 0 /\ tmp:579 = mid_tmp:580 /\ 0 = mid_vb:578
                  /\ havoc:20 = mid_va:577 /\ 0 = mid___cost:576)
                 \/ (1 <= K:575 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (-1 + havoc:20)
                       /\ 0 <= (-mid_vb:578 + havoc:21)
                       /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:578
                       /\ 0 <= mid_va:577
                       /\ 0 <= (-1 + mid_va:577 + mid_vb:578)
                       /\ 0 <= (-1 + mid___cost:576))) /\ K:581 = 0
           /\ mid_tmp:580 = tmp':582 /\ mid_vb:578 = vb':583
           /\ mid_va:577 = va':584 /\ mid___cost:576 = __cost':585
           /\ 0 = K:581 /\ (K:575 + K:581) = K:586 /\ 0 <= K:586
           /\ 1 <= havoc:21 /\ 0 <= vb':583 /\ 0 < havoc:21 /\ va':584 <= 0
           /\ tmp':582 = phi_tmp:587)
          \/ (0 < havoc:21 /\ (!(0 <= K:575) \/ mid___cost:576 = K:575)
                /\ (!(0 <= K:575)
                      \/ ((2 * mid_va:577) + mid_vb:578) <= ((2 * havoc:20)
                                                               + -K:575))
                /\ (!(0 <= K:575) \/ mid_va:577 <= havoc:20)
                /\ (!(0 <= K:575) \/ -mid_va:577 <= (-havoc:20 + K:575))
                /\ ((K:575 = 0 /\ tmp:579 = mid_tmp:580 /\ 0 = mid_vb:578
                       /\ havoc:20 = mid_va:577 /\ 0 = mid___cost:576)
                      \/ (1 <= K:575 /\ 0 <= (-1 + havoc:21)
                            /\ 0 <= (-1 + havoc:20)
                            /\ 0 <= (-mid_vb:578 + havoc:21)
                            /\ 0 <= (-1 + havoc:21) /\ 0 <= mid_vb:578
                            /\ 0 <= mid_va:577
                            /\ 0 <= (-1 + mid_va:577 + mid_vb:578)
                            /\ 0 <= (-1 + mid___cost:576))) /\ K:581 = 0
                /\ mid_tmp:580 = tmp':582 /\ mid_vb:578 = vb':583
                /\ mid_va:577 = va':584 /\ mid___cost:576 = __cost':585
                /\ 0 = K:581 /\ (K:575 + K:581) = K:586 /\ 0 <= K:586
                /\ 1 <= havoc:21 /\ 0 <= vb':583 /\ 0 < havoc:21
                /\ 0 < va':584 /\ havoc:588 = 0 /\ havoc:588 = phi_tmp:587))
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:596)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:596)))}

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

Base relation: 
{__cost := __cost':609
 return := havoc:616
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:617
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:618
 param0@width := type_err:81
 param1@width := type_err:82
 when ((0 < param1:74
          /\ (!(0 <= K:599) \/ mid___cost:600 = (__cost:96 + K:599))
          /\ (!(0 <= K:599)
                \/ ((2 * mid_va:601) + mid_vb:602) <= ((2 * param0:71)
                                                         + -K:599))
          /\ (!(0 <= K:599) \/ mid_va:601 <= param0:71)
          /\ (!(0 <= K:599) \/ -mid_va:601 <= (-param0:71 + K:599))
          /\ ((K:599 = 0 /\ tmp:603 = mid_tmp:604 /\ 0 = mid_vb:602
                 /\ param0:71 = mid_va:601 /\ __cost:96 = mid___cost:600)
                \/ (1 <= K:599 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:602 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:602
                      /\ 0 <= mid_va:601
                      /\ 0 <= (-1 + mid_va:601 + mid_vb:602)
                      /\ 0 <= (-1 + mid___cost:600))) /\ K:605 = 0
          /\ mid_tmp:604 = tmp':606 /\ mid_vb:602 = vb':607
          /\ mid_va:601 = va':608 /\ mid___cost:600 = __cost':609
          /\ 0 = K:605 /\ (K:599 + K:605) = K:610 /\ 0 <= K:610
          /\ 1 <= param1:74 /\ 0 <= vb':607 /\ 0 < param1:74 /\ va':608 <= 0
          /\ tmp':606 = phi_tmp:611)
         \/ (0 < param1:74
               /\ (!(0 <= K:599) \/ mid___cost:600 = (__cost:96 + K:599))
               /\ (!(0 <= K:599)
                     \/ ((2 * mid_va:601) + mid_vb:602) <= ((2 * param0:71)
                                                              + -K:599))
               /\ (!(0 <= K:599) \/ mid_va:601 <= param0:71)
               /\ (!(0 <= K:599) \/ -mid_va:601 <= (-param0:71 + K:599))
               /\ ((K:599 = 0 /\ tmp:603 = mid_tmp:604 /\ 0 = mid_vb:602
                      /\ param0:71 = mid_va:601 /\ __cost:96 = mid___cost:600)
                     \/ (1 <= K:599 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:602 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:602
                           /\ 0 <= mid_va:601
                           /\ 0 <= (-1 + mid_va:601 + mid_vb:602)
                           /\ 0 <= (-1 + mid___cost:600))) /\ K:605 = 0
               /\ mid_tmp:604 = tmp':606 /\ mid_vb:602 = vb':607
               /\ mid_va:601 = va':608 /\ mid___cost:600 = __cost':609
               /\ 0 = K:605 /\ (K:599 + K:605) = K:610 /\ 0 <= K:610
               /\ 1 <= param1:74 /\ 0 <= vb':607 /\ 0 < param1:74
               /\ 0 < va':608 /\ havoc:612 = 0 /\ havoc:612 = phi_tmp:611))}

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

Base relation: 
{__cost := __cost':491
 va := va':490
 vb := vb':489
 tmp := phi_tmp:621
 m := param1:74
 return := havoc:622
 return@pos := type_err:623
 return@width := type_err:624
 when ((0 < param1:74
          /\ (!(0 <= K:482) \/ mid___cost:483 = (__cost:96 + K:482))
          /\ (!(0 <= K:482)
                \/ ((2 * mid_va:484) + mid_vb:485) <= ((2 * param0:71)
                                                         + -K:482))
          /\ (!(0 <= K:482) \/ mid_va:484 <= param0:71)
          /\ (!(0 <= K:482) \/ -mid_va:484 <= (-param0:71 + K:482))
          /\ ((K:482 = 0 /\ tmp:94 = mid_tmp:486 /\ 0 = mid_vb:485
                 /\ param0:71 = mid_va:484 /\ __cost:96 = mid___cost:483)
                \/ (1 <= K:482 /\ 0 <= (-1 + param1:74)
                      /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                      /\ 0 <= (-mid_vb:485 + param1:74)
                      /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:485
                      /\ 0 <= mid_va:484
                      /\ 0 <= (-1 + mid_va:484 + mid_vb:485)
                      /\ 0 <= (-1 + mid___cost:483))) /\ K:487 = 0
          /\ mid_tmp:486 = tmp':488 /\ mid_vb:485 = vb':489
          /\ mid_va:484 = va':490 /\ mid___cost:483 = __cost':491
          /\ 0 = K:487 /\ (K:482 + K:487) = K:492 /\ 0 <= K:492
          /\ 1 <= param1:74 /\ 0 <= vb':489 /\ 0 < param1:74 /\ va':490 <= 0
          /\ tmp':488 = phi_tmp:621)
         \/ (0 < param1:74
               /\ (!(0 <= K:482) \/ mid___cost:483 = (__cost:96 + K:482))
               /\ (!(0 <= K:482)
                     \/ ((2 * mid_va:484) + mid_vb:485) <= ((2 * param0:71)
                                                              + -K:482))
               /\ (!(0 <= K:482) \/ mid_va:484 <= param0:71)
               /\ (!(0 <= K:482) \/ -mid_va:484 <= (-param0:71 + K:482))
               /\ ((K:482 = 0 /\ tmp:94 = mid_tmp:486 /\ 0 = mid_vb:485
                      /\ param0:71 = mid_va:484 /\ __cost:96 = mid___cost:483)
                     \/ (1 <= K:482 /\ 0 <= (-1 + param1:74)
                           /\ 0 <= (-1 + param0:71) /\ 0 <= __cost:96
                           /\ 0 <= (-mid_vb:485 + param1:74)
                           /\ 0 <= (-1 + param1:74) /\ 0 <= mid_vb:485
                           /\ 0 <= mid_va:484
                           /\ 0 <= (-1 + mid_va:484 + mid_vb:485)
                           /\ 0 <= (-1 + mid___cost:483))) /\ K:487 = 0
               /\ mid_tmp:486 = tmp':488 /\ mid_vb:485 = vb':489
               /\ mid_va:484 = va':490 /\ mid___cost:483 = __cost':491
               /\ 0 = K:487 /\ (K:482 + K:487) = K:492 /\ 0 <= K:492
               /\ 1 <= param1:74 /\ 0 <= vb':489 /\ 0 < param1:74
               /\ 0 < va':490 /\ havoc:620 = 0 /\ havoc:620 = phi_tmp:621))}

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

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

Variable bounds at line 28 in run

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

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