Override math functions with uninterpreted ones

This mitigates the timeouts we were experiencing
with CVC4.