From 0ff21bf1d615500ca135f36f5ec8c57c1fd47438 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 May 2013 16:54:20 -0500
Subject: [PATCH] Fix minor bug in full_model_check.cpp

---
 src/theory/quantifiers/full_model_check.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 445f0d6c0..c2a3f895b 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -163,7 +163,7 @@ void Def::simplify(FullModelChecker * m) {
   d_et.reset();
   for (unsigned i=0; i<d_status.size(); i++) {
     if( d_status[i]!=status_redundant ){
-      addEntry(m, d_cond[i], d_value[i]);
+      addEntry(m, cond[i], value[i]);
     }
   }
   d_status.clear();
-- 
2.30.2