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

Solving under Assumptions with SMTInterpol #70

Open
PhilippWendler opened this issue Jul 28, 2016 · 11 comments
Open

Solving under Assumptions with SMTInterpol #70

PhilippWendler opened this issue Jul 28, 2016 · 11 comments
Assignees
Labels
Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver SMTInterpol solver

Comments

@PhilippWendler
Copy link
Member

ultimate-pa/smtinterpol#23 seems to add solving under assumptions for SMTInterpol, so JavaSMT should make use of it. It even seems to support what we call unsatCoreOverAssumptions (with get-unsat-assumptions).

@cheshire cheshire self-assigned this Jul 28, 2016
@cheshire
Copy link
Member

OK, I'll take care of this.

@cheshire
Copy link
Member

cheshire commented Aug 8, 2016

@PhilippWendler yet it's on a branch, so I can't do anything now.

@PhilippWendler
Copy link
Member Author

This could be done now.

@cheshire
Copy link
Member

cheshire commented Sep 8, 2016

Great, I'll take a look.

On Thu, Sep 8, 2016 at 2:58 PM, Philipp Wendler [email protected]
wrote:

This could be done now.


You are receiving this because you were assigned.
Reply to this email directly, view it on GitHub
#70 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AAVTHzYvR7gi0P-hwbKo_rgdun5uzbKfks5qoAZbgaJpZM4JW7vg
.

@PhilippWendler
Copy link
Member Author

I think this should be done now when changes for assumptions are worked on anyway.

@PhilippWendler PhilippWendler added this to the Release 2.0 milestone Mar 9, 2017
@cheshire
Copy link
Member

cheshire commented Mar 9, 2017

Unfortunately, SMTInterpol seems to loop on simple problems which we have in tests. I'll add a ticket on their issue tracker.

@cheshire
Copy link
Member

cheshire commented Mar 9, 2017

Currently blocked by ultimate-pa/smtinterpol#27

@cheshire cheshire added the Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver label Mar 9, 2017
@cheshire
Copy link
Member

cheshire commented Mar 9, 2017

Fixed in a branch in 3aea034

@cheshire cheshire removed this from the Release 2.0 milestone Mar 9, 2017
@PhilippWendler
Copy link
Member Author

Fixed in SMTInterpol: ultimate-pa/smtinterpol#27

@PhilippWendler PhilippWendler removed the Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver label Feb 27, 2018
@kfriedberger
Copy link
Member

kfriedberger commented Mar 12, 2018

Blocked by

@PhilippWendler PhilippWendler added the Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver label Mar 12, 2018
@kfriedberger
Copy link
Member

Current status:
The support in SMTInterpol for solving with assumptions is very weak.
There are many exceptions, and most of them are reported (for some time now) without an available fix.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Blocked by Solver Support solver does not yet support this feature OR there was not yet any public release of the solver SMTInterpol solver
Development

No branches or pull requests

3 participants