13. Using SMT solversΒΆ