mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix #2930

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-02 20:03:55 -08:00
parent 28c827fb69
commit 3760107bb8
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -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;