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: Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)

---
 src/theory/bv/abstraction.cpp | 20 ++++++++++----------
 src/theory/bv/abstraction.h   |  3 +--
 2 files changed, 11 insertions(+), 12 deletions(-)

(limited to 'src/theory')

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);
-- 
cgit v1.2.3