summaryrefslogtreecommitdiff
path: root/src/parser/parser.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-05-17 09:54:15 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-05-20 16:54:27 -0400
commitfdd15f6e418277e471e92a8a32f1e2229c3325f5 (patch)
treea74941b10c39d703eedccd7ac46b89e6747112e7 /src/parser/parser.h
parentdee8aad2f6e54738ad26266618ae71d98e31aa54 (diff)
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places
Thanks to David Cok for reporting these issues.
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r--src/parser/parser.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 1ca56dc06..d13fbf2d6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -482,6 +482,7 @@ public:
}
}
+ inline size_t scopeLevel() const { return d_symtab->getLevel(); }
inline void pushScope() { d_symtab->pushScope(); }
inline void popScope() { d_symtab->popScope(); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback