diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-28 16:26:57 -0500 |
commit | f582b382a25463cead88bc1a46b93dd5c8099fad (patch) | |
tree | 15c54d5b5dc5b9b8a4da72a81c9ed0cf2ee6dc3d /src/theory/uf | |
parent | 358e453bda62923fd0be94af5317b24a7281014b (diff) |
Minor cleanup from last commit (quant util, equality infer). Do not set fmfBoundIntLazy for stringsExp.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 10 |
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 { |