From 95dc44b409a0bd6c26af6ae462ae0ad255cdc049 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Apr 2026 15:51:15 -0700
Subject: [PATCH] bugfix, better debug display of failure

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq/seq_nielsen.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp
index c213bb4df..357957449 100644
--- a/src/smt/seq/seq_nielsen.cpp
+++ b/src/smt/seq/seq_nielsen.cpp
@@ -1458,6 +1458,7 @@ namespace seq {
             if (!ext) {
                 node->to_html(std::cout, m);
                 std::cout << std::endl;
+                display(std::cout, node);
             }
             VERIFY(ext);
             node->set_extended(true);
@@ -1801,6 +1802,7 @@ namespace seq {
             // → deterministically substitute x → t throughout the node
             euf::snode* var = nullptr;
             euf::snode* def;
+
             if (l->is_var() && !snode_contains_var(r, l)) {
                 var = l;
                 def = r;
@@ -1813,7 +1815,7 @@ namespace seq {
                 var = l->arg(0);
                 def = r->arg(0);
             }
-            else if (r->is_unit() && r->arg(0)->is_var() && r->is_char_or_unit()) {
+            else if (r->is_unit() && r->arg(0)->is_var() && l->is_char_or_unit()) {
                 var = r->arg(0);
                 def = l->arg(0);
             }