from z3 import *

def addCheck(a, b, c_in, s, c_out):
  return(And(s == Xor(Xor(a, b), c_in),
         c_out == Or(And(a, b), And(b, c_in), And(a, c_in))))

def test1():
  a, b, c_in = Bools('a b c_in')
  x = Xor(a, b)
  s = Xor(x, c_in)
  y = Not(And(a, b))
  z = Not(And(c_in, x))
  c_out = Not(And(y, z))
  prove(addCheck(a, b, c_in, s, c_out))