CODEWITHSUNDEEP
z3smt
S. Nabil
S. Nabil

Reputation: 319

Unsatisfiable Assumptions in Z3?

According to the SMTLib doc here, we can check sat using check-sat-assuming and then one can determine the unsatisfiable assumptions using get-unsat-assumptions.

Reflecting that on Z3 in JavaAPI, I can see checkAssuming API doing the same thing as thecheck-sat-assuming but I can't seem to find anything that is doing something similar to get-unsat-assumptions, all I can find is getUnsatCore api.

So my question is, is there anyway that I can get unsat assumptions in Z3 using JavaAPI?

Much appreciated!

Upvotes: 4

Views: 248

Answers (1)

alias
alias

Reputation: 30475

Looks like an oversight in the Java API. You might want to file a ticket (or better yet a pull-request) at their github site: https://github.com/Z3Prover/z3/issues

Upvotes: 1

Related Questions