SAWCore primitives cannot be made uninterpreted

[robdockins]

When using the unint variants of proof tactics, it seems that SAWCore primitives cannot be made uninterpreted; although the name of the primitive is accepted in the unint list without error, it is nonetheless still interpreted according to its semantics.

For me, this issue arises with the arrayCopy primitive. I've arranged a proof goal so that I think it should be a relatively straightforward proof of equivalence if we just take arrayCopy as a function. However, it is instead translated to the solver as a "uniquely specified" constant, where the output is a fresh variable and a universally-quantified assertion is made that specifies the value it should have. Unfortunately, this limits the solvers that can be used, and solver generally have a very hard time with such goals. I'd like to force arrayCopy to be treated as a uninterpreted function instead, and defer the reasoning about its semantics to a later step.