Track and show decidability information

[Philipp15b]

It could be useful for users of Caesar what features a verification query has. For example, whether it contains quantifiers, linear or nonlinear arithmetic, and so on. Showing then whether a query is decidable or not would also help. We could also point to specific reasons, such as nonlinear expressions and suggest the user might change those to improve the proof.

This could be incorporated with other information obtained from after running the query, such as resource counts, quantifier instantiations and more.