SMT in Practice: the Alt-Ergo System