From 9b6f16544e18fd4c132d70cb72f24286dca35e49 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Feb 2025 17:16:29 -0600
Subject: [PATCH] Regression

---
 test/regress/cli/CMakeLists.txt                  |  1 +
 test/regress/cli/regress0/bv/macro-rewrites.smt2 | 13 +++++++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 test/regress/cli/regress0/bv/macro-rewrites.smt2

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index f8619cc2cd6..6003972ccdf 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -618,6 +618,7 @@ set(regress_0_tests
   regress0/bv/issue9519.smt2
   regress0/bv/issue10057.smt2
   regress0/bv/le-elim-conv.smt2
+  regress0/bv/macro-rewrites.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
diff --git a/test/regress/cli/regress0/bv/macro-rewrites.smt2 b/test/regress/cli/regress0/bv/macro-rewrites.smt2
new file mode 100644
index 00000000000..ab2d1a48ca4
--- /dev/null
+++ b/test/regress/cli/regress0/bv/macro-rewrites.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(declare-const z (_ BitVec 8))
+(assert (or
+
+(not (= (concat y #b0 #b0 #b0 #b0 #b0 #b0 #b0 #b0 x) (concat y #b00000000 x)))
+(not (= (concat y ((_ extract 7 7) x) ((_ extract 6 6) x) ((_ extract 5 5) x) ((_ extract 4 4) x) ((_ extract 3 3) x) ((_ extract 2 2) x) ((_ extract 1 1) x) ((_ extract 0 0) x)) (concat y x)))
+(not (= (bvxor (bvxor x #b10101010) y z) (bvxor x #b10101010 y z)))
+
+))
+(check-sat)