merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

.github/workflows/coverage.yml

@@ -58,7 +58,7 @@ jobs:
 
     - name: Run examples
       run: |
-        ${{github.workspace}}/build/examples/c_example_build_dir/c_example
+# Disabled:       ${{github.workspace}}/build/examples/c_example_build_dir/c_example
         ${{github.workspace}}/build/examples/cpp_example_build_dir/cpp_example
         ${{github.workspace}}/build/examples/tptp_build_dir/z3_tptp5 --help
         ${{github.workspace}}/build/examples/c_maxsat_example_build_dir/c_maxsat_example ${{github.workspace}}/examples/maxsat/ex.smt

src/ast/simplifiers/dependent_expr_state.h

@@ -116,13 +116,10 @@ class dependent_expr_simplifier {
     unsigned qtail() const { return m_fmls.qtail(); }
     struct iterator {
         dependent_expr_simplifier& s;
-        unsigned m_index = 0;
-        bool at_end = false;
-        unsigned index() const { return at_end ? s.qtail() : std::min(m_index, s.qtail()); }
-        iterator(dependent_expr_simplifier& s, unsigned i) : s(s), m_index(i), at_end(i == s.qtail()) {}
-        bool operator==(iterator const& other) const { return index() == other.index(); }
-        bool operator!=(iterator const& other) const { return !(*this == other); }
-        iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent()) at_end = true; else ++m_index; return *this; }
+        unsigned m_index, m_end;
+        iterator(dependent_expr_simplifier& s, unsigned i, unsigned end) : s(s), m_index(i), m_end(end) {}
+        bool operator!=(iterator const& other) const { return m_index != other.m_index; }
+        iterator& operator++() { if (!s.m.inc() || s.m_fmls.inconsistent() || m_index > s.qtail()) m_index = m_end; else ++m_index; return *this; }
         unsigned operator*() const { return m_index; }
     };