From ad2fc7c63e8f9d91ff0b750207fdae5fd029134b Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 10 Mar 2020 22:42:49 -0700 Subject: [PATCH] bv-gauss-elim: Fix handling of inconsistent case. (#4027) This fixes the case when all rows are inconsistent. Fixes #3999. --- src/preprocessing/passes/bv_gauss.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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) -- 2.30.2