Skip to content

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

Description

@davidstreader

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions