From 7c80c3b3aa2c88a329224623c6b4dd435a9b4b2e Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 14 Mar 2026 18:32:12 +0000
Subject: [PATCH] move seq_model from smt/seq/ to smt/; fix seq_state.h
 add_str_mem typo

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/CMakeLists.txt          | 1 +
 src/smt/seq/CMakeLists.txt      | 1 -
 src/smt/seq/seq_state.h         | 2 +-
 src/smt/{seq => }/seq_model.cpp | 3 ++-
 src/smt/{seq => }/seq_model.h   | 0
 src/smt/theory_nseq.h           | 2 +-
 6 files changed, 5 insertions(+), 4 deletions(-)
 rename src/smt/{seq => }/seq_model.cpp (99%)
 rename src/smt/{seq => }/seq_model.h (100%)

diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 538b7d224..00072f4e3 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -65,6 +65,7 @@ z3_add_component(smt
     theory_intblast.cpp
     theory_lra.cpp
     theory_nseq.cpp
+    seq_model.cpp
     theory_opt.cpp
     theory_pb.cpp
     theory_recfun.cpp
diff --git a/src/smt/seq/CMakeLists.txt b/src/smt/seq/CMakeLists.txt
index afc5bcdd8..d05d2c9af 100644
--- a/src/smt/seq/CMakeLists.txt
+++ b/src/smt/seq/CMakeLists.txt
@@ -2,7 +2,6 @@ z3_add_component(smt_seq
   SOURCES
     seq_regex.cpp
     seq_state.cpp
-    seq_model.cpp
     seq_parikh.cpp
     seq_nielsen.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/smt/seq/seq_state.h b/src/smt/seq/seq_state.h
index 30574bee7..29ace6308 100644
--- a/src/smt/seq/seq_state.h
+++ b/src/smt/seq/seq_state.h
@@ -83,7 +83,7 @@ namespace smt {
             m_eq_sources.push_back({n1, n2});
         }
 
-        void add_str_mem(euf::snode* str, euf::snode* regex, sat:literal lit) {
+        void add_str_mem(euf::snode* str, euf::snode* regex, sat::literal lit) {
             seq::dep_tracker dep;
             m_str_mems.push_back(seq::str_mem(str, regex, nullptr, m_next_mem_id++, dep));
             m_mem_sources.push_back({lit});
diff --git a/src/smt/seq/seq_model.cpp b/src/smt/seq_model.cpp
similarity index 99%
rename from src/smt/seq/seq_model.cpp
rename to src/smt/seq_model.cpp
index 951039928..7177ec05f 100644
--- a/src/smt/seq/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -16,9 +16,10 @@ Author:
     Nikolaj Bjorner (nbjorner) 2026-03-01
 
 --*/
-#include "smt/seq/seq_model.h"
+#include "smt/seq_model.h"
 #include "smt/seq/seq_regex.h"
 #include "smt/seq/seq_state.h"
+#include "smt/smt_context.h"
 #include "smt/smt_model_generator.h"
 #include "smt/proto_model/proto_model.h"
 #include "ast/ast_pp.h"
diff --git a/src/smt/seq/seq_model.h b/src/smt/seq_model.h
similarity index 100%
rename from src/smt/seq/seq_model.h
rename to src/smt/seq_model.h
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index b581235c1..d44c6d67c 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -27,7 +27,7 @@ Author:
 #include "smt/seq/seq_nielsen.h"
 #include "smt/seq/seq_state.h"
 #include "smt/seq/seq_regex.h"
-#include "smt/seq/seq_model.h"
+#include "smt/seq_model.h"
 #include "smt/nseq_context_solver.h"
 
 namespace smt {