Quantified Let Expressions in Encoding Unsoundness

[ArquintL]

The following code snippet successfully verifies although a verification error is expected for the assert false statement.
This is a duplicate of Silicon #736 because Gobra encodes the following program using several quantifiers and let expressions.
This bug has recently been introduced in Viper and older Viper versions (e.g. used by the current stable release) are not affected.

package issue659

type Node struct {
    ok     bool
}

pred (s *Set)mem(){
    acc(s) &&
    acc(s.nodes) &&
    forall i int:: i in domain(s.nodes) ==> acc(s.nodes[i])
}

type Set struct {
    nodes map[int]*Node
}

requires s.mem()
requires acc(n)
requires !(k in unfolding s.mem() in domain(s.nodes))
func (s *Set) add2(n *Node, k int){
    unfold s.mem()
    _,ok := s.nodes[0];
    if ok {
        s.nodes[k] = n
        fold s.mem()
        assert false // should fail
        return
    }
}