Z3 code does not work for specified number of iterations

Question

This code only works for i=4 , but if the location is not initialized, it runs for i=19 ????? location=BoolVal(False) here the location is initialized

 from z3 import * x,t,t1,t2,x_next=Reals ('xt t1 t2 x_next') location,location_next=Bools('location location_next') x=20 #t1=0 t=0 location=BoolVal(False) #set_option(precision=10) k=20 for i in range(k): s=Solver() s.add(Or(And((10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0,Not(location_next)), And((10*x_next)>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0,location_next)), location_next==If(And(Not(location),x_next<19),True,If(And(location,x_next>21),False,location))) print i print s.check() if s.check()==unsat: break m=s.model() x=m[x_next] #t1=m[t2] print m[x_next].as_decimal(10) 

Answer 1

Short answer: the formula added to the s.add(...) command is unsatisfactory at iteration 4. At the beginning of iteration 4, we have x 19 , and location is False . Replacing x and location in the formula, we have:

 [Or(And(10*x_next >= 3*t1 - 3*t2 + 190, 10*x_next <= 190 - t2 + t1, x_next >= 18, t2 - t1 > 0, Not(location_next)), And(10*x_next >= t2 - t1 + 190, 5*x_next <= 95 + t2 - t1, x_next <= 22, t2 - t1 > 0, location_next)), location_next == If(And(Not(False), x_next < 19), True, If(And(False, x_next > 21), False, False))] 

After simplifying the above formula, we have:

 [Or(And(10*x_next >= 190 + 3*t1 - 3*t2, 10*x_next <= 190 - t2 + t1, x_next >= 18, t2 - t1 > 0, Not(location_next)), And(10*x_next >= 190 + t2 - t1, 5*x_next <= 95 + t2 - t1, x_next <= 22, t2 - t1 > 0, location_next)), location_next == x_next < 19] 

To show the unsatisfactoryness of this formula, consider the following two cases: location_next - True, or location_next - False.

• location_next - True. Then x_next < 19 should also be True. Moreover, the first argument of Or is False. Thus, the formula is feasible only if we can make the second argument True. This is not the case because the following is unsatisfactory:

  10*x_next >= 190 + t2 - t1, 5*x_next <= 95 + t2 - t1, x_next < 19

  From the first two inequalities it follows that x_next >= 19 .

• location_next - False. Then x_next >= 19 should be True. For a similar argument, the formula is feasible only if we can make the first argument Or True. This is also not possible, as the following is unsatisfactory:

  10*x_next <= 190 - t2 + t1, t2 - t1 > 0, 19 <= x_next

  From the first two inequalities it follows that x_next < 19 .

Note. You did not update the location value using location_next at the end of the loop. You do this for x , but not for location . This is an orthogonal task. I was expecting a statement like:

 location=m[location_next]