diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-01 20:18:24 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-02 04:18:24 +0000 |
| commit | 968ba63bab1709096f09efcdf84651c8c1481110 (patch) | |
| tree | abc4b20a1b0506ff63bfe7d4e29da860dd0e1caa /src/theory/arrays | |
| parent | 4132e91fdb2f8912a89a101e96c86bf5076b327a (diff) | |
Fix nightly errors. (#6034)
Fixes warnings with CVC4_FALLTHROUGH and -Werror for debug/production with gcc/clang. Clang detects that a CVC4_FALLTHROUGH after an Assert(false); is unreachable and issues a warning, while gcc issues a warning about an implicit fall-through if CVC4_FALLTHROUGH is not present.
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 49f530e32..cdb106199 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -936,11 +936,12 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl; break; case EQUALITY_FALSE_AND_PROPAGATED: + Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair " + "called when false in model" + << std::endl; // Should have been propagated to us Assert(false); -#ifdef NDEBUG - CVC4_FALLTHROUGH; -#endif + break; case EQUALITY_FALSE: CVC4_FALLTHROUGH; case EQUALITY_FALSE_IN_MODEL: // This is unlikely, but I think it could happen |