Sorry if I missed this somewhere in the documentation. Are division and modulus on mathematical integers defined in the SMT-LIB standard? If so, how are they defined when the two arguments have different signs? I saw a message from Clark about the analogous operations on bitvectors (bvsdiv, bvsmod) proposing quotients be rounded towards zero. John.