From: Clark Barrett <barrett@cs.nyu.edu>
Date: Fri, 29 Jan 2010 22:04:43 +0000 (+0000)
Subject: one more bug
X-Git-Tag: cvc5-1.0.0~9325
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c325c978225419708e1aa4a4c99b608b38fece1;p=cvc5.git

one more bug
---

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 76cc03666..078b6a6ef 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -128,10 +128,10 @@ void ContextObj::update() {
   ContextObj* pContextObjSaved = save(d_pScope->getCMM());
 
   // Check that base class data was saved
-  Assert(saved.d_pContextObjNext == d_pContextObjNext &&
-         saved.d_ppContextObjPrev == d_ppContextObjPrev &&
-         saved.d_pContextObjRestore == d_pContextObjRestore &&
-         saved.d_pScope == d_pScope,
+  Assert(pContextObjSaved->d_pContextObjNext == d_pContextObjNext &&
+         pContextObjSaved.d_ppContextObjPrev == d_ppContextObjPrev &&
+         pContextObjSaved.d_pContextObjRestore == d_pContextObjRestore &&
+         pContextObjSaved.d_pScope == d_pScope,
          "save() did not properly copy information in base class");
 
   // Update Scope pointer to current top Scope