Skip to content

Lots of tests fail with --conditionalizePermissions #851

@marcoeilers

Description

@marcoeilers

At least the following:

  • issues/carbon/0179 (unsound because of incorrect treatment of perm-expressions, will be fixed in PR Not pushing conditions using permission introspection further in #853)
  • issues/silicon/0008 (expected incompleteness, --conditionalizePermissions introduces disjunctive aliasing, works with MCE)
  • issues/silicon/0114 (default Silicon is incomplete, test fails because --conditionalizePermissions leads to correct output)
  • issues/silicon/0282 (expected incompleteness, --conditionalizePermissions seems to trigger a general Silicon triggering issue)
  • issues/silicon/0324 (expected incompleteness, --conditionalizePermissions introduces a situation where greedy Silicon is incomplete, works with MCE)
  • issues/silicon/unofficial003 (used to trigger a bug in Silicon, fixed in PR Recording constraints for newly-introduced variables during state consolidation #852)
  • third_party/stefan_recent/testTreeRecursive

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    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