Clause Sharing and Partitioning for Cloud-Based SMT Solving