From e94b6db8e50731a851815b4d6daf8d284c099456 Mon Sep 17 00:00:00 2001
From: CEisenhofer <clemens.eisenhofer@tuwien.ac.at>
Date: Wed, 3 Jun 2026 10:58:25 +0200
Subject: [PATCH] Removed assertion to make the build dependencies acyclic

---
 src/smt/seq/seq_nielsen.cpp |  3 ---
 src/smt/seq/seq_nielsen.h   | 19 ++++++++-----------
 2 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index 75f5fdaf4..8a81a5c59 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -35,14 +35,12 @@ NSB review:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/seq_skolem.h"
 #include "ast/rewriter/var_subst.h"
-#include "smt/smt_enode.h"
 #include "util/statistics.h"
 #include <algorithm>
 #include <complex>
 #include <cstdlib>
 #include <stack>
 #include <unordered_map>
-#include <vector>
 
 namespace seq {
 
@@ -54,7 +52,6 @@ namespace seq {
         for (dep_source const &d : vs) {
             if (std::holds_alternative<enode_pair>(d)) {
                 eqs.push_back(std::get<enode_pair>(d));
-                SASSERT(eqs.back().first->get_root() == eqs.back().second->get_root());
             }
             else if (std::holds_alternative<sat::literal>(d))
                 lits.push_back(std::get<sat::literal>(d));
diff --git a/src/smt/seq/seq_nielsen.h b/src/smt/seq/seq_nielsen.h
index fda4608e3..cbd8b2dac 100644
--- a/src/smt/seq/seq_nielsen.h
+++ b/src/smt/seq/seq_nielsen.h
@@ -232,24 +232,21 @@ Author:
 
 #pragma once
 
-#include "util/vector.h"
-#include "util/uint_set.h"
-#include "util/dependency.h"
-#include "util/map.h"
-#include "util/lbool.h"
-#include "util/rational.h"
 #include "ast/ast.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/euf/euf_sgraph.h"
-#include <map>
 #include "model/model.h"
+#include "util/lbool.h"
+#include "util/dependency.h"
+#include "util/map.h"
 #include "util/obj_ref_hashtable.h"
-#include "util/uint_map.h"
+#include "util/rational.h"
+#include "util/uint_set.h"
+#include "util/vector.h"
+#include <map>
 
-namespace smt {
-    class enode;
-}
+namespace smt { class enode; }
 
 namespace seq {