`saw-core`: Add the ability to assert side conditions during simulation

[RyanGlScott]

When implementing certain SAWCore primitives, it would be very convenient to be able to add side conditions about the symbolic values in scope during simulation. This is how Cryptol implements some of its corresponding primitives. Some particular examples that are worth calling out:

• Cryptol's implemention of division asserts that the divisor is not zero (see the code here). This would be useful for fixing SAW doesn't reliably fail when dividing by zero #2432 on the SAW side.
• Cryptol's implementation of recip x asserts that x is not zero (see the code here). This would be useful for implementing recip in SAWCore (see Unimplemented IntMod SAWCore operators #1912 (comment)).
• Cryptol's implementation of sequence indexing asserts that the index is within bounds (see the code here). This would be useful for fixing Incorrect simulation when indexing into array using out-of-bounds bitvector #1807 on the SAW side.

Despite my attempts to find one, I couldn't find a straightforward way to assert side conditions directly at the SAWCore simulator level (most of the code involving side conditions requires access to a Crucible backend, which the SAWCore simulator lacks). We may need to alter the SAWCore simulator API in order to return a collection of these side conditions so that the call side of the simulator can then assert these side conditions.