diff options
Diffstat (limited to 'src/theory/quantifiers/macros.cpp')
| -rw-r--r-- | src/theory/quantifiers/macros.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 976b81e60..96d682a77 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -147,7 +147,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, } bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ - return pol && ( n.getKind()==EQUAL || n.getKind()==IFF ); + return pol && n.getKind()==EQUAL; } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { @@ -211,7 +211,7 @@ void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidat } Node QuantifierMacros::solveInEquality( Node n, Node lit ){ - if( lit.getKind()==IFF || lit.getKind()==EQUAL ){ + if( lit.getKind()==EQUAL ){ //return the opposite side of the equality if defined that way for( int i=0; i<2; i++ ){ if( lit[i]==n ){ |