When proof enabled, disable uf sym break. Add regression.

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 );