kdrag.theories.logic.temporal.Eq

kdrag.theories.logic.temporal.Eq(x, y)

>>> x,y = smt.Consts("x y", TSort(smt.IntSort()))
>>> smt.simplify(Valid(Eq(x,y)))
val(x)[0] == val(y)[0]