Skip to content

solx and conclusion unsat

When using solx to exclude solutions, we are currently getting a warning "work in progress; behaviour might change", which is fine.

However, if we now exclude solutions and then later add to the conclusion "conclusion UNSAT", this is accepted by pboxide.

I would propose that either solx is "unsupported" for now, or the conclusion check is adapted to reject unsat claims of satisfiable problems where solx was used.