summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-04-28 11:28:25 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-04-28 11:28:25 -0400
commitb01a91bb5690b2648a5b8d91f940a6746cba34a3 (patch)
tree9c4881ead1f7bce2bdd522765a648b6ed896d5c3 /src/theory/quantifiers/term_database.cpp
parent3fc61e7f2b84765dc547634463198b30516ed432 (diff)
parent698f5a09b1c0177abfd2eaa2b110de100fd108ef (diff)
Merge remote-tracking branch 'upstream/master' into sets
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cf183dd18..3168d21a0 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) {
}
d_par_op_map[op][tn1][tn2] = n;
return n;
- }else if( n.getKind()==APPLY_UF ){
+ }else if( inst::Trigger::isAtomicTrigger( n ) ){
return n.getOperator();
}else{
return Node::null();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback