From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 2 Mar 2021 04:18:24 +0000 (-0800)
Subject: Fix nightly errors. (#6034)
X-Git-Tag: cvc5-1.0.0~2171
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=968ba63bab1709096f09efcdf84651c8c1481110;p=cvc5.git

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 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