From e21d154778de840e1268a4c612e8adea641e3568 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jun 2026 19:57:51 -0700 Subject: [PATCH] cleanup, missing case for nullable xor Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_derive.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index f87c894f6..a0f7037af 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -523,6 +523,9 @@ namespace seq { m_br.mk_not(is_nullable(r2), result); m_br.mk_and(result, is_nullable(r1), result); } + else if (re().is_xor(r, r1, r2)) { + m_br.mk_xor(is_nullable(r1), is_nullable(r2), result); + } else if (re().is_star(r) || re().is_opt(r) || re().is_full_seq(r) ||