summaryrefslogtreecommitdiff
path: root/src/theory/arrays/kinds
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/kinds')
-rw-r--r--src/theory/arrays/kinds3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 4a8695ec4..7386ec5c2 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -44,4 +44,7 @@ typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
+# store operations that are ordered (by index) over a store-all are constant
+construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
+
endtheory
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback