Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
	library_versions

1 files changed, 4 insertions, 4 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 0ecc6b5c7..601c251d9 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2273,7 +2273,7 @@ void ValidityChecker::popto(int stackLevel) {
 }
 
 int ValidityChecker::scopeLevel() {
-  return d_parserContext->getDeclarationLevel();
+  return d_parserContext->scopeLevel();
 }
 
 void ValidityChecker::pushScope() {
@@ -2287,12 +2287,12 @@ void ValidityChecker::popScope() {
 void ValidityChecker::poptoScope(int scopeLevel) {
   CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
                       "Cannot pop to a negative scope level %d", scopeLevel);
-  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(),
+  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
                       scopeLevel,
                       "Cannot pop to a scope level higher than the current one!  "
                       "At scope level %u, user requested scope level %d",
-                      d_parserContext->getDeclarationLevel(), scopeLevel);
-  while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) {
+                      d_parserContext->scopeLevel(), scopeLevel);
+  while(unsigned(scopeLevel) < d_parserContext->scopeLevel()) {
     popScope();
   }
 }