#!/usr/bin/env python3
from z3 import *

# Find numbers x and y such that
# floor(x + y) != floor(x) + floor(y) and
# ceiling(x + y) != ceiling(x) + ceiling(y).

def floor(x):
    return x&0xff00

def ceiling(x):
    return If((x&0xff)!=0, (x&0xff00)+0x100, x)

s=Solver()

x,y = BitVecs('x y', 16)

s.add(floor(x+y) != floor(x) + floor(y))
s.add(ceiling(x+y) != ceiling(x) + ceiling(y))

print (s.check())
m=s.model()

_x=m[x].as_long()
_y=m[y].as_long()
print ("x=0x%04x or %f" % (_x, float(_x)/0x100))
print ("y=0x%04x or %f" % (_y, float(_y)/0x100))