| 1766 | } |
| 1767 | |
| 1768 | expr expr::slt(const expr &rhs) const { |
| 1769 | C(); |
| 1770 | if (rhs.isSMin()) |
| 1771 | return false; |
| 1772 | |
| 1773 | int64_t n; |
| 1774 | if (rhs.isInt(n)) |
| 1775 | return sle(mkInt(n - 1, sort())); |
| 1776 | |
| 1777 | return !rhs.sle(*this); |
| 1778 | } |
| 1779 | |
| 1780 | expr expr::sge(const expr &rhs) const { |
| 1781 | return rhs.sle(*this); |