use ghc's z-encoding for talking to smtlib2