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