diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:17:14 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:17:28 -0400 |
| commit | f43c1dd87db36cf212b8bdacdf92b872df3839e6 (patch) | |
| tree | 2894db416c7f3f5f22b59d3ef0c17b4131bd52d8 /test/unit/util | |
| parent | 2c8a7a32b9694f6b1f3da1f9fa577ff94e35fb78 (diff) | |
Fix unit test for ArrayStoreAll.
Diffstat (limited to 'test/unit/util')
| -rw-r--r-- | test/unit/util/array_store_all_black.h | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index ea7b89191..433dd7601 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -55,9 +55,7 @@ public: TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))) ); TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))) ); - TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException ); TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), IllegalArgumentException ); - TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->realType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException ); } void testConstError() { |