Uninformative error message for uninterpreted polymorphic functions

[msaaltink]

I was trying a proof using unint_yices and encountered this error message

Could not create sbv argument for Vec (64) (Bool))

The actual problem, as I eventually found out, is that I had asked for a polymorphic function to be uninterpreted. This error message is not much help in figuring that out!

[brianhuffman]

I just checked, and this is still a problem. Here's how to easily reproduce the error:

sawscript> let {{ foo x = x }}
sawscript> prove (unint_yices ["foo"]) {{ \ (x:[64]) (y:[64]) -> x == y ==> foo x == foo y }}
saw: Stack trace:
"prove" (<stdin>:1:1-1:6):
"unint_yices" (<stdin>:1:8-1:19):
Could not create sbv argument for Vec (64) (Bool)

What we want is for this example to just work. When we ask for a polymorphic function to be uninterpreted, the SMT-Lib backend should get a separate uninterpreted function declared at each type instance that the function is used at.

[brianhuffman]

I'm reopening for now, until we add a proper regression test to the saw-script test suite.