From 5f92d3344def91bdfd5bf4273e8b62ad592bd2aa Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sun, 1 Mar 2026 02:35:32 +0000
Subject: [PATCH] Define eq_ref and eq_refs types in ast.h and use them in
 nseq_ne

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/ast.h             |  8 ++++++++
 src/smt/nseq_constraint.h | 20 +++++++-------------
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 7fc86070d..3cb977663 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2517,6 +2517,14 @@ typedef app_ref_vector                     proof_ref_vector;
 
 typedef ref_pair_vector<expr, ast_manager> expr_ref_pair_vector;
 
+struct eq_ref {
+    expr_ref left;
+    expr_ref right;
+    eq_ref(ast_manager& m): left(m), right(m) {}
+    eq_ref(expr_ref const& l, expr_ref const& r): left(l), right(r) {}
+    eq_ref(expr* l, expr* r, ast_manager& m): left(l, m), right(r, m) {}
+};
+using eq_refs = vector<eq_ref>;
 
 // -----------------------------------
 //
diff --git a/src/smt/nseq_constraint.h b/src/smt/nseq_constraint.h
index d12db0a76..32e4d9e73 100644
--- a/src/smt/nseq_constraint.h
+++ b/src/smt/nseq_constraint.h
@@ -60,25 +60,19 @@ namespace smt {
     // A disequality constraint: lhs != rhs
     // with decomposed sub-equations and justification literals.
     class nseq_ne {
-    public:
-        typedef std::pair<expr_ref_vector, expr_ref_vector> decomposed_eq;
-    private:
-        expr_ref                 m_lhs;
-        expr_ref                 m_rhs;
-        vector<decomposed_eq>    m_eqs;
+        eq_ref                   m_eq;
+        eq_refs                  m_eqs;
         literal_vector           m_lits;
         nseq_dependency*         m_dep;
     public:
         nseq_ne(expr_ref const& l, expr_ref const& r, nseq_dependency* dep)
-            : m_lhs(l), m_rhs(r), m_dep(dep) {
-            expr_ref_vector ls(l.get_manager()); ls.push_back(l);
-            expr_ref_vector rs(r.get_manager()); rs.push_back(r);
-            m_eqs.push_back(std::make_pair(ls, rs));
+            : m_eq(l, r), m_dep(dep) {
+            m_eqs.push_back(eq_ref(l, r));
         }
 
-        expr_ref const& l() const { return m_lhs; }
-        expr_ref const& r() const { return m_rhs; }
-        vector<decomposed_eq> const& eqs() const { return m_eqs; }
+        expr_ref const& l() const { return m_eq.left; }
+        expr_ref const& r() const { return m_eq.right; }
+        eq_refs const& eqs() const { return m_eqs; }
         literal_vector const& lits() const { return m_lits; }
         nseq_dependency* dep() const { return m_dep; }
     };