1 files changed, 91 insertions, 0 deletions
diff --git a/test/regress/regress1/bv/bug787.smt2 b/test/regress/regress1/bv/bug787.smt2
new file mode 100644
index 000000000..8e0ba0016
--- /dev/null
+++ b/test/regress/regress1/bv/bug787.smt2
@@ -0,0 +1,91 @@
+; COMMAND-LINE: --bitblast=eager --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(set-info :status unsat)
+(define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)
+ (bvadd
+  (bvadd
+   (bvadd ((_ zero_extend 3) ((_ extract 0 0) bv))
+    ((_ zero_extend 3) ((_ extract 1 1) bv)))
+   ((_ zero_extend 3) ((_ extract 2 2) bv)))
+  ((_ zero_extend 3) ((_ extract 3 3) bv))))
+(define-fun left-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
+ (_ BitVec 4)
+ (hamming-weight (bvand bv (bvnot (bvsub (bvshl index (_ bv1 4)) (_ bv1 4))))))
+(define-fun right-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
+ (_ BitVec 4) (hamming-weight (bvand bv (bvsub index (_ bv1 4)))))
+(define-fun bit-1 ((bv (_ BitVec 4))) (_ BitVec 4) (bvand bv (bvneg bv)))
+(define-fun bit-2 ((bv (_ BitVec 4))) (_ BitVec 4)
+ (bit-1 (bvand bv (bvsub bv (_ bv1 4)))))
+(define-fun bit-3 ((bv (_ BitVec 4))) (_ BitVec 4)
+ (bit-2 (bvand bv (bvsub bv (_ bv1 4)))))
+(define-fun bit-4 ((bv (_ BitVec 4))) (_ BitVec 4)
+ (bit-3 (bvand bv (bvsub bv (_ bv1 4)))))
+(define-fun bit-5 ((bv (_ BitVec 4))) (_ BitVec 4)
+ (bit-4 (bvand bv (bvsub bv (_ bv1 4)))))
+(define-fun index-bit ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 4)
+ (ite (= index (_ bv0 4)) (bit-1 bv)
+  (ite (= index (_ bv1 4)) (bit-2 bv)
+   (ite (= index (_ bv2 4)) (bit-3 bv) (bit-4 bv)))))
+(define-fun permute
+ ((index (_ BitVec 4)) (obj-0 (_ BitVec 4)) (obj-1 (_ BitVec 4))
+  (obj-2 (_ BitVec 4)) (obj-3 (_ BitVec 4)))
+ (_ BitVec 4)
+ (let ((my-index-bit (bvshl (_ bv1 4) index)))
+  (ite (= my-index-bit obj-0) (_ bv0 4)
+   (ite (= my-index-bit obj-1) (_ bv1 4)
+    (ite (= my-index-bit obj-2) (_ bv2 4) (_ bv3 4))))))
+(define-fun left-zeros ((index (_ BitVec 4))) (_ BitVec 8)
+ (ite (bvugt index (_ bv2 4)) (ite (bvugt index (_ bv4 4)) (_ bv0 8) (_ bv1 8))
+  (ite (bvugt index (_ bv1 4)) (_ bv2 8) (_ bv3 8))))
+(define-fun centered ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 8)
+ (bvshl ((_ zero_extend 4) bv) (left-zeros index)))
+(declare-const v0 (_ BitVec 4))
+(assert (= (_ bv4 4) (hamming-weight v0)))
+(declare-const v1 (_ BitVec 4))
+(assert (= (_ bv4 4) (hamming-weight v1)))
+(declare-const vp1-0 (_ BitVec 4))
+(assert
+ (or (= (_ bv1 4) vp1-0) (= (_ bv2 4) vp1-0) (= (_ bv4 4) vp1-0)
+  (= (_ bv8 4) vp1-0)))
+(declare-const vp1-1 (_ BitVec 4))
+(assert
+ (or (= (_ bv1 4) vp1-1) (= (_ bv2 4) vp1-1) (= (_ bv4 4) vp1-1)
+  (= (_ bv8 4) vp1-1)))
+(declare-const vp1-2 (_ BitVec 4))
+(assert
+ (or (= (_ bv1 4) vp1-2) (= (_ bv2 4) vp1-2) (= (_ bv4 4) vp1-2)
+  (= (_ bv8 4) vp1-2)))
+(declare-const vp1-3 (_ BitVec 4))
+(assert
+ (or (= (_ bv1 4) vp1-3) (= (_ bv2 4) vp1-3) (= (_ bv4 4) vp1-3)
+  (= (_ bv8 4) vp1-3)))
+(assert (= (_ bv15 4) (bvor vp1-0 (bvor vp1-1 (bvor vp1-2 vp1-3)))))
+(assert
+ (and
+  (= (_ bv0 8)
+     (bvxor
+      (bvand
+       (centered (index-bit (permute (_ bv0 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
+       (centered (index-bit (_ bv0 4) v0) v0))
+      (_ bv8 8)))
+  (= (_ bv0 8)
+     (bvxor
+      (bvand
+       (centered (index-bit (permute (_ bv1 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
+       (centered (index-bit (_ bv1 4) v0) v0))
+      (_ bv8 8)))
+  (= (_ bv0 8)
+     (bvxor
+      (bvand
+       (centered (index-bit (permute (_ bv2 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
+       (centered (index-bit (_ bv2 4) v0) v0))
+      (_ bv8 8)))
+  (= (_ bv0 8)
+     (bvxor
+      (bvand
+       (centered (index-bit (permute (_ bv3 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
+       (centered (index-bit (_ bv3 4) v0) v0))
+      (_ bv8 8)))))
+(check-sat)
+