
When I try to write a simple program postcondition, which should be trivially true,I get unsatisfied postcondition as output.
Here is my postcondition:
there exists an integer i in range (10:10), such that i==0,i.e.
ensures exists{int i in (10:10); i==0};
according to me this postcondition should be trivially true for all examples, but thats not the case.
Please help me
Thanks, in advance



Unfortunately, SMT solvers such as Z3, which is the prover behind Spec#, have weak support for existential quantifiers. It is sometimes possible to provide intermediate assertions that help Z3 find a witness for the quantified variable, but I have no suggestion
how to fix your example. If this is part of a bigger example, you could post the entire method; maybe we can come up with a fix then.
Cheers,
Peter



I am not talking about any specific example, but in general. The postcondition and example i have is pretty complex,so I am not posting it here, I tried, in all the examples provided on the page, this assertion seems to fail for all of them. It would nice
of you even if you could give me any workaround,such that I could write my conditions in a different way and make them work(I tried negating, and using forall quantifier but that doesnot works ).
For example:
class Example
{
int x;
void Inc(int y)
ensures exists{int i in (10:10); i==0};
{ x += y;
}
}

