Throw a logic exception if user makes an assertion using a STORE_ALL

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f4661c389806361e8963d44e1a812b9047731730..a05d30517a689560a63225d91a53facca96f8e6f 100644 (file)
--- 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()) {