function f(x: Int): Bool
function g(x: Int): Bool
method foo() {
assume forall x: Int, y: Int :: {f(x), g(y)} f(x) && g(y)
assert forall x: Int, y: Int :: {f(x), g(y)} f(x) && g(y)
}
carbon 1.0
carbon found 1 error in 3.96s:
[0] Assert might fail. Assertion f(x) might not hold. (bug1.vpr@6.10--6.60)
viperproject/silicon#989 also appears to apply to Carbon.
Example program:
Output: