diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-17 07:22:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-17 07:22:35 +0000 |
commit | b77f44a6975e6bab468c774d7b34c23e84371ff1 (patch) | |
tree | 2673500e6d0ec64686210f1c572b81a05cbe2707 | |
parent | 21102d14767364c222f1e7fe13de1f229d541dbc (diff) |
fix improper CongruenceClosureWhite test by merging from a uf branch; fixes the nightly test failure
-rw-r--r-- | test/unit/util/congruence_closure_white.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index 273f9cfa5..29a104a8e 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -348,11 +348,11 @@ public: d_cc->addTerm(gfafb); d_cc->addTerm(gba); + d_cc->addTerm(gfaa); d_cc->addTerm(hfaa); d_cc->addEquality(a_eq_fb); d_cc->addEquality(fa_eq_b); - d_cc->addEquality(h_eq_g); TS_ASSERT(d_cc->areCongruent(a, fb)); TS_ASSERT(d_cc->areCongruent(b, fa)); @@ -376,12 +376,11 @@ public: TS_ASSERT(d_out->areCongruent(gfafb, gba)); TS_ASSERT(d_cc->areCongruent(b, fa)); - TS_ASSERT(d_cc->areCongruent(gfafb, hba)); TS_ASSERT(d_cc->areCongruent(gfafb, gba)); - TS_ASSERT(d_cc->areCongruent(hba, gba)); + TS_ASSERT(d_cc->areCongruent(hba, hba)); TS_ASSERT(d_cc->areCongruent(hfaa, hba)); - TS_ASSERT(d_out->areCongruent(hfaa, gba));// fails due to problem with care lists - TS_ASSERT(d_cc->areCongruent(hfaa, gba)); + TS_ASSERT(d_out->areCongruent(gfaa, gba)); + TS_ASSERT(d_cc->areCongruent(gfaa, gba)); } catch(Exception e) { cout << "\n\n" << e << "\n\n"; |