Changes to Silver's test suite for the PR viperproject/silicon#849. Some notes about my changes:
I extended the test suite from #796 with some tests that involve magic wands in combination with quantified expressions.
In triggerFoldPackage.vpr I reverted a change from #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.
Changes to Silver's test suite for the PR viperproject/silicon#849. Some notes about my changes:
triggerFoldPackage.vprI reverted a change from #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.vpris a simplified version of assume10QPwand.vpr which I used for debugging purposes. I thought this file could be useful in the future.test0inQPWands.vpris failing again. I noticed that the simplified tests that you can find intest15.vprwere failing only when both assignmentsy.f := 1andxs[0].f := 0where 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.