Separating definitions and other assumptions to fix a wand-related unsoundness

[marcoeilers]

This PR extends Silicon's path condition stacks to differentiate between general assumptions and assumptions that represent definitions. For the latter, the new method assumeDefinition is introduced.
The purpose of this distinction is to fix the unsoundness described in issue #338, which was previously already partly addressed and made much more difficult to trigger by @mschwerhoff.

Now, after packaging a wand, instead of performing a smoke check to see if assumptions from producing a wand left us in an inconsistent state and only remembering path conditions if this is not the case (this was the previous workaround, but it does not prevent us from unsoundly assuming properties other than false), we can omit the smoke check and always assume only the definitions, but no other path conditions.

The previous implementation unsoundly verified the following example:

function otherFunc(s: Seq[Int], i: Int): Bool
    requires |s| > 1
{ true }

method foo(x: Ref, y: Ref, s: Seq[Int], i: Int)
{
    package (|s| > 3 ? (i > 1 && i < |s| - 2 && otherFunc(s, i)) : (i > 1 && i < |s| - 2))  --* true {
    }
    //:: ExpectedOutput(assert.failed:assertion.false)
    assert |s| > 0
}

[marcoeilers]

@mschwerhoff Do you think this makes sense the way I did it?

[mschwerhoff]

Looks good to me. Thanks for addressing this long-standing issue!