Fix bug 787.

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 3fd333cc5735de098cc012146f6478d94b0ab12f..87db183e29f338e7bbc77365c9d618365122c5ff 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -155,7 +155,8 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     inQuant = true;
   }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && 
             node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && 
-            node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){
+            node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && 
+            node.getKind()!=kind::BITVECTOR_EAGER_ATOM ){
     // Remember if we're inside a term
     Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl;
     inTerm = true;

diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index da537bdae0b52aa53788231a66b3871472e7e85c..4ff7f8530fdbe914557f51437d198472a017b296 100644 (file)
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -119,7 +119,8 @@ BUG_TESTS = \
        bug440.smt \
        bug733.smt2 \
        bug734.smt2 \
-       bug_extract_mult_leading_bit.smt2
+       bug_extract_mult_leading_bit.smt2 \
+       bug787.smt2
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 

diff --git a/test/regress/regress0/bv/bug787.smt2 b/test/regress/regress0/bv/bug787.smt2
new file mode 100644 (file)
index 0000000..8e0ba00
--- /dev/null
+++ b/test/regress/regress0/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)
+