Skip to content

Conjunction of abstract functions is not able to be asserted #588

Description

@fosslinux

viperproject/silicon#989 also appears to apply to Carbon.

Example program:

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)
}

Output:

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions