From: Clark Barrett <barrett@cs.nyu.edu>
Date: Tue, 2 Feb 2010 22:40:55 +0000 (+0000)
Subject: Fixed bug in context code
X-Git-Tag: cvc5-1.0.0~9310
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=644b09baf99407e122bc8424ddb8be4b303d7166;p=cvc5.git

Fixed bug in context code
---

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 476f6d04b..a00364fe6 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -33,7 +33,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) {
 
 Context::~Context() {
   // Delete all Scopes
-  popto(-1);
+  popto(0);
 
   // Delete the memory manager
   delete d_pCMM;
@@ -99,7 +99,7 @@ void Context::pop() {
 
 void Context::popto(int toLevel) {
   // Pop scopes until there are none left or toLevel is reached
-  if (toLevel < -1) toLevel = -1;
+  if (toLevel < 0) toLevel = 0;
   while (toLevel < getLevel()) pop();
 }