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.

Sign up for GitHub

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

Better ways to identify problematic Cryptol/SAWCore terms #1674

Open
robdockins opened this issue May 23, 2022 · 0 comments
Open

Better ways to identify problematic Cryptol/SAWCore terms #1674

robdockins opened this issue May 23, 2022 · 0 comments
Labels
type: enhancement Issues describing an improvement to an existing feature or capability usability An issue that impedes efficient understanding and use

Comments

@robdockins
Copy link
Contributor

In the middle of doing a proof, I had a problem where SAW would spin off and consume all available memory while preparing to submit a query to a solver. I believed that I had asked SAW to hold uninterpreted all the terms that would cause such problems, but I had missed one. I had to add trace-level debugging to the system to discover what subterm was causing the problem.

We should find some way to provide users with more feedback about what terms are being evaluated to help solve problems like this.
@robdockins robdockins added the type: enhancement Issues describing an improvement to an existing feature or capability label May 23, 2022
@yav yav added the usability An issue that impedes efficient understanding and use label Jun 6, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
type: enhancement Issues describing an improvement to an existing feature or capability usability An issue that impedes efficient understanding and use
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@yav @robdockins