Correcting next_sibling_or_parent on iterators

Author: romainbrenguier

src/util/expr_iterator.h

@@ -55,7 +55,6 @@ inline bool operator==(
   const depth_iterator_expr_statet &right)
 { return left.it==right.it && left.expr.get()==right.expr.get(); }
 
-
 /// Depth first search iterator base - iterates over supplied expression
 /// and all its operands recursively.
 /// Base class using CRTP
@@ -100,14 +99,8 @@ class depth_iterator_baset
   depth_iterator_t &next_sibling_or_parent()
   {
     PRECONDITION(!m_stack.empty());
-    while(!m_stack.empty())
-    {
-      m_stack.back().it++;
-      if(m_stack.back().it==m_stack.back().end)
-        m_stack.pop_back();
-      else if(this->downcast().push_expr(*m_stack.back().it))
-        break;
-    }
+    m_stack.back().it=m_stack.back().end;
+    ++(*this);
     return this->downcast();
   }