From 0522ca5e33f1262c2659aa3afc646ccfae577ffe Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 May 2018 19:12:28 -0700
Subject: [PATCH] Fix bv-abstraction check for AND with non bit-vector atoms.
 (#2024)

---
 src/theory/bv/abstraction.cpp              | 20 ++++++++++----------
 src/theory/bv/abstraction.h                |  3 +--
 test/regress/Makefile.tests                |  1 +
 test/regress/regress0/bv/bv-abstr-bug.smt2 | 16 ++++++++++++++++
 4 files changed, 28 insertions(+), 12 deletions(-)
 create mode 100644 test/regress/regress0/bv/bv-abstr-bug.smt2

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)
-- 
2.30.2