diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 14:36:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 14:36:14 +0000 |
commit | ec29471e427bf25034a93c182b424730d439a90a (patch) | |
tree | f4ddc215f2e78b72fdff2fa62fc8561b7dec84be /src/theory/builtin | |
parent | 265765c9f5c35c4b65934e574dbfabab97b15f7a (diff) |
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.)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 6 |
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 */ |