diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-14 07:33:01 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-14 09:33:01 -0500 |
| commit | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (patch) | |
| tree | f182e942b3bc4ad99a8fdf765959781f1a2570dd /test | |
| parent | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (diff) | |
Use TypeNode in EmptySet (#4740)
This commit changes EmptySet to use TypeNode instead of Type.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/theory/theory_sets_type_enumerator_white.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 19d36614d..67a36200f 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -56,7 +56,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite Node actual0 = *setEnumerator; Node expected0 = - d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType).toType())); + d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType))); TS_ASSERT_EQUALS(expected0, actual0); TS_ASSERT(!setEnumerator.isFinished()); @@ -92,7 +92,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite Node actual0 = *setEnumerator; Node expected0 = - d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode).toType())); + d_nm->mkConst(EmptySet(d_nm->mkSetType(typeNode))); TS_ASSERT_EQUALS(expected0, actual0); TS_ASSERT(!setEnumerator.isFinished()); @@ -158,7 +158,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite Node actual0 = *setEnumerator; Node expected0 = - d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype).toType())); + d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype))); TS_ASSERT_EQUALS(expected0, actual0); TS_ASSERT(!setEnumerator.isFinished()); @@ -217,7 +217,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite Node actual0 = *setEnumerator; Node expected0 = - d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2).toType())); + d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2))); TS_ASSERT_EQUALS(expected0, actual0); TS_ASSERT(!setEnumerator.isFinished()); |