http://cs.nyu.edu/pipermail/cvc-users/2015/000675.html おお。 CVC4って帰納的なデータ型(data)だけでなく、 余帰納的なデータ型(codata)にも対応しているんだ。 

A Decision Procedure for (Co)datatypes in SMT Solvers
http://lara.epfl.ch/~reynolds/cade15.pdf