Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix multiple apply of magic wands with quantified expressions #805

Open
wants to merge 22 commits into
base: master
Choose a base branch
from

Conversation

manud99
Copy link
Contributor

@manud99 manud99 commented Jun 12, 2024

Changes to Silver's test suite for the PR viperproject/silicon#849. Some notes about my changes:

  • I extended the test suite from Test suite for magic wand snap functions. #796 with some tests that involve magic wands in combination with quantified expressions.
  • In triggerFoldPackage.vpr I reverted a change from Update test annotations #790 because I got this exception again with my PR. During debugging I noticed that Silicon's master branch also throws an exception when running it with the latest Z3 version 4.13.0. From that I assume that the error does not lie in my part of the code.
  • assume10QPwand-light.vpr is a simplified version of assume10QPwand.vpr which I used for debugging purposes. I thought this file could be useful in the future.
  • test0 in QPWands.vpr is failing again. I noticed that the simplified tests that you can find in test15.vpr were failing only when both assignments y.f := 1 and xs[0].f := 0 where in place. With only one of them or both commented Silicon succeeded to verify the invariant. Thus, I assume this error does not only occur because of my changes.

@manud99 manud99 changed the title Fix multiple apply of quantified magic wand Fix multiple apply of quantified magic wand Jun 12, 2024
@manud99 manud99 changed the title Fix multiple apply of quantified magic wand Fix multiple apply of magic wands with quantified expressions Jun 27, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants