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

# Find the values of x that satisfy
# each of the following equations.
# a. ceiling((x - 1)/2) = floor(x/2)
# b. ceiling((x - 1)/3) = floor(x/3)

def floor(x):
    return x&0xff00

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

s=Solver()

x = BitVec('x', 16)

# 1 in Q8.8 is just 0x0100 or 1<<8
s.add(ceiling((x-0x100)/2) == floor(x/2))
#s.add(ceiling((x-0x100)/3) == floor(x/3))

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

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