[SMT-LIB] Integer division

John R Harrison johnh at ichips.intel.com
Tue Aug 5 12:32:25 EDT 2008

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


More information about the SMT-LIB mailing list