From 76ba240ee24406a4556109be60859f518b5c2a64 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 11 Mar 2026 21:25:56 +0000
Subject: [PATCH] Add sort parameter to sgraph::mk_var

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/euf/euf_sgraph.cpp  | 5 +++--
 src/ast/euf/euf_sgraph.h    | 4 +++-
 src/smt/seq/seq_nielsen.cpp | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp
index 6e8827a79..cc1228de2 100644
--- a/src/ast/euf/euf_sgraph.cpp
+++ b/src/ast/euf/euf_sgraph.cpp
@@ -450,8 +450,9 @@ namespace euf {
         m_egraph.pop(num_scopes);
     }
 
-    snode* sgraph::mk_var(symbol const& name) {
-        expr_ref e(m.mk_const(name, m_str_sort), m);
+    snode* sgraph::mk_var(symbol const& name, sort* s) {
+        if (!s) s = m_str_sort;
+        expr_ref e(m.mk_const(name, s), m);
         return mk(e);
     }
 
diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h
index 545f21c38..62c4ba67b 100644
--- a/src/ast/euf/euf_sgraph.h
+++ b/src/ast/euf/euf_sgraph.h
@@ -125,8 +125,10 @@ namespace euf {
         // register expression in both sgraph and egraph
         enode* mk_enode(expr* e);
 
+        sort* get_str_sort() const { return m_str_sort; }
+
         // factory methods for creating snodes with corresponding expressions
-        snode* mk_var(symbol const& name);
+        snode* mk_var(symbol const& name, sort* s = nullptr);
         snode* mk_char(unsigned ch);
         snode* mk_empty();
         snode* mk_concat(snode* a, snode* b);
diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index aaf08a6d4..f2529da39 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -2216,7 +2216,7 @@ namespace seq {
     euf::snode* nielsen_graph::mk_fresh_var() {
         ++m_stats.m_num_fresh_vars;
         std::string name = "v!" + std::to_string(m_fresh_cnt++);
-        return m_sg.mk_var(symbol(name.c_str()));
+        return m_sg.mk_var(symbol(name.c_str()), m_sg.get_str_sort());
     }
 
     euf::snode* nielsen_graph::mk_fresh_char_var() {