/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, 70> -> <Unique State Name, 65 69>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 17> -> <Unique State Name, 70>	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, 73> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 59> -> <Unique State Name, 36>	Base relation: 
{i := param0:71
 m := param1:74
 when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
          \/ (0 < param1:74
                /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                      \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0))}	
<Unique State Name, 36> -> <Unique State Name, 74>	Base relation: 
{when (1 <= m:93 /\ 0 <= i:95 /\ 0 < m:93)}	
<Unique State Name, 63> -> <Unique State Name, 19>	Base relation: 
{}	
<Unique State Name, 71> -> <Unique State Name, >	Base relation: 
{}	
<Unique State Name, 64> -> <Unique State Name, 59 63>	Base relation: 
{}	MergeFn[Base relation: 
{}]
<Unique State Name, 74> -> <Unique State Name, 40>	Base relation: 
{}	
<Unique State Name, 19> -> <Unique State Name, 72>	Base relation: 
{return := havoc:54
 return@pos := type_err:57
 return@width := type_err:58}	
<Unique State Name, 65> -> <Unique State Name, 64>	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, 69> -> <Unique State Name, 73>	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, 40> -> <Unique State Name, 36>	Base relation: 
{__cost := (__cost:96 + 1)
 i := phi_i:111
 when (0 < i:95 /\ 0 <= __cost:96 /\ 0 <= (__cost:96 + 1)
         /\ ((i:95 < m:93 /\ (i:95 + -1) = phi_i:111)
               \/ (m:93 <= i:95 /\ (i:95 + -m:93) = phi_i:111)))}	
<Unique State Name, 40> -> <Unique State Name, 71>	Base relation: 
{return := havoc:104
 return@pos := type_err:105
 return@width := type_err:106
 when i:95 <= 0}	
<Unique State Name, 72> -> <Unique State Name, >	Base relation: 
{}	
#################################################################
           Beginning Interprocedural Anaylsis (with regexp=IRE)  
Step 1: =========================================================
Step 2: =========================================================
Step 3: =========================================================
        Converting to IRE regular expressions
