From a79a48ed2a5fba07bca3620037350ec649e7955e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Mar 2026 20:16:07 -0700 Subject: [PATCH] add comment about fresh variable Signed-off-by: Nikolaj Bjorner --- src/smt/seq/seq_nielsen.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index f16c0a6df..4ed0e4583 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -3147,6 +3147,8 @@ namespace seq { euf::snode* v1 = m_sg.drop_right(eq.m_rhs, rhs_toks.size() - j); euf::snode* v2 = m_sg.drop_left(eq.m_rhs, j); euf::snode* x = mk_fresh_var(eq.m_lhs->get_sort()); + // TODO: x = m_sk.mk(symbol("signature-split"), + // eq.m_lhs->get_expr(), eq.m_rhs->get_expr(), eq.m_lhs->get_sort()); for (unsigned branch = 0; branch < 2; ++branch) { nielsen_node* child = mk_child(node);