diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h index 54746489f..b83a39a1e 100644 --- a/src/ast/euf/euf_sgraph.h +++ b/src/ast/euf/euf_sgraph.h @@ -122,13 +122,6 @@ namespace euf { // register expression in both sgraph and egraph enode* mk_enode(expr* e); - snode* get_snode(expr * expr) { - snode* s = find(expr); - if (!s) - s = mk(expr); - return s; - } - sort* get_str_sort() const { return m_str_sort; } // return true if a, b are of the same length and distinct diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index db0e8fbf0..c70b03d99 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -921,7 +921,7 @@ namespace smt { // ----------------------------------------------------------------------- euf::snode* theory_nseq::get_snode(expr* e) { - return m_sgraph.get_snode(e); + return m_sgraph.mk(e); } // -----------------------------------------------------------------------