bvsdiv and bvsrem

23 views
Skip to first unread message

erk...@gmail.com

unread,
Aug 9, 2024, 1:29:40 PM8/9/24
to SMT-LIB
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

unread,
Aug 9, 2024, 1:51:06 PM8/9/24
to smt...@googlegroups.com
These are syntactic sugar, defined in the QF_BV logic, here:


--
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.
Reply all
Reply to author
Forward
0 new messages