Demonstrates function counter-examples
f x z == f (y+2) z whenever
x == y+2. Naturally correct:
f is commutative; which is not necessarily true!
Indeed, the SMT solver returns a counter-example function that is
not commutative. (Note that we have to use Yices as Z3 function
counterexamples are not yet supported by sbv.) We have:
proveWith yicesSMT09 $ forAll ["x", "y"] thmBadFalsifiable. Counter-example: x = 0 :: SWord8 y = 128 :: SWord8 -- uninterpreted: f f 128 0 = 32768 f _ _ = 0
Note how the counterexample function
f returned by Yices violates commutativity;
thus providing evidence that the asserted theorem is not valid.
Old version of Yices, which supports nice output for uninterpreted functions.