Skip to content

Fix SideCondition normalization error (again) #2246

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

Merged
merged 3 commits into from
Nov 10, 2020

Conversation

ttuegel
Copy link
Contributor

@ttuegel ttuegel commented Nov 6, 2020

Fixes #2244


Reviewer checklist
  • Test coverage: stack test --coverage
  • Public API documentation: stack haddock

@ttuegel
Copy link
Contributor Author

ttuegel commented Nov 6, 2020

I think we should just remove the normalization check. It doesn't appear to serve any function. The only thing we can do with the SideCondition is send it to the SMT solver, which doesn't know or care about "normalization".

The normalization check doesn't seem to serve any purpose: it is regularly
violated, and the only thing we can do with the SideCondition is send it to the
solver, which doesn't care about our definition of normalization.
@ttuegel ttuegel marked this pull request as ready for review November 9, 2020 15:08
@ttuegel ttuegel requested a review from ana-pantilie November 9, 2020 15:10
@ttuegel ttuegel merged commit 7f5571e into runtimeverification:master Nov 10, 2020
@ttuegel ttuegel deleted the issue-2244 branch November 10, 2020 17:36
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.

Error in side-condition normalization
2 participants