Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)

4 files changed, 28 insertions, 12 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index c04e8bde9..46ccc4c3d 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -36,13 +36,14 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
 
   TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime);
 
+  TNodeSet seen;
   for (unsigned i = 0; i < assertions.size(); ++i)
   {
     if (assertions[i].getKind() == kind::OR)
     {
       for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j)
       {
-        if (!isConjunctionOfAtoms(assertions[i][j]))
+        if (!isConjunctionOfAtoms(assertions[i][j], seen))
         {
           continue;
         }
@@ -107,25 +108,24 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
   return d_funcToSignature.size() != 0;
 }
 
-bool AbstractionModule::isConjunctionOfAtoms(TNode node) {
-  TNodeSet seen;
-  return isConjunctionOfAtomsRec(node, seen);
-}
-
-bool AbstractionModule::isConjunctionOfAtomsRec(TNode node, TNodeSet& seen) {
+bool AbstractionModule::isConjunctionOfAtoms(TNode node, TNodeSet& seen)
+{
   if (seen.find(node)!= seen.end())
     return true;
 
-  if (!node.getType().isBitVector()) {
-    return (node.getKind() == kind::AND || utils::isBVPredicate(node));
+  if (!node.getType().isBitVector() && node.getKind() != kind::AND)
+  {
+    return utils::isBVPredicate(node);
   }
 
   if (node.getNumChildren() == 0)
     return true;
 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-    if (!isConjunctionOfAtomsRec(node[i], seen))
+    if (!isConjunctionOfAtoms(node[i], seen))
+    {
       return false;
+    }
   }
   seen.insert(node);
   return true;
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 0d7e0ff2a..cc78a550a 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -155,8 +155,7 @@ class AbstractionModule {
   Node abstractSignatures(TNode assertion);
   Node computeSignature(TNode node);
 
-  bool isConjunctionOfAtoms(TNode node);
-  bool isConjunctionOfAtomsRec(TNode node, TNodeSet& seen);
+  bool isConjunctionOfAtoms(TNode node, TNodeSet& seen);
 
   TNode getGeneralization(TNode term);
   void storeGeneralization(TNode s, TNode t);
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 36f0d945e..b92acab94 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -160,6 +160,7 @@ REG0_TESTS = \
 	regress0/bv/bug440.smt \
 	regress0/bv/bug733.smt2 \
 	regress0/bv/bug734.smt2 \
+	regress0/bv/bv-abstr-bug.smt2 \
 	regress0/bv/bv-int-collapse1.smt2 \
 	regress0/bv/bv-int-collapse2.smt2 \
 	regress0/bv/bv-options1.smt2 \
diff --git a/test/regress/regress0/bv/bv-abstr-bug.smt2 b/test/regress/regress0/bv/bv-abstr-bug.smt2
new file mode 100644
index 000000000..745996cb7
--- /dev/null
+++ b/test/regress/regress0/bv/bv-abstr-bug.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --bv-abstraction --bitblast=eager --no-check-models
+;
+; BV-abstraction should not be applied
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+(assert
+ (or
+  (and a b)
+  (and c d)
+ )
+)
+(check-sat)