remove an obsolete (and incorrect) assertion in boolean-terms; also add failing regre...

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 816aba8a6b450906570265c3bed6fce1b73f0510..dda9c7a3e7d1cb89a3c9dfaea6140c39f7e27f54 100644 (file)
--- 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 (file)
index 0000000..7af988e
--- /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)