(Not performing widening.)
alphaHatStar {
**** body value: Base relation: 
{__cost := (__cost:96 + 1)
 i := phi_i:189
 when (1 <= m:93 /\ 0 <= i:95 /\ 0 < m:93 /\ 0 < i:95 /\ 0 <= __cost:96
         /\ 0 <= (__cost:96 + 1)
         /\ ((i:95 < m:93 /\ (i:95 + -1) = phi_i:189)
               \/ (m:93 <= i:95 /\ (i:95 + -m:93) = phi_i:189)))}
**** alpha hat: 
  {<Split [(m:93 + -i:95) <= 0
            (i':191) = (1)*(i:95) + (-1)*m:93
           (__cost':190) = (1)*(__cost:96) + 1
           (i':191) <= (1)*(i:95) + (-1)*1
           (-i':191) <= (1)*(-i:95) + i:95
           }
          pre:
            [|__cost:96>=0; m:93-1>=0; i:95-m:93>=0|]
          post:
            [|__cost':190-1>=0; i':191>=0; m:93-1>=0|]
           (i':191) = (1)*(i:95) + (-1)*1
          (__cost':190) = (1)*(__cost:96) + 1
          }
  pre:
    [|-i:95+m:93-1>=0; __cost:96>=0; i:95-1>=0|]
  post:
    [|i':191>=0; __cost':190-1>=0; m:93-i':191-2>=0|]],
[!((-m:93 + i:95) < 0)
  (i':191) = (1)*(i:95) + (-1)*m:93
 (__cost':190) = (1)*(__cost:96) + 1
 (i':191) <= (1)*(i:95) + (-1)*1
 (-i':191) <= (1)*(-i:95) + i:95
 } pre:   [|__cost:96>=0; m:93-1>=0; i:95-m:93>=0|] post:
  [|__cost':190-1>=0; i':191>=0; m:93-1>=0|]  (i':191) = (1)*(i:95) + (-1)*1
(__cost':190) = (1)*(__cost:96) + 1 } pre:
  [|-i:95+m:93-1>=0; __cost:96>=0; i:95-1>=0|] post:
  [|i':191>=0; __cost':190-1>=0; m:93-i':191-2>=0|]]>}
**** star transition: 
  {__cost := __cost':190
   i := i':191
   when ((!(0 <= K:213) \/ mid_i:215 = (i:95 + -((m:93 * K:213))))
           /\ (!(0 <= K:213) \/ mid___cost:216 = (__cost:96 + K:213))
           /\ (!(0 <= K:213) \/ mid_i:215 <= (i:95 + -K:213))
           /\ (!(0 <= K:213)
                 \/ -mid_i:215 <= (-i:95 + (1/2 * m:93 * K:213)
                                     + (i:95 * K:213)
                                     + (-1/2 * m:93 * (K:213 * K:213))))
           /\ ((K:213 = 0 /\ i:95 = mid_i:215 /\ __cost:96 = mid___cost:216)
                 \/ (1 <= K:213 /\ 0 <= __cost:96 /\ 0 <= (-1 + m:93)
                       /\ 0 <= (i:95 + -m:93) /\ 0 <= (-1 + mid___cost:216)
                       /\ 0 <= mid_i:215 /\ 0 <= (-1 + m:93)))
           /\ (0 = K:213 \/ (m:93 + -i:95) <= 0)
           /\ (!(0 <= K:214) \/ i':191 = (mid_i:215 + -K:214))
           /\ (!(0 <= K:214) \/ __cost':190 = (mid___cost:216 + K:214))
           /\ ((K:214 = 0 /\ mid_i:215 = i':191
                  /\ mid___cost:216 = __cost':190)
                 \/ (1 <= K:214 /\ 0 <= (-1 + -mid_i:215 + m:93)
                       /\ 0 <= mid___cost:216 /\ 0 <= (-1 + mid_i:215)
                       /\ 0 <= i':191 /\ 0 <= (-1 + __cost':190)
                       /\ 0 <= (-2 + m:93 + -i':191)))
           /\ (0 = K:214 \/ !((m:93 + -mid_i:215) <= 0))
           /\ (K:213 + K:214) = K:212
           /\ (!(0 <= K:217) \/ mid_i:219 = (i:95 + -((m:93 * K:217))))
           /\ (!(0 <= K:217) \/ mid___cost:220 = (__cost:96 + K:217))
           /\ (!(0 <= K:217) \/ mid_i:219 <= (i:95 + -K:217))
           /\ (!(0 <= K:217)
                 \/ -mid_i:219 <= (-i:95 + (1/2 * m:93 * K:217)
                                     + (i:95 * K:217)
                                     + (-1/2 * m:93 * (K:217 * K:217))))
           /\ ((K:217 = 0 /\ i:95 = mid_i:219 /\ __cost:96 = mid___cost:220)
                 \/ (1 <= K:217 /\ 0 <= __cost:96 /\ 0 <= (-1 + m:93)
                       /\ 0 <= (i:95 + -m:93) /\ 0 <= (-1 + mid___cost:220)
                       /\ 0 <= mid_i:219 /\ 0 <= (-1 + m:93)))
           /\ (0 = K:217 \/ !((-m:93 + i:95) < 0))
           /\ (!(0 <= K:218) \/ i':191 = (mid_i:219 + -K:218))
           /\ (!(0 <= K:218) \/ __cost':190 = (mid___cost:220 + K:218))
           /\ ((K:218 = 0 /\ mid_i:219 = i':191
                  /\ mid___cost:220 = __cost':190)
                 \/ (1 <= K:218 /\ 0 <= (-1 + -mid_i:219 + m:93)
                       /\ 0 <= mid___cost:220 /\ 0 <= (-1 + mid_i:219)
                       /\ 0 <= i':191 /\ 0 <= (-1 + __cost':190)
                       /\ 0 <= (-2 + m:93 + -i':191)))
           /\ (0 = K:218 \/ (-m:93 + mid_i:219) < 0)
           /\ (K:217 + K:218) = K:212 /\ 0 <= K:212)}
}
Step 4: =========================================================
The procedure (i.e., variable) numbers are: 
6  13  19  


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(19)
  )
  ,
  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=19: 
Weight(Base relation: 
  {__cost := __cost':226
   i := i':225
   m := param1:74
   return := havoc:232
   return@pos := type_err:233
   return@width := type_err:234
   when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
            \/ (0 < param1:74
                  /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                        \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                  /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0)
           /\ (!(0 <= K:221)
                 \/ mid_i:222 = (param0:71 + -((param1:74 * K:221))))
           /\ (!(0 <= K:221) \/ mid___cost:223 = (__cost:96 + K:221))
           /\ (!(0 <= K:221) \/ mid_i:222 <= (param0:71 + -K:221))
           /\ (!(0 <= K:221)
                 \/ -mid_i:222 <= (-param0:71 + (1/2 * param1:74 * K:221)
                                     + (param0:71 * K:221)
                                     + (-1/2 * param1:74 * (K:221 * K:221))))
           /\ ((K:221 = 0 /\ param0:71 = mid_i:222
                  /\ __cost:96 = mid___cost:223)
                 \/ (1 <= K:221 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:223) /\ 0 <= mid_i:222
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:221 \/ (param1:74 + -param0:71) <= 0)
           /\ (!(0 <= K:224) \/ i':225 = (mid_i:222 + -K:224))
           /\ (!(0 <= K:224) \/ __cost':226 = (mid___cost:223 + K:224))
           /\ ((K:224 = 0 /\ mid_i:222 = i':225
                  /\ mid___cost:223 = __cost':226)
                 \/ (1 <= K:224 /\ 0 <= (-1 + -mid_i:222 + param1:74)
                       /\ 0 <= mid___cost:223 /\ 0 <= (-1 + mid_i:222)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:224 \/ !((param1:74 + -mid_i:222) <= 0))
           /\ (K:221 + K:224) = K:227
           /\ (!(0 <= K:228)
                 \/ mid_i:229 = (param0:71 + -((param1:74 * K:228))))
           /\ (!(0 <= K:228) \/ mid___cost:230 = (__cost:96 + K:228))
           /\ (!(0 <= K:228) \/ mid_i:229 <= (param0:71 + -K:228))
           /\ (!(0 <= K:228)
                 \/ -mid_i:229 <= (-param0:71 + (1/2 * param1:74 * K:228)
                                     + (param0:71 * K:228)
                                     + (-1/2 * param1:74 * (K:228 * K:228))))
           /\ ((K:228 = 0 /\ param0:71 = mid_i:229
                  /\ __cost:96 = mid___cost:230)
                 \/ (1 <= K:228 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:230) /\ 0 <= mid_i:229
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:228 \/ !((-param1:74 + param0:71) < 0))
           /\ (!(0 <= K:231) \/ i':225 = (mid_i:229 + -K:231))
           /\ (!(0 <= K:231) \/ __cost':226 = (mid___cost:230 + K:231))
           /\ ((K:231 = 0 /\ mid_i:229 = i':225
                  /\ mid___cost:230 = __cost':226)
                 \/ (1 <= K:231 /\ 0 <= (-1 + -mid_i:229 + param1:74)
                       /\ 0 <= mid___cost:230 /\ 0 <= (-1 + mid_i:229)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:231 \/ (-param1:74 + mid_i:229) < 0)
           /\ (K:228 + K:231) = K:227 /\ 0 <= K:227 /\ 1 <= param1:74
           /\ 0 <= i':225 /\ 0 < param1:74 /\ i':225 <= 0)})



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(19)
    )
    ,
    Weight(Base relation: 
      {return := havoc:54
       return@pos := type_err:57
       return@width := type_err:58}    )
  )
)



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

Weight(Base relation: 
  {__cost := __cost':226
   return := havoc:232
   return@pos := type_err:233
   return@width := type_err:234
   when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
            \/ (0 < param1:74
                  /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                        \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                  /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0)
           /\ (!(0 <= K:221)
                 \/ mid_i:222 = (param0:71 + -((param1:74 * K:221))))
           /\ (!(0 <= K:221) \/ mid___cost:223 = (__cost:96 + K:221))
           /\ (!(0 <= K:221) \/ mid_i:222 <= (param0:71 + -K:221))
           /\ (!(0 <= K:221)
                 \/ -mid_i:222 <= (-param0:71 + (1/2 * param1:74 * K:221)
                                     + (param0:71 * K:221)
                                     + (-1/2 * param1:74 * (K:221 * K:221))))
           /\ ((K:221 = 0 /\ param0:71 = mid_i:222
                  /\ __cost:96 = mid___cost:223)
                 \/ (1 <= K:221 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:223) /\ 0 <= mid_i:222
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:221 \/ (param1:74 + -param0:71) <= 0)
           /\ (!(0 <= K:224) \/ i':225 = (mid_i:222 + -K:224))
           /\ (!(0 <= K:224) \/ __cost':226 = (mid___cost:223 + K:224))
           /\ ((K:224 = 0 /\ mid_i:222 = i':225
                  /\ mid___cost:223 = __cost':226)
                 \/ (1 <= K:224 /\ 0 <= (-1 + -mid_i:222 + param1:74)
                       /\ 0 <= mid___cost:223 /\ 0 <= (-1 + mid_i:222)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:224 \/ !((param1:74 + -mid_i:222) <= 0))
           /\ (K:221 + K:224) = K:227
           /\ (!(0 <= K:228)
                 \/ mid_i:229 = (param0:71 + -((param1:74 * K:228))))
           /\ (!(0 <= K:228) \/ mid___cost:230 = (__cost:96 + K:228))
           /\ (!(0 <= K:228) \/ mid_i:229 <= (param0:71 + -K:228))
           /\ (!(0 <= K:228)
                 \/ -mid_i:229 <= (-param0:71 + (1/2 * param1:74 * K:228)
                                     + (param0:71 * K:228)
                                     + (-1/2 * param1:74 * (K:228 * K:228))))
           /\ ((K:228 = 0 /\ param0:71 = mid_i:229
                  /\ __cost:96 = mid___cost:230)
                 \/ (1 <= K:228 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:230) /\ 0 <= mid_i:229
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:228 \/ !((-param1:74 + param0:71) < 0))
           /\ (!(0 <= K:231) \/ i':225 = (mid_i:229 + -K:231))
           /\ (!(0 <= K:231) \/ __cost':226 = (mid___cost:230 + K:231))
           /\ ((K:231 = 0 /\ mid_i:229 = i':225
                  /\ mid___cost:230 = __cost':226)
                 \/ (1 <= K:231 /\ 0 <= (-1 + -mid_i:229 + param1:74)
                       /\ 0 <= mid___cost:230 /\ 0 <= (-1 + mid_i:229)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:231 \/ (-param1:74 + mid_i:229) < 0)
           /\ (K:228 + K:231) = K:227 /\ 0 <= K:227 /\ 1 <= param1:74
           /\ 0 <= i':225 /\ 0 < param1:74 /\ i':225 <= 0)})



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


Finished Gaussian Elimination.

New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=6: 
Weight(Base relation: 
  {__cost := __cost':261
   return := 0
   param0 := havoc:20
   param1 := havoc:21
   return@pos := type_err:275
   param0@pos := type_err:269
   param1@pos := type_err:270
   return@width := type_err:276
   param0@width := type_err:272
   param1@width := type_err:273
   when (((havoc:21 <= 0 /\ 0 = phi_tmp:254)
            \/ (0 < havoc:21
                  /\ ((havoc:21 < havoc:20 /\ 1 = phi_tmp:255)
                        \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp:255))
                  /\ phi_tmp:255 = phi_tmp:254)) /\ !(phi_tmp:254 = 0)
           /\ (!(0 <= K:256)
                 \/ mid_i:257 = (havoc:20 + -((havoc:21 * K:256))))
           /\ (!(0 <= K:256) \/ mid___cost:258 = K:256)
           /\ (!(0 <= K:256) \/ mid_i:257 <= (havoc:20 + -K:256))
           /\ (!(0 <= K:256)
                 \/ -mid_i:257 <= (-havoc:20 + (1/2 * havoc:21 * K:256)
                                     + (havoc:20 * K:256)
                                     + (-1/2 * havoc:21 * (K:256 * K:256))))
           /\ ((K:256 = 0 /\ havoc:20 = mid_i:257 /\ 0 = mid___cost:258)
                 \/ (1 <= K:256 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (havoc:20 + -havoc:21)
                       /\ 0 <= (-1 + mid___cost:258) /\ 0 <= mid_i:257
                       /\ 0 <= (-1 + havoc:21)))
           /\ (0 = K:256 \/ (havoc:21 + -havoc:20) <= 0)
           /\ (!(0 <= K:259) \/ i':260 = (mid_i:257 + -K:259))
           /\ (!(0 <= K:259) \/ __cost':261 = (mid___cost:258 + K:259))
           /\ ((K:259 = 0 /\ mid_i:257 = i':260
                  /\ mid___cost:258 = __cost':261)
                 \/ (1 <= K:259 /\ 0 <= (-1 + -mid_i:257 + havoc:21)
                       /\ 0 <= mid___cost:258 /\ 0 <= (-1 + mid_i:257)
                       /\ 0 <= i':260 /\ 0 <= (-1 + __cost':261)
                       /\ 0 <= (-2 + havoc:21 + -i':260)))
           /\ (0 = K:259 \/ !((havoc:21 + -mid_i:257) <= 0))
           /\ (K:256 + K:259) = K:262
           /\ (!(0 <= K:263)
                 \/ mid_i:264 = (havoc:20 + -((havoc:21 * K:263))))
           /\ (!(0 <= K:263) \/ mid___cost:265 = K:263)
           /\ (!(0 <= K:263) \/ mid_i:264 <= (havoc:20 + -K:263))
           /\ (!(0 <= K:263)
                 \/ -mid_i:264 <= (-havoc:20 + (1/2 * havoc:21 * K:263)
                                     + (havoc:20 * K:263)
                                     + (-1/2 * havoc:21 * (K:263 * K:263))))
           /\ ((K:263 = 0 /\ havoc:20 = mid_i:264 /\ 0 = mid___cost:265)
                 \/ (1 <= K:263 /\ 0 <= (-1 + havoc:21)
                       /\ 0 <= (havoc:20 + -havoc:21)
                       /\ 0 <= (-1 + mid___cost:265) /\ 0 <= mid_i:264
                       /\ 0 <= (-1 + havoc:21)))
           /\ (0 = K:263 \/ !((-havoc:21 + havoc:20) < 0))
           /\ (!(0 <= K:266) \/ i':260 = (mid_i:264 + -K:266))
           /\ (!(0 <= K:266) \/ __cost':261 = (mid___cost:265 + K:266))
           /\ ((K:266 = 0 /\ mid_i:264 = i':260
                  /\ mid___cost:265 = __cost':261)
                 \/ (1 <= K:266 /\ 0 <= (-1 + -mid_i:264 + havoc:21)
                       /\ 0 <= mid___cost:265 /\ 0 <= (-1 + mid_i:264)
                       /\ 0 <= i':260 /\ 0 <= (-1 + __cost':261)
                       /\ 0 <= (-2 + havoc:21 + -i':260)))
           /\ (0 = K:266 \/ (-havoc:21 + mid_i:264) < 0)
           /\ (K:263 + K:266) = K:262 /\ 0 <= K:262 /\ 1 <= havoc:21
           /\ 0 <= i':260 /\ 0 < havoc:21 /\ i':260 <= 0
           /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:274)
                 \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:274)))})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=13: 
Weight(Base relation: 
  {__cost := __cost':284
   return := havoc:293
   param0 := param0:71
   param1 := param1:74
   return@pos := type_err:294
   param0@pos := type_err:79
   param1@pos := type_err:80
   return@width := type_err:295
   param0@width := type_err:81
   param1@width := type_err:82
   when (((param1:74 <= 0 /\ 0 = phi_tmp:277)
            \/ (0 < param1:74
                  /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:278)
                        \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:278))
                  /\ phi_tmp:278 = phi_tmp:277)) /\ !(phi_tmp:277 = 0)
           /\ (!(0 <= K:279)
                 \/ mid_i:280 = (param0:71 + -((param1:74 * K:279))))
           /\ (!(0 <= K:279) \/ mid___cost:281 = (__cost:96 + K:279))
           /\ (!(0 <= K:279) \/ mid_i:280 <= (param0:71 + -K:279))
           /\ (!(0 <= K:279)
                 \/ -mid_i:280 <= (-param0:71 + (1/2 * param1:74 * K:279)
                                     + (param0:71 * K:279)
                                     + (-1/2 * param1:74 * (K:279 * K:279))))
           /\ ((K:279 = 0 /\ param0:71 = mid_i:280
                  /\ __cost:96 = mid___cost:281)
                 \/ (1 <= K:279 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:281) /\ 0 <= mid_i:280
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:279 \/ (param1:74 + -param0:71) <= 0)
           /\ (!(0 <= K:282) \/ i':283 = (mid_i:280 + -K:282))
           /\ (!(0 <= K:282) \/ __cost':284 = (mid___cost:281 + K:282))
           /\ ((K:282 = 0 /\ mid_i:280 = i':283
                  /\ mid___cost:281 = __cost':284)
                 \/ (1 <= K:282 /\ 0 <= (-1 + -mid_i:280 + param1:74)
                       /\ 0 <= mid___cost:281 /\ 0 <= (-1 + mid_i:280)
                       /\ 0 <= i':283 /\ 0 <= (-1 + __cost':284)
                       /\ 0 <= (-2 + param1:74 + -i':283)))
           /\ (0 = K:282 \/ !((param1:74 + -mid_i:280) <= 0))
           /\ (K:279 + K:282) = K:285
           /\ (!(0 <= K:286)
                 \/ mid_i:287 = (param0:71 + -((param1:74 * K:286))))
           /\ (!(0 <= K:286) \/ mid___cost:288 = (__cost:96 + K:286))
           /\ (!(0 <= K:286) \/ mid_i:287 <= (param0:71 + -K:286))
           /\ (!(0 <= K:286)
                 \/ -mid_i:287 <= (-param0:71 + (1/2 * param1:74 * K:286)
                                     + (param0:71 * K:286)
                                     + (-1/2 * param1:74 * (K:286 * K:286))))
           /\ ((K:286 = 0 /\ param0:71 = mid_i:287
                  /\ __cost:96 = mid___cost:288)
                 \/ (1 <= K:286 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:288) /\ 0 <= mid_i:287
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:286 \/ !((-param1:74 + param0:71) < 0))
           /\ (!(0 <= K:289) \/ i':283 = (mid_i:287 + -K:289))
           /\ (!(0 <= K:289) \/ __cost':284 = (mid___cost:288 + K:289))
           /\ ((K:289 = 0 /\ mid_i:287 = i':283
                  /\ mid___cost:288 = __cost':284)
                 \/ (1 <= K:289 /\ 0 <= (-1 + -mid_i:287 + param1:74)
                       /\ 0 <= mid___cost:288 /\ 0 <= (-1 + mid_i:287)
                       /\ 0 <= i':283 /\ 0 <= (-1 + __cost':284)
                       /\ 0 <= (-2 + param1:74 + -i':283)))
           /\ (0 = K:289 \/ (-param1:74 + mid_i:287) < 0)
           /\ (K:286 + K:289) = K:285 /\ 0 <= K:285 /\ 1 <= param1:74
           /\ 0 <= i':283 /\ 0 < param1:74 /\ i':283 <= 0)})


New-style (IRE) regular expression in IREregExpsAfterIsolation for reID=19: 
Weight(Base relation: 
  {__cost := __cost':226
   return := havoc:232
   return@pos := type_err:233
   return@width := type_err:234
   when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
            \/ (0 < param1:74
                  /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                        \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                  /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0)
           /\ (!(0 <= K:221)
                 \/ mid_i:222 = (param0:71 + -((param1:74 * K:221))))
           /\ (!(0 <= K:221) \/ mid___cost:223 = (__cost:96 + K:221))
           /\ (!(0 <= K:221) \/ mid_i:222 <= (param0:71 + -K:221))
           /\ (!(0 <= K:221)
                 \/ -mid_i:222 <= (-param0:71 + (1/2 * param1:74 * K:221)
                                     + (param0:71 * K:221)
                                     + (-1/2 * param1:74 * (K:221 * K:221))))
           /\ ((K:221 = 0 /\ param0:71 = mid_i:222
                  /\ __cost:96 = mid___cost:223)
                 \/ (1 <= K:221 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:223) /\ 0 <= mid_i:222
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:221 \/ (param1:74 + -param0:71) <= 0)
           /\ (!(0 <= K:224) \/ i':225 = (mid_i:222 + -K:224))
           /\ (!(0 <= K:224) \/ __cost':226 = (mid___cost:223 + K:224))
           /\ ((K:224 = 0 /\ mid_i:222 = i':225
                  /\ mid___cost:223 = __cost':226)
                 \/ (1 <= K:224 /\ 0 <= (-1 + -mid_i:222 + param1:74)
                       /\ 0 <= mid___cost:223 /\ 0 <= (-1 + mid_i:222)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:224 \/ !((param1:74 + -mid_i:222) <= 0))
           /\ (K:221 + K:224) = K:227
           /\ (!(0 <= K:228)
                 \/ mid_i:229 = (param0:71 + -((param1:74 * K:228))))
           /\ (!(0 <= K:228) \/ mid___cost:230 = (__cost:96 + K:228))
           /\ (!(0 <= K:228) \/ mid_i:229 <= (param0:71 + -K:228))
           /\ (!(0 <= K:228)
                 \/ -mid_i:229 <= (-param0:71 + (1/2 * param1:74 * K:228)
                                     + (param0:71 * K:228)
                                     + (-1/2 * param1:74 * (K:228 * K:228))))
           /\ ((K:228 = 0 /\ param0:71 = mid_i:229
                  /\ __cost:96 = mid___cost:230)
                 \/ (1 <= K:228 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                       /\ 0 <= (param0:71 + -param1:74)
                       /\ 0 <= (-1 + mid___cost:230) /\ 0 <= mid_i:229
                       /\ 0 <= (-1 + param1:74)))
           /\ (0 = K:228 \/ !((-param1:74 + param0:71) < 0))
           /\ (!(0 <= K:231) \/ i':225 = (mid_i:229 + -K:231))
           /\ (!(0 <= K:231) \/ __cost':226 = (mid___cost:230 + K:231))
           /\ ((K:231 = 0 /\ mid_i:229 = i':225
                  /\ mid___cost:230 = __cost':226)
                 \/ (1 <= K:231 /\ 0 <= (-1 + -mid_i:229 + param1:74)
                       /\ 0 <= mid___cost:230 /\ 0 <= (-1 + mid_i:229)
                       /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                       /\ 0 <= (-2 + param1:74 + -i':225)))
           /\ (0 = K:231 \/ (-param1:74 + mid_i:229) < 0)
           /\ (K:228 + K:231) = K:227 /\ 0 <= K:227 /\ 1 <= param1:74
           /\ 0 <= i':225 /\ 0 < param1:74 /\ i':225 <= 0)})


Step 5: =========================================================
[Newton] Running Newton
-------------------------------------------------------------------------------
Round 0:
Evaluating variable number 6 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':261
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:275
 param0@pos := type_err:269
 param1@pos := type_err:270
 return@width := type_err:276
 param0@width := type_err:272
 param1@width := type_err:273
 when (((havoc:21 <= 0 /\ 0 = phi_tmp:254)
          \/ (0 < havoc:21
                /\ ((havoc:21 < havoc:20 /\ 1 = phi_tmp:255)
                      \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp:255))
                /\ phi_tmp:255 = phi_tmp:254)) /\ !(phi_tmp:254 = 0)
         /\ (!(0 <= K:256) \/ mid_i:257 = (havoc:20 + -((havoc:21 * K:256))))
         /\ (!(0 <= K:256) \/ mid___cost:258 = K:256)
         /\ (!(0 <= K:256) \/ mid_i:257 <= (havoc:20 + -K:256))
         /\ (!(0 <= K:256)
               \/ -mid_i:257 <= (-havoc:20 + (1/2 * havoc:21 * K:256)
                                   + (havoc:20 * K:256)
                                   + (-1/2 * havoc:21 * (K:256 * K:256))))
         /\ ((K:256 = 0 /\ havoc:20 = mid_i:257 /\ 0 = mid___cost:258)
               \/ (1 <= K:256 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (havoc:20 + -havoc:21)
                     /\ 0 <= (-1 + mid___cost:258) /\ 0 <= mid_i:257
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:256 \/ (havoc:21 + -havoc:20) <= 0)
         /\ (!(0 <= K:259) \/ i':260 = (mid_i:257 + -K:259))
         /\ (!(0 <= K:259) \/ __cost':261 = (mid___cost:258 + K:259))
         /\ ((K:259 = 0 /\ mid_i:257 = i':260 /\ mid___cost:258 = __cost':261)
               \/ (1 <= K:259 /\ 0 <= (-1 + -mid_i:257 + havoc:21)
                     /\ 0 <= mid___cost:258 /\ 0 <= (-1 + mid_i:257)
                     /\ 0 <= i':260 /\ 0 <= (-1 + __cost':261)
                     /\ 0 <= (-2 + havoc:21 + -i':260)))
         /\ (0 = K:259 \/ !((havoc:21 + -mid_i:257) <= 0))
         /\ (K:256 + K:259) = K:262
         /\ (!(0 <= K:263) \/ mid_i:264 = (havoc:20 + -((havoc:21 * K:263))))
         /\ (!(0 <= K:263) \/ mid___cost:265 = K:263)
         /\ (!(0 <= K:263) \/ mid_i:264 <= (havoc:20 + -K:263))
         /\ (!(0 <= K:263)
               \/ -mid_i:264 <= (-havoc:20 + (1/2 * havoc:21 * K:263)
                                   + (havoc:20 * K:263)
                                   + (-1/2 * havoc:21 * (K:263 * K:263))))
         /\ ((K:263 = 0 /\ havoc:20 = mid_i:264 /\ 0 = mid___cost:265)
               \/ (1 <= K:263 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (havoc:20 + -havoc:21)
                     /\ 0 <= (-1 + mid___cost:265) /\ 0 <= mid_i:264
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:263 \/ !((-havoc:21 + havoc:20) < 0))
         /\ (!(0 <= K:266) \/ i':260 = (mid_i:264 + -K:266))
         /\ (!(0 <= K:266) \/ __cost':261 = (mid___cost:265 + K:266))
         /\ ((K:266 = 0 /\ mid_i:264 = i':260 /\ mid___cost:265 = __cost':261)
               \/ (1 <= K:266 /\ 0 <= (-1 + -mid_i:264 + havoc:21)
                     /\ 0 <= mid___cost:265 /\ 0 <= (-1 + mid_i:264)
                     /\ 0 <= i':260 /\ 0 <= (-1 + __cost':261)
                     /\ 0 <= (-2 + havoc:21 + -i':260)))
         /\ (0 = K:266 \/ (-havoc:21 + mid_i:264) < 0)
         /\ (K:263 + K:266) = K:262 /\ 0 <= K:262 /\ 1 <= havoc:21
         /\ 0 <= i':260 /\ 0 < havoc:21 /\ i':260 <= 0
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:274)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:274)))}

Evaluating variable number 13 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':284
 return := havoc:293
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:294
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:295
 param0@width := type_err:81
 param1@width := type_err:82
 when (((param1:74 <= 0 /\ 0 = phi_tmp:277)
          \/ (0 < param1:74
                /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:278)
                      \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:278))
                /\ phi_tmp:278 = phi_tmp:277)) /\ !(phi_tmp:277 = 0)
         /\ (!(0 <= K:279)
               \/ mid_i:280 = (param0:71 + -((param1:74 * K:279))))
         /\ (!(0 <= K:279) \/ mid___cost:281 = (__cost:96 + K:279))
         /\ (!(0 <= K:279) \/ mid_i:280 <= (param0:71 + -K:279))
         /\ (!(0 <= K:279)
               \/ -mid_i:280 <= (-param0:71 + (1/2 * param1:74 * K:279)
                                   + (param0:71 * K:279)
                                   + (-1/2 * param1:74 * (K:279 * K:279))))
         /\ ((K:279 = 0 /\ param0:71 = mid_i:280
                /\ __cost:96 = mid___cost:281)
               \/ (1 <= K:279 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:281) /\ 0 <= mid_i:280
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:279 \/ (param1:74 + -param0:71) <= 0)
         /\ (!(0 <= K:282) \/ i':283 = (mid_i:280 + -K:282))
         /\ (!(0 <= K:282) \/ __cost':284 = (mid___cost:281 + K:282))
         /\ ((K:282 = 0 /\ mid_i:280 = i':283 /\ mid___cost:281 = __cost':284)
               \/ (1 <= K:282 /\ 0 <= (-1 + -mid_i:280 + param1:74)
                     /\ 0 <= mid___cost:281 /\ 0 <= (-1 + mid_i:280)
                     /\ 0 <= i':283 /\ 0 <= (-1 + __cost':284)
                     /\ 0 <= (-2 + param1:74 + -i':283)))
         /\ (0 = K:282 \/ !((param1:74 + -mid_i:280) <= 0))
         /\ (K:279 + K:282) = K:285
         /\ (!(0 <= K:286)
               \/ mid_i:287 = (param0:71 + -((param1:74 * K:286))))
         /\ (!(0 <= K:286) \/ mid___cost:288 = (__cost:96 + K:286))
         /\ (!(0 <= K:286) \/ mid_i:287 <= (param0:71 + -K:286))
         /\ (!(0 <= K:286)
               \/ -mid_i:287 <= (-param0:71 + (1/2 * param1:74 * K:286)
                                   + (param0:71 * K:286)
                                   + (-1/2 * param1:74 * (K:286 * K:286))))
         /\ ((K:286 = 0 /\ param0:71 = mid_i:287
                /\ __cost:96 = mid___cost:288)
               \/ (1 <= K:286 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:288) /\ 0 <= mid_i:287
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:286 \/ !((-param1:74 + param0:71) < 0))
         /\ (!(0 <= K:289) \/ i':283 = (mid_i:287 + -K:289))
         /\ (!(0 <= K:289) \/ __cost':284 = (mid___cost:288 + K:289))
         /\ ((K:289 = 0 /\ mid_i:287 = i':283 /\ mid___cost:288 = __cost':284)
               \/ (1 <= K:289 /\ 0 <= (-1 + -mid_i:287 + param1:74)
                     /\ 0 <= mid___cost:288 /\ 0 <= (-1 + mid_i:287)
                     /\ 0 <= i':283 /\ 0 <= (-1 + __cost':284)
                     /\ 0 <= (-2 + param1:74 + -i':283)))
         /\ (0 = K:289 \/ (-param1:74 + mid_i:287) < 0)
         /\ (K:286 + K:289) = K:285 /\ 0 <= K:285 /\ 1 <= param1:74
         /\ 0 <= i':283 /\ 0 < param1:74 /\ i':283 <= 0)}

Evaluating variable number 19 (using IRE) 

  The IRE-evaluated value on this round is: 

Base relation: 
{__cost := __cost':226
 return := havoc:232
 return@pos := type_err:233
 return@width := type_err:234
 when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
          \/ (0 < param1:74
                /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                      \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0)
         /\ (!(0 <= K:221)
               \/ mid_i:222 = (param0:71 + -((param1:74 * K:221))))
         /\ (!(0 <= K:221) \/ mid___cost:223 = (__cost:96 + K:221))
         /\ (!(0 <= K:221) \/ mid_i:222 <= (param0:71 + -K:221))
         /\ (!(0 <= K:221)
               \/ -mid_i:222 <= (-param0:71 + (1/2 * param1:74 * K:221)
                                   + (param0:71 * K:221)
                                   + (-1/2 * param1:74 * (K:221 * K:221))))
         /\ ((K:221 = 0 /\ param0:71 = mid_i:222
                /\ __cost:96 = mid___cost:223)
               \/ (1 <= K:221 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:223) /\ 0 <= mid_i:222
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:221 \/ (param1:74 + -param0:71) <= 0)
         /\ (!(0 <= K:224) \/ i':225 = (mid_i:222 + -K:224))
         /\ (!(0 <= K:224) \/ __cost':226 = (mid___cost:223 + K:224))
         /\ ((K:224 = 0 /\ mid_i:222 = i':225 /\ mid___cost:223 = __cost':226)
               \/ (1 <= K:224 /\ 0 <= (-1 + -mid_i:222 + param1:74)
                     /\ 0 <= mid___cost:223 /\ 0 <= (-1 + mid_i:222)
                     /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                     /\ 0 <= (-2 + param1:74 + -i':225)))
         /\ (0 = K:224 \/ !((param1:74 + -mid_i:222) <= 0))
         /\ (K:221 + K:224) = K:227
         /\ (!(0 <= K:228)
               \/ mid_i:229 = (param0:71 + -((param1:74 * K:228))))
         /\ (!(0 <= K:228) \/ mid___cost:230 = (__cost:96 + K:228))
         /\ (!(0 <= K:228) \/ mid_i:229 <= (param0:71 + -K:228))
         /\ (!(0 <= K:228)
               \/ -mid_i:229 <= (-param0:71 + (1/2 * param1:74 * K:228)
                                   + (param0:71 * K:228)
                                   + (-1/2 * param1:74 * (K:228 * K:228))))
         /\ ((K:228 = 0 /\ param0:71 = mid_i:229
                /\ __cost:96 = mid___cost:230)
               \/ (1 <= K:228 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:230) /\ 0 <= mid_i:229
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:228 \/ !((-param1:74 + param0:71) < 0))
         /\ (!(0 <= K:231) \/ i':225 = (mid_i:229 + -K:231))
         /\ (!(0 <= K:231) \/ __cost':226 = (mid___cost:230 + K:231))
         /\ ((K:231 = 0 /\ mid_i:229 = i':225 /\ mid___cost:230 = __cost':226)
               \/ (1 <= K:231 /\ 0 <= (-1 + -mid_i:229 + param1:74)
                     /\ 0 <= mid___cost:230 /\ 0 <= (-1 + mid_i:229)
                     /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                     /\ 0 <= (-2 + param1:74 + -i':225)))
         /\ (0 = K:231 \/ (-param1:74 + mid_i:229) < 0)
         /\ (K:228 + K:231) = K:227 /\ 0 <= K:227 /\ 1 <= param1:74
         /\ 0 <= i':225 /\ 0 < param1:74 /\ i':225 <= 0)}

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

NumRnds: 1

Step 6: =========================================================
##### Question automaton as FWPDS
<__pstate, (Unique State Name,65)_g1> -> <__pstate, (Unique State Name,59)_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}	
<__pstate, accept> -> <__pstate, (Unique State Name,65)_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}	
##### QUERY2
WFA -
  Initial State : __pstate
  Q: {__pstate, __done}
  F: {__done}
    ( __pstate , accept , __done )	Base relation: 
{}

Weights on states: 
__done 0x528eba0: 
	Weight: Base relation: 
{when false}
	Accept: Base relation: 
{}
__pstate 0x5247160: 
	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,59)_g1 , __done )	Base relation: 
{__cost := 0
 n := havoc:20
 param0 := havoc:20
 param1 := havoc:21
 param0@pos := type_err:338
 param1@pos := type_err:339
 param0@width := type_err:340
 param1@width := type_err:341}
    ( __pstate , (Unique State Name,65)_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}

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

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

Base relation: 
{__cost := __cost':303
 n := havoc:20
 return := 0
 param0 := havoc:20
 param1 := havoc:21
 return@pos := type_err:317
 param0@pos := type_err:311
 param1@pos := type_err:312
 return@width := type_err:318
 param0@width := type_err:314
 param1@width := type_err:315
 when (((havoc:21 <= 0 /\ 0 = phi_tmp:296)
          \/ (0 < havoc:21
                /\ ((havoc:21 < havoc:20 /\ 1 = phi_tmp:297)
                      \/ (havoc:20 <= havoc:21 /\ 0 = phi_tmp:297))
                /\ phi_tmp:297 = phi_tmp:296)) /\ !(phi_tmp:296 = 0)
         /\ (!(0 <= K:298) \/ mid_i:299 = (havoc:20 + -((havoc:21 * K:298))))
         /\ (!(0 <= K:298) \/ mid___cost:300 = K:298)
         /\ (!(0 <= K:298) \/ mid_i:299 <= (havoc:20 + -K:298))
         /\ (!(0 <= K:298)
               \/ -mid_i:299 <= (-havoc:20 + (1/2 * havoc:21 * K:298)
                                   + (havoc:20 * K:298)
                                   + (-1/2 * havoc:21 * (K:298 * K:298))))
         /\ ((K:298 = 0 /\ havoc:20 = mid_i:299 /\ 0 = mid___cost:300)
               \/ (1 <= K:298 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (havoc:20 + -havoc:21)
                     /\ 0 <= (-1 + mid___cost:300) /\ 0 <= mid_i:299
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:298 \/ (havoc:21 + -havoc:20) <= 0)
         /\ (!(0 <= K:301) \/ i':302 = (mid_i:299 + -K:301))
         /\ (!(0 <= K:301) \/ __cost':303 = (mid___cost:300 + K:301))
         /\ ((K:301 = 0 /\ mid_i:299 = i':302 /\ mid___cost:300 = __cost':303)
               \/ (1 <= K:301 /\ 0 <= (-1 + -mid_i:299 + havoc:21)
                     /\ 0 <= mid___cost:300 /\ 0 <= (-1 + mid_i:299)
                     /\ 0 <= i':302 /\ 0 <= (-1 + __cost':303)
                     /\ 0 <= (-2 + havoc:21 + -i':302)))
         /\ (0 = K:301 \/ !((havoc:21 + -mid_i:299) <= 0))
         /\ (K:298 + K:301) = K:304
         /\ (!(0 <= K:305) \/ mid_i:306 = (havoc:20 + -((havoc:21 * K:305))))
         /\ (!(0 <= K:305) \/ mid___cost:307 = K:305)
         /\ (!(0 <= K:305) \/ mid_i:306 <= (havoc:20 + -K:305))
         /\ (!(0 <= K:305)
               \/ -mid_i:306 <= (-havoc:20 + (1/2 * havoc:21 * K:305)
                                   + (havoc:20 * K:305)
                                   + (-1/2 * havoc:21 * (K:305 * K:305))))
         /\ ((K:305 = 0 /\ havoc:20 = mid_i:306 /\ 0 = mid___cost:307)
               \/ (1 <= K:305 /\ 0 <= (-1 + havoc:21)
                     /\ 0 <= (havoc:20 + -havoc:21)
                     /\ 0 <= (-1 + mid___cost:307) /\ 0 <= mid_i:306
                     /\ 0 <= (-1 + havoc:21)))
         /\ (0 = K:305 \/ !((-havoc:21 + havoc:20) < 0))
         /\ (!(0 <= K:308) \/ i':302 = (mid_i:306 + -K:308))
         /\ (!(0 <= K:308) \/ __cost':303 = (mid___cost:307 + K:308))
         /\ ((K:308 = 0 /\ mid_i:306 = i':302 /\ mid___cost:307 = __cost':303)
               \/ (1 <= K:308 /\ 0 <= (-1 + -mid_i:306 + havoc:21)
                     /\ 0 <= mid___cost:307 /\ 0 <= (-1 + mid_i:306)
                     /\ 0 <= i':302 /\ 0 <= (-1 + __cost':303)
                     /\ 0 <= (-2 + havoc:21 + -i':302)))
         /\ (0 = K:308 \/ (-havoc:21 + mid_i:306) < 0)
         /\ (K:305 + K:308) = K:304 /\ 0 <= K:304 /\ 1 <= havoc:21
         /\ 0 <= i':302 /\ 0 < havoc:21 /\ i':302 <= 0
         /\ ((0 < havoc:20 /\ havoc:20 = phi_tmp___1:316)
               \/ (havoc:20 <= 0 /\ 0 = phi_tmp___1:316)))}

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

Base relation: 
{__cost := __cost':326
 return := havoc:335
 param0 := param0:71
 param1 := param1:74
 return@pos := type_err:336
 param0@pos := type_err:79
 param1@pos := type_err:80
 return@width := type_err:337
 param0@width := type_err:81
 param1@width := type_err:82
 when (((param1:74 <= 0 /\ 0 = phi_tmp:319)
          \/ (0 < param1:74
                /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:320)
                      \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:320))
                /\ phi_tmp:320 = phi_tmp:319)) /\ !(phi_tmp:319 = 0)
         /\ (!(0 <= K:321)
               \/ mid_i:322 = (param0:71 + -((param1:74 * K:321))))
         /\ (!(0 <= K:321) \/ mid___cost:323 = (__cost:96 + K:321))
         /\ (!(0 <= K:321) \/ mid_i:322 <= (param0:71 + -K:321))
         /\ (!(0 <= K:321)
               \/ -mid_i:322 <= (-param0:71 + (1/2 * param1:74 * K:321)
                                   + (param0:71 * K:321)
                                   + (-1/2 * param1:74 * (K:321 * K:321))))
         /\ ((K:321 = 0 /\ param0:71 = mid_i:322
                /\ __cost:96 = mid___cost:323)
               \/ (1 <= K:321 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:323) /\ 0 <= mid_i:322
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:321 \/ (param1:74 + -param0:71) <= 0)
         /\ (!(0 <= K:324) \/ i':325 = (mid_i:322 + -K:324))
         /\ (!(0 <= K:324) \/ __cost':326 = (mid___cost:323 + K:324))
         /\ ((K:324 = 0 /\ mid_i:322 = i':325 /\ mid___cost:323 = __cost':326)
               \/ (1 <= K:324 /\ 0 <= (-1 + -mid_i:322 + param1:74)
                     /\ 0 <= mid___cost:323 /\ 0 <= (-1 + mid_i:322)
                     /\ 0 <= i':325 /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (-2 + param1:74 + -i':325)))
         /\ (0 = K:324 \/ !((param1:74 + -mid_i:322) <= 0))
         /\ (K:321 + K:324) = K:327
         /\ (!(0 <= K:328)
               \/ mid_i:329 = (param0:71 + -((param1:74 * K:328))))
         /\ (!(0 <= K:328) \/ mid___cost:330 = (__cost:96 + K:328))
         /\ (!(0 <= K:328) \/ mid_i:329 <= (param0:71 + -K:328))
         /\ (!(0 <= K:328)
               \/ -mid_i:329 <= (-param0:71 + (1/2 * param1:74 * K:328)
                                   + (param0:71 * K:328)
                                   + (-1/2 * param1:74 * (K:328 * K:328))))
         /\ ((K:328 = 0 /\ param0:71 = mid_i:329
                /\ __cost:96 = mid___cost:330)
               \/ (1 <= K:328 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:330) /\ 0 <= mid_i:329
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:328 \/ !((-param1:74 + param0:71) < 0))
         /\ (!(0 <= K:331) \/ i':325 = (mid_i:329 + -K:331))
         /\ (!(0 <= K:331) \/ __cost':326 = (mid___cost:330 + K:331))
         /\ ((K:331 = 0 /\ mid_i:329 = i':325 /\ mid___cost:330 = __cost':326)
               \/ (1 <= K:331 /\ 0 <= (-1 + -mid_i:329 + param1:74)
                     /\ 0 <= mid___cost:330 /\ 0 <= (-1 + mid_i:329)
                     /\ 0 <= i':325 /\ 0 <= (-1 + __cost':326)
                     /\ 0 <= (-2 + param1:74 + -i':325)))
         /\ (0 = K:331 \/ (-param1:74 + mid_i:329) < 0)
         /\ (K:328 + K:331) = K:327 /\ 0 <= K:327 /\ 1 <= param1:74
         /\ 0 <= i':325 /\ 0 < param1:74 /\ i':325 <= 0)}

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

Base relation: 
{__cost := __cost':226
 i := i':225
 m := param1:74
 return := havoc:232
 return@pos := type_err:233
 return@width := type_err:234
 when (((param1:74 <= 0 /\ 0 = phi_tmp:109)
          \/ (0 < param1:74
                /\ ((param1:74 < param0:71 /\ 1 = phi_tmp:110)
                      \/ (param0:71 <= param1:74 /\ 0 = phi_tmp:110))
                /\ phi_tmp:110 = phi_tmp:109)) /\ !(phi_tmp:109 = 0)
         /\ (!(0 <= K:221)
               \/ mid_i:222 = (param0:71 + -((param1:74 * K:221))))
         /\ (!(0 <= K:221) \/ mid___cost:223 = (__cost:96 + K:221))
         /\ (!(0 <= K:221) \/ mid_i:222 <= (param0:71 + -K:221))
         /\ (!(0 <= K:221)
               \/ -mid_i:222 <= (-param0:71 + (1/2 * param1:74 * K:221)
                                   + (param0:71 * K:221)
                                   + (-1/2 * param1:74 * (K:221 * K:221))))
         /\ ((K:221 = 0 /\ param0:71 = mid_i:222
                /\ __cost:96 = mid___cost:223)
               \/ (1 <= K:221 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:223) /\ 0 <= mid_i:222
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:221 \/ (param1:74 + -param0:71) <= 0)
         /\ (!(0 <= K:224) \/ i':225 = (mid_i:222 + -K:224))
         /\ (!(0 <= K:224) \/ __cost':226 = (mid___cost:223 + K:224))
         /\ ((K:224 = 0 /\ mid_i:222 = i':225 /\ mid___cost:223 = __cost':226)
               \/ (1 <= K:224 /\ 0 <= (-1 + -mid_i:222 + param1:74)
                     /\ 0 <= mid___cost:223 /\ 0 <= (-1 + mid_i:222)
                     /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                     /\ 0 <= (-2 + param1:74 + -i':225)))
         /\ (0 = K:224 \/ !((param1:74 + -mid_i:222) <= 0))
         /\ (K:221 + K:224) = K:227
         /\ (!(0 <= K:228)
               \/ mid_i:229 = (param0:71 + -((param1:74 * K:228))))
         /\ (!(0 <= K:228) \/ mid___cost:230 = (__cost:96 + K:228))
         /\ (!(0 <= K:228) \/ mid_i:229 <= (param0:71 + -K:228))
         /\ (!(0 <= K:228)
               \/ -mid_i:229 <= (-param0:71 + (1/2 * param1:74 * K:228)
                                   + (param0:71 * K:228)
                                   + (-1/2 * param1:74 * (K:228 * K:228))))
         /\ ((K:228 = 0 /\ param0:71 = mid_i:229
                /\ __cost:96 = mid___cost:230)
               \/ (1 <= K:228 /\ 0 <= __cost:96 /\ 0 <= (-1 + param1:74)
                     /\ 0 <= (param0:71 + -param1:74)
                     /\ 0 <= (-1 + mid___cost:230) /\ 0 <= mid_i:229
                     /\ 0 <= (-1 + param1:74)))
         /\ (0 = K:228 \/ !((-param1:74 + param0:71) < 0))
         /\ (!(0 <= K:231) \/ i':225 = (mid_i:229 + -K:231))
         /\ (!(0 <= K:231) \/ __cost':226 = (mid___cost:230 + K:231))
         /\ ((K:231 = 0 /\ mid_i:229 = i':225 /\ mid___cost:230 = __cost':226)
               \/ (1 <= K:231 /\ 0 <= (-1 + -mid_i:229 + param1:74)
                     /\ 0 <= mid___cost:230 /\ 0 <= (-1 + mid_i:229)
                     /\ 0 <= i':225 /\ 0 <= (-1 + __cost':226)
                     /\ 0 <= (-2 + param1:74 + -i':225)))
         /\ (0 = K:231 \/ (-param1:74 + mid_i:229) < 0)
         /\ (K:228 + K:231) = K:227 /\ 0 <= K:227 /\ 1 <= param1:74
         /\ 0 <= i':225 /\ 0 < param1:74 /\ i':225 <= 0)}

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

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

Variable bounds at line 26 in run

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

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