diff options
author | Guy <katz911@gmail.com> | 2016-07-26 16:37:57 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-26 16:37:57 -0700 |
commit | 90312eb079b1f70ea4d8d229f66273a66a1b7ab1 (patch) | |
tree | 27655ab10aee46391ed85af7656db80a6961f68f | |
parent | e6d75ab22dfb56df202b916ecd9b4327f931c782 (diff) |
Bug fix:
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay
-rw-r--r-- | src/proof/proof_manager.cpp | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e5e00f117..65dbb644d 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -336,11 +336,8 @@ std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) { prop::SatLiteral lit = (*clause)[i]; Node node = getCnfProof()->getAtom(lit.getSatVariable()); Expr atom = node.toExpr(); - if (atom.isConst()) { - Assert (atom == utils::mkTrue()); - continue; - } - result.insert(lit.isNegated() ? node.notNode() : node); + if (atom != utils::mkTrue()) + result.insert(lit.isNegated() ? node.notNode() : node); } return result; |