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 | |
| parent | e6e4bf1f11e0c09a8fd414aa4f91e9bbe3eb19cd (diff) | |
| parent | f43c1dd87db36cf212b8bdacdf92b872df3839e6 (diff) | |
Merge branch '1.4.x'
| -rw-r--r-- | AUTHORS | 9 | ||||
| -rw-r--r-- | test/unit/util/array_store_all_black.h | 2 |
2 files changed, 5 insertions, 6 deletions
@@ -2,14 +2,15 @@ The core authors and designers of CVC4 are: Kshitij Bansal <kshitij@cs.nyu.edu>, New York University Clark Barrett <barrett@cs.nyu.edu>, New York University - Francois Bobot <bobot@lri.fr>, Paris-Sud University - Christopher Conway <cconway@cs.nyu.edu>, New York University + Francois Bobot <bobot@lri.fr>, Commissariat a l'Energie Atomique (CEA) + Martin Brain <martin.brain@cs.ox.ac.uk>, University of Oxford + Christopher Conway <cconway@cs.nyu.edu>, Google Morgan Deters <mdeters@cs.nyu.edu>, New York University Liana Hadarean <lianah@cs.nyu.edu>, New York University - Dejan Jovanovic <dejan@cs.nyu.edu>, New York University + Dejan Jovanovic <dejan@cs.nyu.edu>, SRI International Tim King <taking@cs.nyu.edu>, New York University Tianyi Liang <tianyi-liang@uiowa.edu>, The University of Iowa - Andrew Reynolds <andrew.j.reynolds@gmail.com>, The University of Iowa + Andrew Reynolds <andrew.j.reynolds@gmail.com>, EPFL Cesare Tinelli <tinelli@cs.uiowa.edu>, The University of Iowa CVC4 is the fourth in the CVC series of tools (CVC, CVC Lite, CVC3) but does 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() { |