diff options
Diffstat (limited to 'src/prop/sat.cpp')
| -rw-r--r-- | src/prop/sat.cpp | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 57ec29259..2197cb23e 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -56,12 +56,7 @@ void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) { const unsigned i_end = outputNodes.size(); for (unsigned i = 0; i < i_end; ++ i) { Debug("prop-explain") << "theoryPropagate() => " << outputNodes[i].toString() << std::endl; - // The second argument ("true") instructs the CNF stream to create - // a new literal mapping if it doesn't exist. This can happen due - // to a circular dependence, if a SAT literal "a" is asserted as a - // unit to the SAT solver, a round of theory propagation can occur - // before all Nodes have SAT variable mappings. - SatLiteral l = d_cnfStream->getLiteral(outputNodes[i], true); + SatLiteral l = d_cnfStream->getLiteral(outputNodes[i]); output.push_back(l); } } @@ -91,11 +86,8 @@ void SatSolver::clearPropagatedLiterals() { void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) { Node literalNode = d_cnfStream->getNode(l); Debug("prop") << "enqueueing theory literal " << l << " " << literalNode << std::endl; - // We can get null from the prop engine if the literal is useless (i.e.) - // the expression is not in context anyomore - if(!literalNode.isNull()) { - d_theoryEngine->assertFact(literalNode); - } + Assert(!literalNode.isNull()); + d_theoryEngine->assertFact(literalNode); } void SatSolver::setCnfStream(CnfStream* cnfStream) { |