From a302c2f15ee0e4d24ce9036050fffd8e827fe053 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 11 Dec 2022 15:21:23 +0000 Subject: [PATCH] fix crashes in elim-uncnstr2 This would crash before: (declare-fun x () (_ BitVec 4)) (assert (not (bvule x #x1))) (apply elim-uncnstr2) That's because the index_set iterator was querying qtail to compute the end of the iteration But the problem is that elim-uncnstr2 may add new fmls to the goal, as in this case. The bvule is replaced with an 'or', but since it's negated, it turns into 2 goals Solve the issue by freezing the qtail for the iteration loop. This is the right behavior for elim-uncnstr2, as it can't rewrite exprs that haven't been analyzed before @NikolajBjorner please check if this the right behavior for the other simplifiers. Thank you --- src/ast/simplifiers/dependent_expr_state.h | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 85b6352ad..f9faee549 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -116,20 +116,17 @@ 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 = m_end; else ++m_index; return *this; } unsigned operator*() const { return m_index; } }; struct index_set { dependent_expr_simplifier& s; - iterator begin() { return iterator(s, s.qhead()); } - iterator end() { return iterator(s, s.qtail()); } + iterator begin() { return iterator(s, s.qhead(), s.qtail()); } + iterator end() { return iterator(s, s.qtail(), s.qtail()); } index_set(dependent_expr_simplifier& s) : s(s) {} };