diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-01 22:44:40 +0200 |
commit | cbcc5124a8f0f17acd981a80c182616cd0a778ff (patch) | |
tree | 0a77487acde8a9a05762b7dcfe436c76defb1f0b /src/proof/cnf_proof.cpp | |
parent | 7f85896a9f1c9d3c8f65c53c16fea2156bc4dfab (diff) |
When proof enabled, disable uf sym break. Add regression.
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index b546fcf87..263e1fe8c 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -87,6 +87,7 @@ void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) { os << "(th_let_pf _ "; //TODO + Trace("cnf-pf-debug") << "; preprocess assertion : " << e << std::endl; os << "(trust_f "; LFSCTheoryProof::printTerm(e, os); os << ") "; @@ -132,7 +133,9 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id ); ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id ); - + Trace("cnf-pf") << std::endl; + Trace("cnf-pf") << "; formula for clause id " << id << " : " << base_assertion << std::endl; + //get the assertion for the clause id std::map< Expr, unsigned > childIndex; std::map< Expr, bool > childPol; @@ -152,7 +155,6 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { std::map< Expr, unsigned >::iterator itci = childIndex.find( base_assertion ); bool is_in_clause = itci!=childIndex.end(); unsigned base_index = is_in_clause ? itci->second : 0; - Trace("cnf-pf") << std::endl; Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl; if( !is_input ){ Assert( is_in_clause ); |