Z3Interfacing and TheoryInstantion only aware of each other, yet...

[quickbeam123]

While it's OK to translate some theory functions and predicates such as REAL_IS_RAT for Z3 as uninterpreted in AVATAR, it is not OK for TheoryInstantion. The latter now hardcodes a list of these and never even asks Z3 if such a question would contain any. From the sw-engineering perspective this is not ideal. Let's:

*) Change theory instantiation so that the second step (the instantiation) is evaluated (and thus verified) by vampire (at least in debug mode)
*) Make the list of unsupported operations in theory instantiation provided by the Z3Interfacing, so that it's closer to it in the code and can be reduced as more operations get supported
*) Reduce the list of unsupported operations in Z3Interfacing: some of them are identity functions (REAL_TO_REAL) or constant true (REAL_IS_REAL, but even REAL_IS_RAT) anyway...)