From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 2 Oct 2014 12:47:45 +0000 (-0400)
Subject: Fix for an array-of-record model generation assert-fail (assert was too strong).
X-Git-Tag: cvc5-1.0.0~6509^2~22
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d4a075f5154051d64d81605f023c6d6db8a6550;p=cvc5.git

Fix for an array-of-record model generation assert-fail (assert was too strong).
---

diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h
index bccefdd58..b1d624266 100644
--- a/src/util/array_store_all.h
+++ b/src/util/array_store_all.h
@@ -46,7 +46,7 @@ public:
     // because this check is done in production builds too
     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.getType().isComparableTo(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");
   }