1 files changed, 13 insertions, 2 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index b0f7a2cb8..3ff27366b 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -175,8 +175,12 @@ Node BvInverter::getPathToPv(
   return Node::null();
 }
 
-Node BvInverter::getPathToPv(
-    Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path)
+Node BvInverter::getPathToPv(Node lit,
+                             Node pv,
+                             Node sv,
+                             Node pvs,
+                             std::vector<unsigned>& path,
+                             bool projectNl)
 {
   std::unordered_set<TNode, TNodeHashFunction> visited;
   Node slit = getPathToPv(lit, pv, sv, path, visited);
@@ -186,7 +190,14 @@ Node BvInverter::getPathToPv(
     // substitute pvs for the other occurrences of pv
     TNode tpv = pv;
     TNode tpvs = pvs;
+    Node prev_lit = slit;
     slit = slit.substitute(tpv, tpvs);
+    if (!projectNl && slit != prev_lit)
+    {
+      // found another occurrence of pv that was not on the solve path,
+      // hence lit is non-linear wrt pv and we return null.
+      return Node::null();
+    }
   }
   return slit;
 }