SC^2: Satisfiability Checking Meets Symbolic Computation