projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
2c8a7a3
)
Fix unit test for ArrayStoreAll.
author
Morgan Deters
<mdeters@cs.nyu.edu>
Fri, 3 Oct 2014 15:17:14 +0000
(11:17 -0400)
committer
Morgan Deters
<mdeters@cs.nyu.edu>
Fri, 3 Oct 2014 15:17:28 +0000
(11:17 -0400)
test/unit/util/array_store_all_black.h
patch
|
blob
|
history
diff --git
a/test/unit/util/array_store_all_black.h
b/test/unit/util/array_store_all_black.h
index ea7b891912c9de6137f48894a515460af9c1db3f..433dd76015e28a414b6e118cf8b2785eb3b0b76b 100644
(file)
--- 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_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->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() {
}
void testConstError() {