From a58a9114d27aed0ba1c80999e3ab3bd428873319 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Sat, 4 Apr 2026 18:32:02 +0200
Subject: [PATCH] Fix str.< Skolem length generation overhead

---
 src/smt/theory_nseq.cpp | 3 +++
 src/smt/theory_nseq.h   | 1 -
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index 6075e23b5..b442d216e 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -175,6 +175,9 @@ namespace smt {
         // register in our private sgraph
         get_snode(term);
 
+        if (m_seq.is_seq(term) && m_axioms.sk().is_skolem(term))
+            ensure_length_var(term);
+
         // track higher-order terms for lazy unfolding
         expr* ho_f = nullptr, *ho_s = nullptr, *ho_b = nullptr, *ho_i = nullptr;
         if (m_seq.str.is_map(term, ho_f, ho_s) ||
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index 84cbeb147..615c61816 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -19,7 +19,6 @@ Author:
 --*/
 #pragma once
 
-#include <variant>
 #include "ast/seq_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "ast/rewriter/seq_axioms.h"