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.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 4712db91f6b73cb0bdf15ef311fbffd386df5d45..704214d063d582e69d2d8ebfbd6762783613c465 100644 (file)
--- 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 49f530e3262916040ba364d972d7bc2e4dc6b476..cdb106199df85af59556659ef60996e6c49cccf1 100644 (file)
--- 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