"stp -h" suggests that "stp -p" will print a counterexample, if the input formula is Invalid.
But, running "stp -p" on the following input:
x, t : BOOLEAN;
ASSERT(t <=> x);
yields the following output:
ASSERT( x = t );
ASSERT( t = TRUE );
This is not what I wanted to see. It is not a valid counterexample. A counterexample should provide a concrete assignment (assigning either TRUE or FALSE to each boolean variable) that satisfies all of the ASSERTs. Here we do not yet have a concrete assignment.
If STP could perform constant propagation, or instantiate its template-counterexample to get a fully concrete counterexample, that would be a lot more helpful.
In theory, I could write my own program to parse the output of STP and perform constant propagation myself, but this would be annoying to do, and would require every user of "stp -p" to implement this. Since STP has the internal data structures to do this, I think it makes more sense for STP to do this.
This behavior is on the latest Subversion head. I will note that a pre-compiled version of STP that I had downloaded earlier (which is presumably an earlier version of STP) does not have this problem; it outputs fully concrete counterexamples.
I haven't fully characterized the cases where this bug appears, but it appears to be related to the "<=>" operator. All of the examples I know of where this comes up, use "<=>".
Oddly, if I turn off optimization, I get fully concrete counterexamples. In other words, "stp -p -a" works where "stp -p" fails. If I swap the order of the two ASSERTs above, I get a fully concrete counterexample. If I change "t <=> x" to "NOT(t XOR x)" (which ought to be equivalent?), I get a fully concrete counterexample. This makes me wonder if there is something funny in the optimization or rewriting.