From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 1 Dec 2012 16:41:09 +0000 (+0000)
Subject: Throw a logic exception if user makes an assertion using a STORE_ALL
X-Git-Tag: cvc5-1.0.0~7489
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ca3c6c4842f122641c4bb5096e6c9249db2ff12b;p=cvc5.git

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 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()) {