调用方法前断言成立但后续失效：二叉决策树剪枝验证问题

我正在实现二叉决策树程序，尝试编写沿指定轴剪枝树的递归方法。当树为非叶子节点且剪枝轴与分裂轴不匹配时，我想返回包含剪枝后左右子树的新树，但无法证明剪枝后的子树满足方法的保证条件。

在以下Dafny代码的prune_left方法中，分配left和right后立即断言prune_left的第四条保证，两个断言均成立。但创建new_split后，这两个断言突然失效。由于left、right以及split.left、split.right均未被修改，我无法理解断言突然失效的原因。若将最后两个断言改为假设，验证可通过，否则会在返回语句处因第四条保证而阻塞。

trait Tree {
    const dim: nat
    const depth: nat

    predicate valid()
    decreases depth

    function eval(x: array<real>) : (res: real)
    reads x
    requires x.Length == dim
    requires wellFormed(this)
    decreases depth
}

class Leaf extends Tree {
    const val: real

    predicate valid()
    decreases depth
    { ... }

    constructor (arg_dim: nat, arg_val: real)
    ...
    ensures wellFormed(this)
    ensures fresh(this)
    { ... }

    function eval(x: array<real>) : (res: real)
    requires x.Length == dim
    requires wellFormed(this)
    decreases depth
    { val }
}

class Split extends Tree {
    const axis: nat
    const loc: real
    const left: Tree
    const right: Tree

    predicate valid()
    decreases depth
    { ... }

    constructor (arg_dim: nat, arg_axis: nat, arg_loc: real, arg_left: Tree, arg_right: Tree)
    ...
    ensures wellFormed(arg_left) && wellFormed(arg_right) ==> wellFormed(this)
    ensures fresh(this)
    { ... }

    function eval(x: array<real>) : (res: real)
    reads x
    requires x.Length == dim
    requires wellFormed(this)
    decreases depth
    { if x[axis] <= loc then left.eval(x) else right.eval(x) }
}

predicate wellFormed(tree: Tree)
decreases tree.depth
{
    tree.valid() &&
    (tree is Leaf || tree is Split) &&
    (tree is Split ==> wellFormed((tree as Split).left) && wellFormed((tree as Split).right))
}

method prune_left(tree: Tree, axis: nat, loc: real) returns (res: Tree)
requires wellFormed(tree)
requires axis < tree.dim
ensures wellFormed(res)
ensures res.depth <= tree.depth
ensures res.dim == tree.dim
ensures forall x: array<real> | x.Length == tree.dim :: x[axis] <= loc ==> tree.eval(x) == res.eval(x)
decreases tree.depth
{
    if tree is Leaf {
        return tree;
    }
    var split := tree as Split;
    if split.axis != axis{
        var left := prune_left(split.left, axis, loc);
        assert forall x: array<real> | x.Length == tree.dim :: x[axis] <= loc ==> split.left.eval(x) == left.eval(x); // holds
        var right := prune_left(split.right, axis, loc);
        assert forall x: array<real> | x.Length == tree.dim :: x[axis] <= loc ==> split.right.eval(x) == right.eval(x); // holds
        var new_split := new Split (tree.dim, split.axis, split.loc, left, right);        
        assert forall x: array<real> | x.Length == tree.dim :: x[axis] <= loc ==> split.left.eval(x) == left.eval(x); // fails        
        assert forall x: array<real> | x.Length == tree.dim :: x[axis] <= loc ==> split.right.eval(x) == right.eval(x); // fails
        return new_split;
    } else {
        ...
    }
}

内容的提问来源于stack exchange，提问作者sdsanft