SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer