diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
| commit | 9df318ca1ab33001bd203c24ae57a8b5739b8f36 (patch) | |
| tree | 3b104cc97f5daa2f69285056d81ace0ed7c916e9 /src/theory/quantifiers/term_database.cpp | |
| parent | 458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (diff) | |
Fix some mistakes in datatypes theory combination, disable two regressions. Minor fix for fun defs.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3f6f2a6ed..392fc269a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1001,7 +1001,7 @@ Node TermDb::getRewriteRule( Node q ) { } bool TermDb::isFunDef( Node q ) { - if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF ){ + if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ if( q[2][i].getKind()==INST_ATTRIBUTE ){ if( q[2][i][0].getAttribute(FunDefAttribute()) ){ |