diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-25 21:27:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-25 21:27:17 +0000 |
commit | 3cbd118238dbe1a68c53a970169488bee2b63ae7 (patch) | |
tree | 2d334f8b36ef83d88fef580c86ff113e80cfa3c5 /test/unit/util/boolean_simplification_black.h | |
parent | 80afd586eb0865efcc38aa14833d682f1b7cc27f (diff) |
fix unit tests
Diffstat (limited to 'test/unit/util/boolean_simplification_black.h')
-rw-r--r-- | test/unit/util/boolean_simplification_black.h | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index 8dafd202e..8f2d0d97f 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -76,17 +76,17 @@ public: d_nm = new NodeManager(d_context, NULL); d_scope = new NodeManagerScope(d_nm); - a = d_nm->mkVar("a", d_nm->booleanType()); - b = d_nm->mkVar("b", d_nm->booleanType()); - c = d_nm->mkVar("c", d_nm->booleanType()); - d = d_nm->mkVar("d", d_nm->booleanType()); - e = d_nm->mkVar("e", d_nm->booleanType()); - f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->booleanType(), - d_nm->booleanType())); - g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->booleanType(), - d_nm->booleanType())); - h = d_nm->mkVar("h", d_nm->mkFunctionType(d_nm->booleanType(), - d_nm->booleanType())); + a = d_nm->mkSkolem("a", d_nm->booleanType()); + b = d_nm->mkSkolem("b", d_nm->booleanType()); + c = d_nm->mkSkolem("c", d_nm->booleanType()); + d = d_nm->mkSkolem("d", d_nm->booleanType()); + e = d_nm->mkSkolem("e", d_nm->booleanType()); + f = d_nm->mkSkolem("f", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); + g = d_nm->mkSkolem("g", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); + h = d_nm->mkSkolem("h", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); fa = d_nm->mkNode(kind::APPLY_UF, f, a); fb = d_nm->mkNode(kind::APPLY_UF, f, b); fc = d_nm->mkNode(kind::APPLY_UF, f, c); |