From f43c1dd87db36cf212b8bdacdf92b872df3839e6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 3 Oct 2014 11:17:14 -0400 Subject: [PATCH] Fix unit test for ArrayStoreAll. --- test/unit/util/array_store_all_black.h | 2 -- 1 file changed, 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() { -- 2.30.2