Fix minor bug in full_model_check.cpp

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 445f0d6c0ed6a1de261e4cd82181ac18b6cefa9a..c2a3f895b76431b4b6b6a3195da87a419be4a9d4 100755 (executable)
--- 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();\r
   for (unsigned i=0; i<d_status.size(); i++) {\r
     if( d_status[i]!=status_redundant ){\r
-      addEntry(m, d_cond[i], d_value[i]);\r
+      addEntry(m, cond[i], value[i]);\r
     }\r
   }\r
   d_status.clear();\r