diff options
| -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; |