When the match error bug from https://github.com/gradual-verification/gvc0/issues/18 is temporarily resolved by making predicate bodies precise, another error pops up: gvc.weaver.WeaverException: Invalid branch condition. It seems like the issue is related to the fact that the ViperBranch object’s apply definition is missing cases for positional information that are fold and unfold statements. In particular, the branch condition that is creating the exception is: BranchCond(!(a == c), start == end, Some(GenericNode(fold acc(sortedSegHelper(a, c, aPrev, cVal), write)))).
When the match error bug from https://github.com/gradual-verification/gvc0/issues/18 is temporarily resolved by making predicate bodies precise, another error pops up:
gvc.weaver.WeaverException: Invalid branch condition. It seems like the issue is related to the fact that theViperBranchobject’sapplydefinition is missing cases for positional information that are fold and unfold statements. In particular, the branch condition that is creating the exception is:BranchCond(!(a == c), start == end, Some(GenericNode(fold acc(sortedSegHelper(a, c, aPrev, cVal), write)))).