summaryrefslogtreecommitdiff
path: root/src/smt/boolean_terms.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/boolean_terms.cpp')
-rw-r--r--src/smt/boolean_terms.cpp1
1 files changed, 0 insertions, 1 deletions
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback