Refine using YAML violation witnesses

[sim642]

This is an extension of #1301, which #1512 implemented on a primitive level where the contents of the violation sequence aren't used at all.

It should be possible to interpret the violation sequence and refine our analysis accordingly. We should be able to kill some paths or refine some values based on that, a la (linear) observer automaton.
That would be more likely to reject some violation witnesses whose verdict might be correct, but the counterexample is obviously wrong.

Despite the YAML format trying to be less tied to internal representations, one big obstacle for us might be branching since CIL transformations introduce more conditionals. If we count branches incorrectly, we can become unsound. GraphML witness generation tried to do some un-CIL transformations, but those are probably incomplete.