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

prove and sat fails on proof scripts of types other than ProofScript SatResult #10

Closed
brianhuffman opened this issue May 21, 2015 · 0 comments
Closed

prove and sat fails on proof scripts of types other than ProofScript SatResult #10

brianhuffman opened this issue May 21, 2015 · 0 comments

Comments

@brianhuffman
Copy link
Contributor

The types of prove and sat indicate that they should work with any argument of type ProofScript b, but they fail in many other cases:

sawscript> prove (return ()) {{ True }}
saw: fromValue SatResult: ()

sawscript> prove assume_valid {{ True }}
WARNING: assuming goal prove is valid
saw: fromValue SatResult: Valid

sawscript> sat (return ()) {{ True }}
saw: fromValue SatResult: ()

sawscript> sat assume_valid {{ True }}
WARNING: assuming goal sat is valid
saw: fromValue SatResult: Valid
brianhuffman pushed a commit that referenced this issue Jun 1, 2015
prove(_print) and sat(_print) now require 'ProofScript SatResult' arg…
1737473 
…ument

This avoids a run-time type error, instead catching the error in the
saw-script typechecker. Fixes #10.

This is a temporary stop-gap measure: Eventually the proof commands
will change so that we can allow additional types of proof scripts.
(See issue #9.)
brianhuffman pushed a commit that referenced this issue Apr 26, 2021
@kquick
Merge pull request #10 from GaloisInc/release_2_1_0
29c2404 
Increase bounds for parameterized-utils release 2.1.0.
brianhuffman pushed a commit that referenced this issue Apr 26, 2021
@ChrisEPhifer
Merge pull request #10 from GaloisInc/fix/compm-enhancements
92ce5f6 
Move some stuff from the formal-vaccine project into the CompM module
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@brianhuffman