text: Over the last decade , a variety of SMT algorithms have been built and empirically tested whereas little is known about the computational complexity of some of the fundamental [[ problems ]] of << SMT >> .