In this case I observed brittle behaviour with Z3, which behaved
differently on two equivalent queries with only variables renamed.
The reason for different versions was that in isoltest, we add version
pragma to the source code and this changes the ids of AST nodes. These
are in turn used to generate uniques names for SMT variables.
Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
