From bee3077640ae4de245b7563fc047fadacf5e1ab4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Aug 2020 20:13:46 -0700 Subject: [PATCH] free memory in egraph Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 4 ++-- src/sat/tactic/goal2sat.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 50b622c29e5..5715447a8e1 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -130,9 +130,9 @@ namespace euf { return n; } - void egraph::~egraph() { + egraph::~egraph() { for (enode* n : m_nodes) - n->~enode(); + n->m_parents.finalize(); } void egraph::pop(unsigned num_scopes) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index a7de8badda2..8b26587d909 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -94,7 +94,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_ite_extra = p.get_bool("ite_extra", true); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_xor_solver = p.get_bool("xor_solver", false); - m_euf = true; // false; // true; + m_euf = false; } void throw_op_not_handled(std::string const& s) {