- if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
- Node mp = d_match_pattern[1-i];
- Node mpo = d_match_pattern[i];
- if( mp.getKind()!=INST_CONSTANT ){
- if( i==0 ){
- if( d_match_pattern.getKind()==GEQ ){
- d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
- d_pattern = d_pattern.negate();
- }else{
- d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
- }
+ Node mp = d_match_pattern[i];
+ Node mpo = d_match_pattern[1 - i];
+ // If this side has free variables, and the other side does not or
+ // it is a free variable, then we will match on this side of the
+ // relation.
+ if (quantifiers::TermUtil::hasInstConstAttr(mp)
+ && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
+ || mpo.getKind() == INST_CONSTANT))
+ {
+ if (i == 1)
+ {
+ if (d_match_pattern.getKind() == GEQ)
+ {
+ d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
+ d_pattern = d_pattern.negate();
+ }
+ else
+ {
+ d_pattern = NodeManager::currentNM()->mkNode(
+ d_match_pattern.getKind(), mp, mpo);