From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 May 2013 21:54:20 +0000 (-0500)
Subject: Fix minor bug in full_model_check.cpp
X-Git-Tag: cvc5-1.0.0~7287^2~113^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ff21bf1d615500ca135f36f5ec8c57c1fd47438;p=cvc5.git

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 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();