Towards an Effective Decision Procedure for LTL formulas with Constraints