bvsdiv and bvsrem

[erk...@gmail.com]

Looking at https://smt-lib.org/theories-FixedSizeBitVectors.shtml

I see bvudiv and bvurem, but I see no mention of bvsdiv and bvsrem.

Are these mentioned somewhere else?

Cheers,

-Levent.

[Clark Barrett]

These are syntactic sugar, defined in the QF_BV logic, here:

https://smt-lib.org/logics-all.shtml#QF_BV

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/1f440072-cb5c-4242-8081-8c29dd8fdd1fn%40googlegroups.com.