From 968ba63bab1709096f09efcdf84651c8c1481110 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Mar 2021 20:18:24 -0800 Subject: [PATCH] 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. --- src/preprocessing/passes/bv_to_int.cpp | 9 +-------- src/theory/arrays/theory_arrays.cpp | 7 ++++--- 2 files changed, 5 insertions(+), 11 deletions(-) diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 4712db91f..704214d06 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -687,16 +687,9 @@ Node BVToInt::translateWithChildren(Node original, returnNode = translateQuantifiedFormula(original); break; } - case kind::EXISTS: - { - // Exists is eliminated by the rewriter. - Assert(false); -#ifdef NDEBUG - CVC4_FALLTHROUGH; -#endif - } default: { + Assert(oldKind != kind::EXISTS); // Exists is eliminated by the rewriter. // In the default case, we have reached an operator that we do not // translate directly to integers. The children whose types have // changed from bv to int should be adjusted back to bv and then 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 -- 2.30.2