Package org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper

Wrapper-classes to guarantee identical behavior for all solvers. If a solver does not support BasicProverEnvironment.isUnsatWithAssumptions(java.util.Collection<org.sosy_lab.java_smt.api.BooleanFormula>), we wrap it in a (subclass of) BasicProverWithAssumptionsWrapper, whose task it is to keep the assumptions as long on the solver's stack as no other operation accesses it. It allows computing interpolants and unsat cores. without direct support from the solver.