SMT-based verification of temporal properties for component-based software systems