Fix the way abstract values are typed; fixes some compliance issues.

Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion).

(this commit was certified error- and warning-free by the test-and-commit script.)

1 files changed, 3 insertions, 3 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 40f838623..baf498968 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -139,9 +139,9 @@ class AbstractValueTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
     // An UnknownTypeException means that this node has no type.  For now,
-    // only abstract values are like this.  Assigning them a type in all
-    // cases is difficult, since then the parser and the SmtEngine must be
-    // more tightly coupled.
+    // only abstract values are like this---and then, only if they are created
+    // by the user and don't actually correspond to one that the SmtEngine gave
+    // them previously.
     throw UnknownTypeException(n);
   }
 };/* class AbstractValueTypeRule */