From 3760107bb8ff04746cff31a2a31145caab9cdf5a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Feb 2020 20:03:55 -0800 Subject: [PATCH] fix #2930 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/reduce_invertible_tactic.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 77f9f7912..22b4b3395 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -236,6 +236,7 @@ private: // TBD: could be made to be recursive, by walking multiple layers of parents. bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) { + if (m_parents.size() <= v->get_id()) return false; p = m_parents[v->get_id()].get(); if (!p) return false; if (m_inverted.is_marked(p)) return false;