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

:set smtFile doesn't work with online what4-based provers #1475

Closed
RyanGlScott opened this issue Nov 30, 2022 · 1 comment
Closed

:set smtFile doesn't work with online what4-based provers #1475

RyanGlScott opened this issue Nov 30, 2022 · 1 comment
Labels
bug Something not working correctly

Comments

@RyanGlScott
Copy link
Contributor

RyanGlScott commented Nov 30, 2022

If you run this script:

:set smtFile=a.smt2
let f (x : [2]) = take y : [10] where y = x # y
:set prover=w4-z3
:sat \x -> f x == zero

With:

$ ~/Software/cryptol-2.13.0/bin/cryptol -b a.icry

Then despite having set smtFile=a.smt2, no a.smt2 file will be created. Note that a.smt2 will be created if you change prover to sbv-z3 or w4-z3, however, suggesting an inconsistency in the online what4 backend.

@RyanGlScott RyanGlScott added the bug Something not working correctly label Nov 30, 2022
RyanGlScott added a commit that referenced this issue Nov 30, 2022
This cargo-cults the existing code for making the offline `what4` backend and
uses it in the online `what4` backend, thereby fixing #1475. After this patch,
the test case in #1475 now produces an `.smt2` file, as expected.
RyanGlScott added a commit that referenced this issue Dec 1, 2022
This cargo-cults the existing code for making the offline `what4` backend and
uses it in the online `what4` backend, thereby fixing #1475. After this patch,
the test case in #1475 now produces an `.smt2` file, as expected.
RyanGlScott added a commit that referenced this issue Dec 3, 2022
This passes the value of `smtFile` to each call to `startSolverProcess` in the
online `what4` backend, thereby fixing #1475. After this patch, the test case
in #1475 now produces an `.smt2` file, as expected.
RyanGlScott added a commit that referenced this issue Dec 17, 2022
This passes the value of `smtFile` to each call to `startSolverProcess` in the
online `what4` backend, thereby fixing #1475. After this patch, the test case
in #1475 now produces an `.smt2` file, as expected.
@RyanGlScott
Copy link
Contributor Author

Fixed in #1476.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly
Projects
None yet
Development

No branches or pull requests

1 participant