From 73486be590472ff40bfe77618c2adc4fee764126 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 11 Jun 2018 13:46:27 -0700 Subject: [PATCH] fix typo in mk_pure --- src/qe/qe_term_graph.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index b951244f3..6ea2194b7 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -78,7 +78,7 @@ namespace qe { }; class children { - term const& t; + term const& t; public: children(term const& _t):t(_t) {} children(term const* _t):t(*_t) {} @@ -628,9 +628,9 @@ namespace qe { } expr* term_graph::mk_pure(term& t) { - expr* e = t.get_expr(); - // AG: the if-statement looks wrong - if (m_term2app.find(t.get_id(), e)) e; + expr* e = nullptr; + if (m_term2app.find(t.get_id(), e)) return e; + e = t.get_expr(); if (!is_app(e)) return nullptr; app* a = ::to_app(e); expr_ref_vector kids(m); @@ -647,11 +647,11 @@ namespace qe { expr_ref_vector term_graph::project(func_decl_ref_vector const& decls, bool exclude) { u_map _decls; for (func_decl* f : decls) _decls.insert(f->get_id(), true); - // . propagate representatives up over parents. + // - propagate representatives up over parents. // use work-list + marking to propagate. - // . produce equalities over represented classes. - // . produce other literals over represented classes - // (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls) + // - produce equalities over represented classes. + // - produce other literals over represented classes + // (walk disequalities in m_lits and represent lhs/rhs over decls or excluding decls) expr_ref_vector result(m); m_term2app.reset();