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

Jump to bottom

Workaround fix for summation-kernel-0 after Viper update #117

Closed
wytseoortwijn opened this issue Aug 23, 2018 · 4 comments
Closed

Workaround fix for summation-kernel-0 after Viper update #117

wytseoortwijn opened this issue Aug 23, 2018 · 4 comments
Labels
A-Enh Enhancement R Rewriting problem
Projects
Post-update Viper fixes Board

Comments

@wytseoortwijn
Copy link
Contributor

To fix the carp/summation-kernel-0.pvl example after the Viper update (see wytseoortwijn/vercors@aeac296), an extra (non-intuitive) lemma was used. The new version of Viper seems somewhat more strict when it comes to matrix multiplication (which is tricky anyway for SMT solvers). As an enhancement, we should try to make this example work without the auxiliary lemma.
@wytseoortwijn wytseoortwijn added the A-Enh Enhancement label Aug 23, 2018
@wytseoortwijn
Copy link
Contributor Author

Similar workarounds have been applied in wytseoortwijn/vercors@c0038ed and wytseoortwijn/vercors@02766ca.

@wytseoortwijn
Copy link
Contributor Author

The same fix is applied in summation-kernel-1.pvl (e.g. see wytseoortwijn/vercors@a34dfd8). One should also fix this example before closing this issue.

@sjcjoosten
Copy link
Contributor

We decided to contact Alex about this

HenkMulder added a commit to HenkMulder/vercors that referenced this issue Mar 5, 2019
@HenkMulder
Update examples utwente-fmt#117
8fe6202 
In the new encoding the workaround fix from utwente-fmt#117, using lemma_mult_n to aid in calculate indexes for flattened arrays, is no longer needed.
@pieter-bos pieter-bos mentioned this issue Jan 23, 2020
Closed
@pieter-bos pieter-bos added the R Rewriting problem label Jan 23, 2020
@pieter-bos pieter-bos added this to Needs Discussion in Board May 4, 2020
@pieter-bos
Copy link
Member

Seems like a pretty standard z3 NLA incompleteness thing to me.

Board automation moved this from Needs Discussion to Done Jun 14, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
A-Enh Enhancement R Rewriting problem
Projects
Board
Done
Post-update Viper fixes
  
To do
Milestone
No milestone
Development

No branches or pull requests
3 participants
@pieter-bos @wytseoortwijn @sjcjoosten