* iface/dve2/dve2check.cc: Use postprocessor to simplify the code.
* iface/dve2/dve2check.test: Adjust to some different output values
when a counterexample is found, caused by nondeterminism introduced by
the orders of transitions.