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 | |
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.
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 9 | ||||
-rw-r--r-- | 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 |