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 9634cb47bbaf7a0d511a35ea274ec1ad038470e1..b546fcf87c2cd7d9b42acf9407836d9385445d85 100644 (file)
--- 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 a8e7b6a8e191399af909e79d5fb7d930b12e6fbc..50de00b61736f312ec6402d5dc8b743459d16ac5 100644 (file)
--- 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