diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 50b622c29..5715447a8 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 a7de8badd..8b26587d9 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) {