Enormous amount of output when missing SMTLib translation running krun --prove

[ehildenb]

runtimeverification/evm-semantics#95

As demonstrated there, krun --prove generates an enormous amount of (highly redundant) output sometimes when Z3 translations are not present.

Is there a way we can be smarter about what is output to the user? Perhaps only output "missing SMTLib translation" once per missing symbol?

[dwightguth]

I think the simplest thing to do is just emit the error message and not the stack trace. Is anyone really gaining any information from those stack traces?

[ehildenb]

So you mean what would show up is still:

java.lang.UnsupportedOperationException: missing SMTLib translation for .WordStack

But none of the lines like:

        at org.kframework.backend.java.symbolic.KILtoSMTLib.translate(KILtoSMTLib.java:241)

This sounds like a good fix to me. I think there would still be some redundancy in the output though, as it seems that the same missing translation gets reported multiple times.

[dwightguth]

I mean, sure, but the main problem is that it's massively verbose, and this would take it from hundreds of lines down to maybe 10 at most.