diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-10 22:42:49 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-10 22:42:49 -0700 |
| commit | ad2fc7c63e8f9d91ff0b750207fdae5fd029134b (patch) | |
| tree | faf75906635adc4abfe642a6f8c0900fe921ab53 /src/preprocessing | |
| parent | 6a2619c8c14e138b0ce4fdfe59e06dbcde2f61c7 (diff) | |
bv-gauss-elim: Fix handling of inconsistent case. (#4027)
This fixes the case when all rows are inconsistent.
Fixes #3999.
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/passes/bv_gauss.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
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) |