Address Heapster Implication Prover Bug (Word Equality)

[ChrisEPhifer]

Previously, the function implLLVMFieldTryProveWordEq had a case like this:

  _ ->
    implDropM y p >>> implLLVMFieldSetTrue x (llvmFieldSetEqVar fp y) >>>
    return Nothing

The pattern-match here is on the permission left on top of the stack by an elimination as performed by elimOrsExistsNamesM; in the above version, this is being ignored, and the previous permission p is propagated to implDropM.

This is incorrect, as elimOrsExistsNamesM can, of course, perform an elimination and change the permission at the top of the stack. Fortunately, the correction is trivial:

  p' ->
    implDropM y p' >>> implLLVMFieldSetTrue x (llvmFieldSetEqVar fp y) >>>
    return Nothing

Thank you to @eddywestbrook for catching this!

[eddywestbrook]

I'm Eddy Westbrook, and I approve this change