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/expr/node_builder.h | |
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/expr/node_builder.h')
-rw-r--r-- | src/expr/node_builder.h | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index e68873176..f6aa1920d 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1303,14 +1303,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { - try { - d_nm->getType(n, true); - } catch(UnknownTypeException&) { - // Ignore the error; this expression doesn't have a type, - // because it has an abstract value in it. If the user - // depends on the type of this expression, he should get an - // exception, but so far he's only constructed it. - } + d_nm->getType(n, true); } } } |