diff options
Diffstat (limited to 'src/theory/uf/eq_proof.cpp')
| -rw-r--r-- | src/theory/uf/eq_proof.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 70675e22c..f709dce32 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -207,8 +207,8 @@ bool EqProof::foldTransitivityChildren( inSubstCase = true; Node premiseTermEq = premises[offending][termPos]; Node conclusionTermEq = conclusion[0].getKind() == kind::CONST_BOOLEAN - ? conclusion[1] - : conclusion[0]; + ? conclusion[1] + : conclusion[0]; Trace("eqproof-conv") << "EqProof::foldTransitivityChildren: Substitition " "case. Need to build subst from " << premiseTermEq << " to " << conclusionTermEq |