Disable solving non-linear BV literals by default (#2070)

1 files changed, 11 insertions, 3 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
index 0274d45cd..cf09cfa55 100644
--- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp
@@ -991,8 +991,9 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
   std::vector<unsigned> path;
   Node sv = d_inverter->getSolveVariable(pv.getType());
   Node pvs = ci->getModelValue(pv);
-  Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl;
-  Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path);
+  Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
+  Node slit =
+      d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cbqiBvSolveNl());
   if (!slit.isNull())
   {
     CegInstantiatorBvInverterQuery m(ci);
@@ -1017,6 +1018,10 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
       Trace("cegqi-bv") << "...failed to solve." << std::endl;
     }
   }
+  else
+  {
+    Trace("cegqi-bv") << "...no path." << std::endl;
+  }
 }
 
 Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
@@ -1981,7 +1986,10 @@ void BvInstantiatorPreprocess::collectExtracts(
       {
         if (cur.getKind() == BITVECTOR_EXTRACT)
         {
-          extract_map[cur[0]].push_back(cur);
+          if (cur[0].getKind() == INST_CONSTANT)
+          {
+            extract_map[cur[0]].push_back(cur);
+          }
         }
 
         for (const Node& nc : cur)