bv-gauss-elim: Fix handling of inconsistent case. (#4027)

This fixes the case when all rows are inconsistent.
Fixes #3999.

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 0f2674680a121dd18e5692c66ff47e0ff0384030..68371641019192241e753a6cde78848dd68d7839 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -571,7 +571,10 @@ BVGauss::Result BVGauss::gaussElimRewriteForUrem(
   }
 
   size_t nvars = vars.size();
-  Assert(nvars);
+  if (nvars == 0)
+  {
+    return BVGauss::Result::INVALID;
+  }
   size_t nrows = vars.begin()->second.size();
 #ifdef CVC4_ASSERTIONS
   for (const auto& p : vars)