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

Add support for the (reset) SMTLIB command #32

Open
sy6sy2 opened this issue Jan 20, 2019 · 3 comments
Open

Add support for the (reset) SMTLIB command #32

sy6sy2 opened this issue Jan 20, 2019 · 3 comments
Assignees
@mpreiner
Labels
feature New feature or request

Comments

@sy6sy2
Copy link

sy6sy2 commented Jan 20, 2019

Hi,
Do you plan to add the support for the (reset) SMTLIB command?

According to http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf:

The new command reset brings the state of a solver to the state it had immediately after start up (resetting everything).

In my case, I have a lot of formula to check but they are not related at all. This is why I use the (reset) command with Z3 and CVC4. But with Boolector I have to kill the Boolector process and start a new one each time I want to "start a fresh session".

Thank you!
@sy6sy2 sy6sy2 changed the title Add support for the reset SMTLIB command Add support for the (reset) SMTLIB command Jan 20, 2019
@sy6sy2 sy6sy2 changed the title Add support for the (reset) SMTLIB command Add support for the (reset) SMTLIB command Jan 20, 2019
@mpreiner mpreiner self-assigned this Jan 20, 2019
@mpreiner mpreiner added the feature New feature or request label Jan 20, 2019
@mpreiner
Copy link
Member

Should be doable! We'll have a look.

@sy6sy2 sy6sy2 mentioned this issue Feb 28, 2019
Closed
@makaimann makaimann mentioned this issue Apr 1, 2019
Merged
@sy6sy2
Copy link
Author

sy6sy2 commented Aug 10, 2020

Hi, is the SMTLIBv2 (reset) support sill on the table? 😇
Thank you!

@aytey
Copy link
Contributor

aytey commented Aug 10, 2020

You might be interested in this other issue: #139 (particularly #139 (comment))

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mpreiner mpreiner

Labels
feature New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@mpreiner @sy6sy2 @aytey