SC2: Satisfiability checking meets symbolic computation (Project Paper)