Fix BV-abstraction check to consider SKOLEM. (#2042)

Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.

5 files changed, 19 insertions, 8 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 46ccc4c3d..f0c1d5488 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -276,7 +276,7 @@ Node AbstractionModule::computeSignature(TNode node) {
 
 Node AbstractionModule::getSignatureSkolem(TNode node)
 {
-  Assert(node.getKind() == kind::VARIABLE);
+  Assert(node.getMetaKind() == kind::metakind::VARIABLE);
   NodeManager* nm = NodeManager::currentNM();
   unsigned bitwidth = utils::getSize(node);
   if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end())
@@ -550,8 +550,9 @@ void AbstractionModule::collectArguments(TNode node, TNode signature, std::vecto
   if (seen.find(node)!= seen.end())
     return;
 
-  if (node.getKind() == kind::VARIABLE ||
-      node.getKind() == kind::CONST_BITVECTOR) {
+  if (node.getMetaKind() == kind::metakind::VARIABLE
+      || node.getKind() == kind::CONST_BITVECTOR)
+  {
     // a constant in the node can either map to an argument of the abstraction
     // or can be hard-coded and part of the abstraction
     if (signature.getKind() == kind::SKOLEM) {
@@ -666,8 +667,7 @@ Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsign
   }
 
   if (signature.getNumChildren() == 0) {
-    Assert (signature.getKind() != kind::VARIABLE &&
-            signature.getKind() != kind::SKOLEM);
+    Assert(signature.getKind() != kind::metakind::VARIABLE);
     seen[signature] = signature;
     return signature;
   }
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 7e666bcbf..80930866f 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -139,7 +139,8 @@ AigBitblaster::AigBitblaster()
       d_nullContext(new context::Context()),
       d_aigCache(),
       d_bbAtoms(),
-      d_aigOutputNode(NULL)
+      d_aigOutputNode(NULL),
+      d_notify()
 {
   prop::SatSolver* solver = nullptr;
   switch (options::bvSatSolver())
@@ -149,8 +150,8 @@ AigBitblaster::AigBitblaster()
       prop::BVSatSolverInterface* minisat =
           prop::SatSolverFactory::createMinisat(
               d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
-      MinisatEmptyNotify notify;
-      minisat->setNotify(&notify);
+      d_notify.reset(new MinisatEmptyNotify());
+      minisat->setNotify(d_notify.get());
       solver = minisat;
       break;
     }
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 30f1dd00b..dea2d0429 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -67,6 +67,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   // the thing we are checking for sat
   Abc_Obj_t* d_aigOutputNode;
 
+  std::unique_ptr<MinisatEmptyNotify> d_notify;
+
   void addAtom(TNode atom);
   void simplifyAig();
   void storeBBAtom(TNode atom, Abc_Obj_t* atom_bb) override;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 0e0cee7f8..0c5920951 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -161,6 +161,7 @@ REG0_TESTS = \
 	regress0/bv/bug733.smt2 \
 	regress0/bv/bug734.smt2 \
 	regress0/bv/bv-abstr-bug.smt2 \
+	regress0/bv/bv-abstr-bug2.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-bug2.smt2 b/test/regress/regress0/bv/bv-abstr-bug2.smt2
new file mode 100644
index 000000000..939439adf
--- /dev/null
+++ b/test/regress/regress0/bv/bv-abstr-bug2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-int-as-bv=32 --bitblast=eager
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun _substvar_7_ () Bool)
+(declare-fun _substvar_3_ () Int)
+(assert (or _substvar_7_ (= 0 _substvar_3_)))
+(check-sat)