Dafny-VSCode icon indicating copy to clipboard operation
Dafny-VSCode copied to clipboard

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

Open davidstreader opened this issue 4 years ago • 0 comments

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

davidstreader avatar Jul 20 '20 06:07 davidstreader