diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-11 12:35:46 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-11 14:35:58 -0400 |
| commit | d6ebdff6379d7b7a24bc6b9b59eb92d32fe0634a (patch) | |
| tree | 8e7796642448cbe9861d438f79342c67c0ed52d3 /src | |
| parent | 455123f08cb9001bfa05f94030db8e1d776381c7 (diff) | |
sets: comment out an assertion too strong
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3ca446ec5..f768bd62d 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -90,7 +90,9 @@ void TheorySetsPrivate::check(Theory::Effort level) { finishPropagation(); Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; - Assert( d_conflict ^ d_equalityEngine.consistent() ); + // Assert( d_conflict ^ d_equalityEngine.consistent() ); + // ^ doesn't hold when we propagate equality/disequality between shared terms + // and that leads to conflict (externally). if(d_conflict) { return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } |