summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/macros.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/macros.cpp')
-rw-r--r--src/theory/quantifiers/macros.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 8e1083b7b..9cd12fbfb 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -119,7 +119,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node n_op ){
}
bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){
- return pol && n.getKind()==EQUAL;//( n.getKind()==EQUAL || n.getKind()==IFF );
+ return pol && ( n.getKind()==EQUAL || n.getKind()==IFF );
}
void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback