DafnyVSCode / Dafny-VSCode

Dafny 2 for Visual Studio Code (Legacy)
https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode-legacy
MIT License
18 stars 12 forks source link

assert fails to respond to !false in the same way as if !false #63

Open davidstreader opened 4 years ago

davidstreader commented 4 years ago

Hi with the code below

function method palin(a:seq<int>) :bool {
    forall i:int :: (0<=i && i<(|a|/2)) ==> a[i]==a[|a|-i -1]
}
method Main() { 
    var xe:seq<int> := [0,1,2,3,0];
    var se:seq<int> := [0,1,2,1,0];
    var ohb := palin(se);
    var ohx :bool := palin(xe);
    print "ohb= ",ohb,"\n";
    print "ohx= ",ohx,"\n";
    assert ohb;
    //assert !ohx;    
}

when run the output is:

    ohb= true
    ohx= false

But uncommenting the final assert and it will not verify. As the if statement knows that ohx is false I assume that the assert should also know this? regards david