Skip to content

Booster: only check the SMT prelude once, on server start #4036

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

Closed
geo2a opened this issue Aug 15, 2024 · 0 comments · Fixed by #4040
Closed

Booster: only check the SMT prelude once, on server start #4036

geo2a opened this issue Aug 15, 2024 · 0 comments · Fixed by #4040

Comments

@geo2a
Copy link
Collaborator

geo2a commented Aug 15, 2024

Booster currently issues a (check-sat) command upon sending the SMT prelude to the solver on every restart. Instead, we should do the same thing that Kore does and only check the prelude once at server start-up. On all server restarts we should just send the prelude commands, without the trailing (check-sat).

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 a pull request may close this issue.

1 participant