From 2520dcb04ba2661cb7ed8e433833338e25559f7f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 Dec 2022 14:03:22 -0800
Subject: [PATCH] merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .github/workflows/coverage.yml             |  2 +-
 src/ast/simplifiers/dependent_expr_state.h | 11 ++++-------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index 707db63d6..e8caa9bfb 100644
--- a/.github/workflows/coverage.yml
+++ b/.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
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index 85b6352ad..6d1f1aa77 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -116,13 +116,10 @@ protected:
     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; }
     };