Error in Z3Py code
z3, z3py
Solution
`m=s.model` assigns a function to `m`. I believe you meant to assign the result of calling `s.model`, so include parenthesis to make the call:
m=s.model()
Problem
Whats wrong with the following script http://rise4fun.com/Z3Py/Cbl? Adding the last two lines gives me the following error `'instancemethod' object is not #subscriptable` ``` x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next') location,location_next=Bools('location location_next') x=0 location=BoolVal(False) k=20 for i in range(k): s=Solver() s.add(Or(And(x_next-x>=2*t,x_next-x<=3*t,x_next<=12,t>0,Not(location)), And(x_next-x>=-2*t,x_next-x<=-t,x_next>=0,t>0,location)),location_next==If(And(Not(location),x_next>=12),True,If(And(location,x_next<=0),False,location))) print s.check() print s.model() m=s.model #x=m[x_next] #location=m[location_next] ```