diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5a8a75aab..0ab188dc4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -772,14 +772,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Node normalizedLiteral = Rewriter::rewrite(literal); if (d_propEngine->isSatLiteral(normalizedLiteral)) { // If there is a literal, propagate it to SAT - if (d_propEngine->hasValue(normalizedLiteral, value)) { - // if we are propagting something that already has a sat value we better be the same - Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl; - Assert(value); - } else { - SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); - d_propagatedSharedLiterals.push_back(sharedLiteral); - } + SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST); + d_propagatedSharedLiterals.push_back(sharedLiteral); } // Assert to interested theories Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl; |