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

"""
Prove each statement, where n is an integer.
a. ceiling(n/2) = floor((n + 1)/2)
b. floor(n/2) = ceiling((n - 1)/2)
"""

def floor(x):
    return x&0xff00

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

s=Solver()

n = BitVec('n', 16)

# n is always integer, it has no fraction
s.add((n&0xff)==0)

# prevent integer overflow, n is always positive
s.add(n<0x8000)

s.add(ceiling(n/2) != (floor((n+0x100)/2))) # a
#s.add(floor(n/2) != (ceiling((n-0x100)/2))) # b

# must be unsat for a/b
print (s.check())