Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques