From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Fri, 22 Mar 2013 00:07:44 +0000 (-0400)
Subject: another typo/bugfix for equality constant evaluation
X-Git-Tag: cvc5-1.0.0~7372
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=36816ad2537a2e6163037e9592c513b9a69aa9dc;p=cvc5.git

another typo/bugfix for equality constant evaluation
---

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index b2713d420..45f161143 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -603,9 +603,9 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // If it's interpreted and we can interpret
-	if (fun.isInterpreted() && class1isConstant && !d_isInternal[funId]) {
+	if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId]) {
 	  // Get the actual term id 
-	  TNode term = d_nodes[useNode.getApplicationId()];
+	  TNode term = d_nodes[funId];
 	  subtermEvaluates(getNodeId(term));
 	}
 	// Check if there is an application with find arguments