An implementation of `zendo` using linear-arithmetic