Bug: a variable is assigned twice successively.

[ustchcs-bugfinder]

z3/src/ast/rewriter/hoist_rewriter.cpp

Line 158 in 7fc4653

v = m_uf2.mk_var();

unsigned hoist_rewriter::mk_var(expr* e) {
    unsigned v = 0;
    if (m_expr2var.find(e, v)) {
        return v;
    }
    v = m_uf1.mk_var();                       // v is assigned fore the first time here.
    v = m_uf2.mk_var();                       // v is assigned fore the second time here.
    SASSERT(v == m_var2expr.size());
    m_expr2var.insert(e, v);
    m_var2expr.push_back(e);
    return v;
}

Reported by: USTCHCS Analysis Toolsuite Bugfinder
(bugfinder-2.7: A variable should not be assigned values twice successively.)