1455   Expr ineq1 = betaLTt.getExpr();  in normalizeProjectIneqs()  local
1460   Theorem isIntBeta(isIntegerThm(ineq1[0]));  in normalizeProjectIneqs()
1464   TRACE("arith ineq", "normalizeProjectIneqs(", ineq1,  in normalizeProjectIneqs()
1466   DebugAssert((isLE(ineq1) || isLT(ineq1)) &&  in normalizeProjectIneqs()
1469               ineq1.toString() + ineq2.toString());  in normalizeProjectIneqs()
1470   DebugAssert(!isPlus(ineq1[1]) && !isPlus(ineq2[0]),  in normalizeProjectIneqs()
1472               ineq1.toString() + ineq2.toString());  in normalizeProjectIneqs()
1477   Rational b = isMult(ineq1[1]) ? (ineq1[1])[0].getRational() : 1;  in normalizeProjectIneqs()
1520     Theorem thm2 = iffMP(betaLTt, d_rules->multIneqn(ineq1, rat(factor1)));  in normalizeProjectIneqs()
1522     ineq1 = betaLTt.getExpr();  in normalizeProjectIneqs()
1533   Expr beta(ineq1[0]);  in normalizeProjectIneqs()
1536   if(isLE(ineq1) && isLE(ineq2) && alpha == beta) {  in normalizeProjectIneqs()
1919   const Expr& ineq1(alphaLEax.getExpr());  in processFiniteInterval()  local
1921   DebugAssert(isLE(ineq1), "TheoryArith3::processFiniteInterval: ineq1 = "  in processFiniteInterval()
1922 	      +ineq1.toString());  in processFiniteInterval()
1926   if(!isInteger(ineq1[0])  in processFiniteInterval()
1927      || !isInteger(ineq1[1])  in processFiniteInterval()
1932   const Expr& ax = ineq1[1];  in processFiniteInterval()
1944     thm1 = canonPred(iffMP(alphaLEax, d_rules->multIneqn(ineq1, b)));  in processFiniteInterval()