The Yices support needs some care. First is to revert d6fe42d since c3 instances have been retired. This will trigger some test failures:

1. In bvlib.rkt the rotate-left and rotate-right tests call integer->bitvector, so they should require the int2bv feature.
2. In real.rkt tests:< triggers a "logic already set" error from Yices.

There could be more errors, but I ran out of time to troubleshoot. This can also be a good time to try supporting the latest version of Yices.