Searched refs:boundThm (Results 1 – 1 of 1) sorted by relevance
4687 Theorem boundThm = termLowerBoundThm[t1]; in registerAtom() local4688 Expr boundIneq = boundThm.getExpr(); in registerAtom()4690 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyWeakerInequality(boundIneq, e))); in registerAtom()4698 Theorem boundThm = termUpperBoundThm[t1]; in registerAtom() local4699 Expr boundIneq = boundThm.getExpr(); in registerAtom()4701 enqueueFact(getCommonRules()->implMP(boundThm, d_rules->implyNegatedInequality(boundIneq, e))); in registerAtom()