diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-07 07:11:24 +0000 |
| commit | 49dd14da8d872403b4d772a2d49224e4d6bda227 (patch) | |
| tree | 5abbd246c8a1bb797e97d4b9754a4f850e1dc1b5 /src/theory/arrays | |
| parent | 67903280f8fe6946a36ef9fc08bfc747f74bfbd7 (diff) | |
fixing some bugs in propagation of disequalities
still doesnt fix the wrong answers thought :(
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
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; |