Crash on example with "unknown symbol"

[marcoeilers]

The following program crashes Silicon; Z3 complains that it does not now the symbol "result":

// fields of Node
field vari: Int   // negative for leafs
field left: Ref
field right: Ref
field height: Int
field const: Bool

// field of BB
field map: Map[Ref, Ref]

function lookupKey(bdd: Ref, node: Ref): Ref
    requires isBDD(bdd)
    requires acc(isNode(node), wildcard)
    ensures (result == null) == (unfolding isBDD(bdd) in (forall n: Ref :: n in domain(bdd.map) ==> !equal(n, node)))
    ensures (result != null) == (unfolding isBDD(bdd) in result in domain(bdd.map) && equal(result, node))

predicate isNode(this: Ref) {
    acc(this.vari) && acc(this.height) && 0 <= this.height &&
    (0 <= this.vari ==> 
        acc(this.left) && isNode(this.left) && (unfolding isNode(this.left) in this.left.height < this.height) &&
        acc(this.right) && isNode(this.right) && (unfolding isNode(this.right) in this.right.height < this.height)
    ) &&
    (this.vari < 0  ==> acc(this.const)) 
}

predicate isBDD(this: Ref) {
    acc(this.map) &&
    (forall n: Ref :: n in domain(this.map) ==> acc(isNode(n), wildcard)) &&
    (forall n: Ref :: n in range(this.map) ==> acc(isNode(n), wildcard))
}


function equal(n: Ref, m: Ref): Bool
    requires acc(isNode(n), wildcard)
    requires acc(isNode(m), wildcard)
{
    unfolding acc(isNode(n), wildcard) in unfolding acc(isNode(m), wildcard) in
    (n.vari < 0 && m.vari < 0 && n.const == m.const) ||
    (0 <= n.vari && n.vari == m.vari && equal(n.left, m.left) && equal(n.right, m.right))
}

function isTrue(n: Ref): Bool
    requires acc(isNode(n), wildcard)
{
    unfolding acc(isNode(n), wildcard) in
    n.vari < 0 && n.const
}

function isFalse(n: Ref): Bool
    requires acc(isNode(n), wildcard)
{
    unfolding acc(isNode(n), wildcard) in
    n.vari < 0 && !n.const
}

method getNode(bdd: Ref, node: Ref) returns (res: Ref)
    requires isBDD(bdd)
    requires acc(isNode(node), wildcard)
    ensures isBDD(bdd)
    ensures acc(isNode(node), wildcard)
    ensures acc(isNode(res), wildcard)
{
    unfold acc(isNode(node), wildcard)
    if(0 <= node.vari && node.left == node.right) {
        unfold acc(isNode(node.left), wildcard)
        res := node.left
        fold acc(isNode(node.left), wildcard)
        fold acc(isNode(res), wildcard)
    } else {
        var key: Ref
        key := lookupKey(bdd, node)
        unfold isBDD(bdd)
        if(key == null) {
            bdd.map := bdd.map[node := node]
            res := node
        } else {
            res := bdd.map[key]
        }
        fold isBDD(bdd)
    }
    fold acc(isNode(node), wildcard)
}

method mkLeaf(bdd: Ref, val: Bool) returns (res: Ref)
    requires isBDD(bdd)
    ensures  isBDD(bdd)
    ensures acc(isNode(res), wildcard)
{
    var n: Ref
    n := new(vari, const)
    n.vari := -1
    n.const := val
    fold isNode(n)
    res := getNode(bdd, n)
}

method mkCompound(bdd: Ref, v: Int, l: Ref, r: Ref) returns (res: Ref)
    requires isBDD(bdd)
    requires 0 <= v
    requires acc(isNode(l), wildcard)
    requires acc(isNode(r), wildcard)
    ensures  isBDD(bdd)
    ensures acc(isNode(res), wildcard)
{
    var n: Ref
    n := new(vari, left, right)
    n.vari := v
    n.left := l
    n.right := r
    fold acc(isNode(n), wildcard)
    res := getNode(bdd, n)
}

method not(bdd: Ref, node: Ref) returns (res: Ref)
    requires isBDD(bdd)
    requires acc(isNode(node), wildcard)
    ensures  isBDD(bdd)
    ensures  acc(isNode(node), wildcard)
    ensures  acc(isNode(res), wildcard)
{
    if(isTrue(node)) {
        res := mkLeaf(bdd, false)
    } else {    
        if(isFalse(node)) {
        res := mkLeaf(bdd, true)
        } else {
            unfold acc(isNode(node), wildcard)
            var l1: Ref
            var r1: Ref
            l1 := not(bdd,node.left)
            r1 := not(bdd,node.right)
            res := mkCompound(bdd, node.vari, l1, r1)
        }
    }
}

method and(bdd: Ref, node1: Ref, node2: Ref) returns (res: Ref)
    requires isBDD(bdd)
    requires acc(isNode(node1), wildcard)
    requires acc(isNode(node2), wildcard)
    ensures  isBDD(bdd)
    ensures  acc(isNode(node1), wildcard)
    ensures  acc(isNode(node2), wildcard)
    ensures  acc(isNode(res), wildcard)
{
    if(isTrue(node1)) {
        res := node2
    } else {    
        if(isTrue(node2)) {
        res := node1
        } else {
            if(isFalse(node1) || isFalse(node2)) {
                res := mkLeaf(bdd, false)
            } else {
                var l1: Ref
                var r1: Ref
                unfold acc(isNode(node1), wildcard)
                unfold acc(isNode(node2), wildcard)
                if (node1.vari < node2.vari) {
                    l1 := and(bdd, node1.left, node2)
                    r1 := and(bdd, node1.right, node2)
                    res := mkCompound(bdd, node1.vari, l1, r1)
                } else {
                    if (node1.vari == node2.vari) {
                        l1 := and(bdd, node1.left, node2.left)
                        r1 := and(bdd, node1.right, node2.right)
                        res := mkCompound(bdd, node1.vari, l1, r1)
                    } else {
                        l1 := and(bdd,node1, node2.left)
                        r1 := and(bdd,node1, node2.right)
                        res := mkCompound(bdd, node2.vari, l1, r1)
                    }
                }
            }
        }
    }
}

[marcoeilers]

Fixed in PR #712