Override math functions with uninterpreted ones

This mitigates the timeouts we were experiencing
with CVC4.
Merge branch 'master' into llvm-trunk