Lots of tests fail with --conditionalizePermissions
Opened this issue · 0 comments
marcoeilers commented
At least the following:
- issues/carbon/0179 (unsound because of incorrect treatment of perm-expressions, will be fixed in PR #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 #852)
- third_party/stefan_recent/testTreeRecursive