mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

free memory in egraph

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-30 20:13:46 -07:00
parent a003af494b
commit bee3077640
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/euf/euf_egraph.cpp
View file

@ -130,9 +130,9 @@ namespace euf {
return n; return n;
} }
void egraph::~egraph() { egraph::~egraph() {
for (enode* n : m_nodes) for (enode* n : m_nodes)
n->~enode(); n->m_parents.finalize();
} }
void egraph::pop(unsigned num_scopes) { void egraph::pop(unsigned num_scopes) {

2
src/sat/tactic/goal2sat.cpp
View file

@ -94,7 +94,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_ite_extra = p.get_bool("ite_extra", true); m_ite_extra = p.get_bool("ite_extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_xor_solver = p.get_bool("xor_solver", false); 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) { void throw_op_not_handled(std::string const& s) {