diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /test/unit/util | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'test/unit/util')
| -rw-r--r-- | test/unit/util/boolean_simplification_black.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index cb5e20db9..e5c18ff83 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -94,10 +94,10 @@ public: hfc = d_nm->mkNode(kind::APPLY_UF, h, fc); gfb = d_nm->mkNode(kind::APPLY_UF, g, fb); - ac = d_nm->mkNode(kind::IFF, a, c); - ffbd = d_nm->mkNode(kind::IFF, ffb, d); - efhc = d_nm->mkNode(kind::IFF, e, fhc); - dfa = d_nm->mkNode(kind::IFF, d, fa); + ac = d_nm->mkNode(kind::EQUAL, a, c); + ffbd = d_nm->mkNode(kind::EQUAL, ffb, d); + efhc = d_nm->mkNode(kind::EQUAL, e, fhc); + dfa = d_nm->mkNode(kind::EQUAL, d, fa); // this test is designed for >= 10 removal threshold TS_ASSERT_LESS_THAN_EQUALS(10u, |