Bug: same conditions found. It is very likely a copy-paste bug.

[ustchcs-bugfinder]

z3/src/smt/seq_offset_eq.cpp

Line 103 in 7fc4653

!a.is_numeral(n2->get_owner()) &&

bool seq_offset_eq::find(enode* n1, enode* n2, int& offset) const {
    n1 = n1->get_root();
    n2 = n2->get_root();
    if (n1->get_owner_id() > n2->get_owner_id()) 
        std::swap(n1, n2);
    return 
        !a.is_numeral(n2->get_owner()) &&            // line 103
        !a.is_numeral(n2->get_owner()) &&            //Same as previous line 
        m_offset_equalities.find(n1, n2, offset);
}

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-2.3: LHS and RHS of a logical binary-operator (&&, ||), relational/equality binary-operator expression should not contain the same sub-expression.)