From 9de196b3cb4f94c4bb1952b5aa4018af23ecf3c2 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Wed, 3 Jun 2026 17:39:09 +0200
Subject: [PATCH] Some signatures changed after merging in master

---
 src/smt/seq_model.cpp   | 4 ++--
 src/smt/theory_nseq.cpp | 2 +-
 src/smt/theory_nseq.h   | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/smt/seq_model.cpp b/src/smt/seq_model.cpp
index baf1146c3..840f6bffb 100644
--- a/src/smt/seq_model.cpp
+++ b/src/smt/seq_model.cpp
@@ -119,7 +119,7 @@ namespace smt {
     }
 
     model_value_proc* seq_model::mk_value(enode* n, model_generator& mg) {
-        app* e = n->get_expr();
+        expr* e = n->get_expr();
 
         if (!m_seq.is_seq(e) && !m_seq.is_re(e) && !m_seq.str.is_nth_u(e))
             return nullptr;
@@ -128,7 +128,7 @@ namespace smt {
         // Regexes are interpreted as themselves in the model.
         if (m_seq.is_re(e)) {
             m_trail.push_back(e);
-            return alloc(expr_wrapper_proc, e);
+            return alloc(expr_wrapper_proc, to_app(e));
         }
 
         // For nth_u (underspecified nth): the Nielsen character-peel /
diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp
index f94ac0651..fd528999f 100644
--- a/src/smt/theory_nseq.cpp
+++ b/src/smt/theory_nseq.cpp
@@ -577,7 +577,7 @@ namespace smt {
             m_axioms.str_to_code_axiom(n);
     }
 
-    void theory_nseq::relevant_eh(app* n) {
+    void theory_nseq::relevant_eh(expr * n) {
         if (m_seq.str.is_length(n)     ||
             m_seq.str.is_index(n)      ||
             m_seq.str.is_last_index(n) ||
diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h
index c23ebebee..09d7f35b5 100644
--- a/src/smt/theory_nseq.h
+++ b/src/smt/theory_nseq.h
@@ -119,7 +119,7 @@ namespace smt {
         void propagate() override;
         void init() override;
         void assign_eh(bool_var v, bool is_true) override;
-        void relevant_eh(app* n) override;
+        void relevant_eh(expr * n) override;
         final_check_status final_check_eh(unsigned) override;
         void push_scope_eh() override;
         void pop_scope_eh(unsigned num_scopes) override;