diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-12-14 01:04:00 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-12-14 01:04:00 +0000 |
| commit | 795ab3d4e6a2e75e4e6c6d795d78ef3ae3d17eeb (patch) | |
| tree | 1db680561164760f3016ddc8574e1b6278b0de58 /src/theory/uf | |
| parent | 1b48cea6ff4a6433c8a8c06c8db51fb59bf75143 (diff) | |
fix to static learning application in UF, resolves bug# 239
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/morgan/theory_uf_morgan.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index ef00b5818..cd9ee79c3 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -647,6 +647,7 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { // binary OR of binary ANDs of EQUALities if(n.getKind() == kind::OR && n.getNumChildren() == 2 && n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && + n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && |