ArrayStoreAll should (for now) only allow constant expressions, as it is itself a...

diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index 277422ecf7268340442966a5dab0c7cb65c3b613..7cfe2eab439f7735b82e56d4d42dc0b88e5a2a9a 100644 (file)
--- 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 915f853d6882c9e6493b580c330f946bc591375f..2c1bd959de462adc051625642bd5f6cd1486df42 100644 (file)
--- 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 */