Removed unsat_core from solver.ml
Lots of fixes for proof generation.