Shostak primitives (records, enums, addition/subtraction/scaling/comparison for arithmetic, extract/concat for BV)
Multiplication (through interval propagation and/or distributivity), unless --no-nla is passed
Exponentiation (delayed functions)
BV primitives (bugs may exist but we should have complete propagators there)
Int/BV conversions (delayed functions)
Non-linear arithmetic, integer/real conversions, and FP operators if--enable-theories fpa (or maybe --enable-theories nra,ria sometimes) is provided; must check the preludes
ADTs when #1093 is merged (presumably?)
And we don't guarantee it for:
sqrt (I think), but note that we don't really advertise it as a primitive
Arrays (I think we still have bugs with abstract values but maybe we don't? Also needs to be checked)
I guess we do support it for almost everything then, but all of these need to be checked before being put into the documentation.
As discussed at the user's club meeting.
Off the top of my head this is:
--no-nlais passed--enable-theories fpa(or maybe--enable-theories nra,riasometimes) is provided; must check the preludesAnd we don't guarantee it for:
sqrt(I think), but note that we don't really advertise it as a primitiveI guess we do support it for almost everything then, but all of these need to be checked before being put into the documentation.