From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 11 Mar 2020 05:42:49 +0000 (-0700)
Subject: bv-gauss-elim: Fix handling of inconsistent case. (#4027)
X-Git-Tag: cvc5-1.0.0~3519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad2fc7c63e8f9d91ff0b750207fdae5fd029134b;p=cvc5.git

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 0f2674680..683716410 100644
--- 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)