From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 25 May 2015 08:34:26 +0000 (+0200)
Subject: Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.
X-Git-Tag: cvc5-1.0.0~6324
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e22a9ebb7b1825cd8f35fe258e6ac345773a9e5;p=cvc5.git

Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.
---

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 9634cb47b..b546fcf87 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -194,7 +194,7 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
           //Assert( child_pol==childPol[child_base] );
           os_main << "(or_elim_1 _ _ ";
           prop::SatLiteral lit = (*clause)[itcic->second];
-          if( childPol[child_base] ){
+          if( childPol[child_base] && base_pol ){
             os_main << ProofManager::getLitName(lit) << " ";
           }else{
             os_main << "(not_not_intro _ " << ProofManager::getLitName(lit) << ") ";
@@ -224,7 +224,7 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
         if( itcic!=childIndex.end() ){
           os << "(contra _ ";
           prop::SatLiteral lit = (*clause)[itcic->second];
-          if( childPol[child_base] ){
+          if( childPol[child_base] && base_pol ){
             os << os_main.str() << " " << ProofManager::getLitName(lit);
           }else{
             os << ProofManager::getLitName(lit) << " " << os_main.str();
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index a8e7b6a8e..50de00b61 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -48,7 +48,8 @@ TESTS =	\
 	proof00.smt2 \
 	cnf-iff.smt2 \
 	cnf-iff-base.smt2 \
-	cnf-ite.smt2
+	cnf-ite.smt2 \
+	cnf-and-neg.smt2
 
 EXTRA_DIST = $(TESTS) \
 	mkpidgeon