mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 18:08:57 +00:00
Code Activity

remove aux function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-01 19:07:37 -07:00
parent 6e8c201234
commit 2245451e96
2 changed files with 1 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/euf/euf_sgraph.h
View file

@ -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

2
src/smt/theory_nseq.cpp
View file

@ -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);
}
// -----------------------------------------------------------------------