diff options
-rw-r--r-- | src/proof/cnf_proof.cpp | 4 | ||||
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 3 | ||||
-rwxr-xr-x | test/regress/regress0/uf/cnf-and-neg.smt2 | 11 |
3 files changed, 15 insertions, 3 deletions
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 diff --git a/test/regress/regress0/uf/cnf-and-neg.smt2 b/test/regress/regress0/uf/cnf-and-neg.smt2 new file mode 100755 index 000000000..711740f67 --- /dev/null +++ b/test/regress/regress0/uf/cnf-and-neg.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort I 0)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+(declare-fun f (I) I)
+(assert (not (= (f a) (f b))))
+(assert (not (= (f a) (f c))))
+(assert (not (and (not (= a b)) (not (= a c)))))
+(check-sat)
|