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

1 files changed, 10 insertions, 3 deletions

diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 59dc543ae..2d9e04281 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -59,9 +59,16 @@ class BvInverter
    * pvs (if pvs is non-null). If return value R is non-null, then :
    *   lit.path = pv R.path = sv
    *   R.path' = pvs for all lit.path' = pv, where path' != path
+   *
+   * If the flag projectNl is false, we return the null node if the
+   * literal lit is non-linear with respect to pv.
    */
-  Node getPathToPv(
-      Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path);
+  Node getPathToPv(Node lit,
+                   Node pv,
+                   Node sv,
+                   Node pvs,
+                   std::vector<unsigned>& path,
+                   bool projectNl);
 
   /**
    * Same as above, but does not linearize lit for pv.
@@ -69,7 +76,7 @@ class BvInverter
    */
   Node getPathToPv(Node lit, Node pv, std::vector<unsigned>& path)
   {
-    return getPathToPv(lit, pv, pv, Node::null(), path);
+    return getPathToPv(lit, pv, pv, Node::null(), path, false);
   }
 
   /** solveBvLit