diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:18:41 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-03 11:18:41 -0400 |
| commit | 3a29fafdb098d82ba56cdc02af7f1b0981a74d02 (patch) | |
| tree | d428d31fa37ce9271f6ad6220e403d9daddc9e52 /test/unit | |
| parent | e6e4bf1f11e0c09a8fd414aa4f91e9bbe3eb19cd (diff) | |
| parent | f43c1dd87db36cf212b8bdacdf92b872df3839e6 (diff) | |
Merge branch '1.4.x'
Diffstat (limited to 'test/unit')
| -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() { |