Thanks Rustan,
Meanwhile I have been reading "Solving quantified verification conditions using SMT" (Ge et al) which, together with your email, has made things a lot clearer. Could I check the following (speculative) reasoning? I have three specific questions Q1Q3
below.
The program
method Main() {
assert (exists x:: x>0) ==> (exists x:: x>0);
assume exists x:: x>0;
assert exists x:: x>0;
}
gives
input(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
Dafny program verifier finished with 1 verified, 1 error
So there's a difference between "assert A==>A;" and "assume A; assert A;". In this case the former succeeds but the latter fails.
Why does assert A==>A succeed, in spite of there being no trigger? Is it because it is a propositional tautology whose negation is therefore easily refuted by the SAT solver, thus never needing to examine the quantifiers at all?
===Q1: Is that correct?
And why does assume A; assert A; fail? Here I will try to combine your email with what I read in Ge et al. In this case the two abstract literals are considered to be different, and so the DPLL state begins with
 (exists x:: x>0), (forall x:: !(x>0))
the two literals treated (to repeat) as distinct. Then after UnitPropagate we have
(exists x:: x>0), (forall x:: !(x>0))  (exists x:: x>0), (forall x:: !(x>0))
and then after existsinst we have
(exists x:: x>0), (forall x:: !(x>0))  (exists x:: x>0), (forall x:: !(x>0)), !(exists x:: x>0)  X>0
for a new Skolem constant X. Then UnitPropagate gives
(exists x:: x>0), (forall x:: !(x>0)), X>0  (exists x:: x>0), (forall x:: !(x>0)), !(exists x:: x>0)  X>0 ,
and the whole thing would be finished off nicely by instantiating forall x to X  but that does not happen because no subexpression in the forall mentions X (as indeed it cannot, since X was fresh). And so we are stuck.
===Q2: Is that correct?
===Q3: This is the essential difference between asserting an implication, and assuming antecedent then asserting consequent, that in the latter case the SAT solver does not get a chance to notice that two literals are the same?
Thanks!
