diff options
| -rw-r--r-- | src/util/array_store_all.h | 1 | ||||
| -rw-r--r-- | test/unit/util/array_store_all_black.h | 8 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h index 277422ecf..7cfe2eab4 100644 --- a/src/util/array_store_all.h +++ b/src/util/array_store_all.h @@ -49,6 +49,7 @@ public: CheckArgument(type.isArray(), type, "array store-all constants can only be created for array types, not `%s'", type.toString().c_str()); CheckArgument(expr.getType().isSubtypeOf(type.getConstituentType()), expr, "expr type `%s' does not match constituent type of array type `%s'", expr.getType().toString().c_str(), type.toString().c_str()); + CheckArgument(expr.isConst(), expr, "ArrayStoreAll requires a constant expression"); } ~ArrayStoreAll() throw() { diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 915f853d6..2c1bd959d 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -47,7 +47,6 @@ public: void testStoreAll() { Type usort = d_em->mkSort("U"); ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), d_em->mkConst(Rational(9, 2))); - ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)); ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkConst(UninterpretedConstant(usort, 0))); ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), d_em->mkConst(Rational(0))); ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), d_em->mkConst(Rational(0))); @@ -63,4 +62,11 @@ public: TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->realType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException ); } + void testConstError() { + Type usort = d_em->mkSort("U"); + TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)) ); + TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkVar("x", d_em->integerType())) ); + TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), d_em->mkConst(Rational(0)))) ); + } + };/* class ArrayStoreAllBlack */ |