bitwiseAnd verification

from z3 import *

width = 64

Range = Datatype("range")
Range.declare('make', ('lo', BitVecSort(width)), ('hi', BitVecSort(width)))
Range = Range.create()

def isEmptySet(r):
    return And((Range.lo(r) == BitVecVal(0, width)), (Range.hi(r) == BitVecVal(0, width)))

def isFullSet(r):
    return And((Range.lo(r) == BitVecVal(-1, width)), (Range.hi(r) == BitVecVal(-1, width)))

def fullSet():
    return Range.make(BitVecVal(-1, width), BitVecVal(-1, width))

def emptySet():
    return Range.make(BitVecVal(0, width), BitVecVal(0, width))

def isWrappedSet(r):
    return UGT(Range.lo(r), Range.hi(r))

def getUnsignedMax(r):
    return If(Or(isFullSet(r), isWrappedSet(r)),
              BitVecVal(-1, width),
              Range.hi(r) - 1)

def umin(x, y):
    return If(ULT(x, y), x, y)

def bitwiseAnd(x, y):
    UM = umin(getUnsignedMax(x), getUnsignedMax(y))
    return If(Or(isEmptySet(x), isEmptySet(y)),
              emptySet(),
              If(UM == BitVecVal(-1, width),
                 fullSet(),
                 Range.make(BitVecVal(0, width), UM + 1)))

def invariant(r):
    return Implies(Range.lo(r) == Range.hi(r),
                   Or(Range.lo(r) == BitVecVal(0, width), Range.lo(r) == BitVecVal(-1, width)))

def memberOf(x, r):
    return If(isEmptySet(r),
              False,
              If(isFullSet(r),
                 True,
                 If(isWrappedSet(r),
                    Or(UGE(x, Range.lo(r)), ULT(x, Range.hi(r))),
                    And(UGE(x, Range.lo(r)), ULT(x, Range.hi(r))))))

def check():
    x = BitVec('x', width)
    y = BitVec('y', width)
    z = BitVec('z', width)
    w = BitVec('w', width)
    a = Range.make(x, y)
    b = Range.make(z, w)
    o = BitVec('o', width)
    p = BitVec('p', width)

    s = Solver()
    s.add(invariant(a))
    s.add(invariant(b))
    s.add(memberOf(o, a))
    s.add(memberOf(p, b))
    s.add(Not(memberOf(o & p, bitwiseAnd(a, b))))

    res = s.check()
    print res
    if res == sat:
        m = s.model()
        print m

check()