summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c0b318f23..e27d438be 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
bool MatchGen::isHandledUfTerm( TNode n ) {
return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
- n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;
+ n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
}
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback