From 49dd14da8d872403b4d772a2d49224e4d6bda227 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Thu, 7 Jun 2012 07:11:24 +0000 Subject: fixing some bugs in propagation of disequalities still doesnt fix the wrong answers thought :( --- src/theory/arrays/theory_arrays.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'src/theory/arrays') diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4ba4aeba5..91bbae2f4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -581,8 +581,8 @@ void TheoryArrays::computeCareGraph() Assert(false); break; case EQUALITY_FALSE_AND_PROPAGATED: - // TODO: eventually this should be an Assert(false), but for now, disequalities are not propagated - continue; + // Should have been propagated to us + Assert(false); break; case EQUALITY_FALSE: case EQUALITY_TRUE: @@ -591,7 +591,6 @@ void TheoryArrays::computeCareGraph() break; case EQUALITY_FALSE_IN_MODEL: Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl; - continue; break; default: break; -- cgit v1.2.3