semantic explain test
changed smt solver api signature, not very clean in existing solvers, feeding back explanations back to sat solver (needs testing)