From ca3c6c4842f122641c4bb5096e6c9249db2ff12b Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 1 Dec 2012 16:41:09 +0000
Subject: [PATCH] Throw a logic exception if user makes an assertion using a
 STORE_ALL

---
 src/theory/arrays/theory_arrays.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f4661c389..a05d30517 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -24,6 +24,7 @@
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
 #include "theory/arrays/options.h"
+#include "smt/logic_exception.h"
 
 
 using namespace std;
@@ -456,6 +457,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     checkStore(node);
     break;
   }
+  case kind::STORE_ALL: {
+    throw LogicException("Array theory solver does not yet support assertions using constant array value");
+  }    
   default:
     // Variables etc
     if (node.getType().isArray()) {
-- 
2.30.2