From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 1 Dec 2012 12:42:18 +0000 (+0000)
Subject: remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regre... 
X-Git-Tag: cvc5-1.0.0~7493
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=557d4c2d3dd0f9f0210b9438c952903635248357;p=cvc5.git

remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regression for bug 472
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 816aba8a6..dda9c7a3e 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -121,7 +121,6 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
   }
 
   if(mk == kind::metakind::CONSTANT) {
-    Assert(k != kind::STORE_ALL, "array store-all not yet supported by Boolean-term conversion");
     return top;
   } else if(mk == kind::metakind::VARIABLE) {
     TypeNode t = top.getType();
diff --git a/test/regress/regress0/bug472.smt2 b/test/regress/regress0/bug472.smt2
new file mode 100644
index 000000000..7af988ec3
--- /dev/null
+++ b/test/regress/regress0/bug472.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_AUFLIA)
+(set-option :produce-models true)
+(declare-fun a () (Array Int Int))
+(assert (= (select a 0) 0))
+(check-sat)
+(get-value (a))
+(assert (= a @1))
+(check-sat)