summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
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 c34d86497..9f222431e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) {
bool ret = false;
if( n.getKind()==UNINTERPRETED_CONSTANT ){
ret = true;
- }else{
+ }else if( n.getKind()!=SEP_NIL ){ //sep.nil has dummy argument FIXME
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( containsUninterpretedConstant( n[i] ) ){
ret = true;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback