Bug: a variable is assigned twice successively.

[ustchcs-bugfinder]

z3/src/opt/maxres.cpp

Line 293 in 8439057

m_last_index = 0;

     ...
     if (m_hill_climb) {
            /**
               Give preference to cores that have large minimal values.
            */
            sort_assumptions(asms);              
            m_last_index = std::min(m_last_index, asms.size()-1);            //assigned for the first time
            m_last_index = 0;                                                                    //assigned twice
            unsigned index = m_last_index>0?m_last_index-1:0;
            m_last_index = 0;
            bool first = index > 0;
            SASSERT(index < asms.size() || asms.empty());
            IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
            while (index < asms.size() && is_sat == l_true) {
                while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) {
                    index = next_index(asms, index);
                }
                first = false;
                m_last_index = index;
                is_sat = check_sat(index, asms.c_ptr());
            }            
        }
...

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