// Same signature but observably different return values. The prover should
// emit no finding — Z3 should hand back a SAT counterexample.

int id_a(int x) { return x; }
int off_by_one(int x) { return x + 1; }