summaryrefslogtreecommitdiff
path: root/src/expr/node_builder.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_builder.h')
-rw-r--r--src/expr/node_builder.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 68655aed9..cc7e89bc8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1244,7 +1244,7 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
enabled and the current node isn't a variable or constant */
if( d_nm->getOptions()->earlyTypeChecking ) {
kind::MetaKind mk = n.getMetaKind();
- if( mk != kind::metakind::VARIABLE
+ if( mk != kind::metakind::VARIABLE
&& mk != kind::metakind::CONSTANT ) {
d_nm->getType(n, true);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback