Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.

1 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 48aee1c35..d4a1e5ca4 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1206,12 +1206,12 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Node a = d_nodes[currentNode];
               Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
 
-              if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
-                d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
-                                                                              equalities, eqpc);
-              }
-
               if (eqpc) {
+                //apply proof reconstruction processing (when eqpc is non-null)
+                if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
+                  d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
+                                                                                equalities, eqpc);
+                }
                 if (reasonType == MERGED_THROUGH_EQUALITY) {
                   eqpc->d_node = reason;
                 } else {