Judging the project from its feature list in the README.md, it does not seem like LASER is capable of handling arbitrary invariants.