witness-solver