def longVal(x):
    """ longVal(x):
          if 'x' is a z3 constant (i.e. function of arity 0) whose value is an integer,
            then return that integer as a python long
            else return 'None'"""
    if(hasattr(x, 'as_long')): return x.as_long()
    elif(hasattr(x, 'numerator_as_long')):
        if(x.denominator_as_long() == 1): return x.numerator_as_long()
    return None