Regression

ajreynol · Feb 20, 2025 · 9b6f165 · 9b6f165
1 parent b2223ff
commit 9b6f165
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git 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
@@ -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)