Searched refs:boundIneq (Results 1 – 1 of 1) sorted by relevance
4688 Expr boundIneq = boundThm.getExpr(); in registerAtom() local4689 … if (boundValue > c1 || (boundValue == c1 && !(boundIneq.getKind() == LE && e.getKind() == LT))) { in registerAtom()4690 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyWeakerInequality(boundIneq, e))); in registerAtom()4699 Expr boundIneq = boundThm.getExpr(); in registerAtom() local4700 if (boundValue < c1 || (boundValue == c1 && boundIneq.getKind() == LT && e.getKind() == LT)) { in registerAtom()4701 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyNegatedInequality(boundIneq, e))); in registerAtom()