Getting Integer value from Instance in Z3

Question

My code is

def test():
    s = Solver()
    a = Int('x')
    b = Int('y')
    s.add(a*b==22)
    print s.check()
    return s.model()[a], s.model()[b]

This will print numbers, but when you see type(s.model()[a]) or type(s.model()[b]) it will give <type 'instance'> . How to cast it in a way it will return <type 'int'> ? I cannot use the return type into my code any further as it returned instance even though if you print s.model()[a] it will look like a integer but it isn't.

Answer 1

Simply use the as_long method. That is, replace the last line in your function with:

   return s.model()[a].as_long(), s.model()[b].as_long()