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

3 files changed, 13 insertions, 9 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 );
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 2d8c4178a..311d4afeb 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -176,15 +176,16 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK
     d_propVars.insert(lit.getSatVariable());
   }*/
   if (kind == INPUT) {
+    Debug("cores") << "; Add to inputClauses " << id << std::endl;
     d_inputClauses.insert(std::make_pair(id, clause));
     Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
-    Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl;
+    Debug("cores") << "; core id is " << d_satProof->d_inputClauses[id] << std::endl;
     if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
-      Debug("cores") << " + constant unit (true or false)" << std::endl;
+      Debug("cores") << "; + constant unit (true or false)" << std::endl;
     } else if(options::unsatCores()) {
       Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
-      Debug("cores") << "core input assertion from CnfStream is " << e << std::endl;
-      Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl;
+      Debug("cores") << "; core input assertion from CnfStream is " << e << std::endl;
+      Debug("cores") << "; with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000llu) >> 32) << std::endl;
       // Invalid proof rules are currently used for parts of CVC4 that don't
       // support proofs (these are e.g. unproven theory lemmas) or don't need
       // proofs (e.g. split lemmas).  We can ignore these safely when
@@ -331,12 +332,13 @@ bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) {
 }
 
 void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) {
+  Trace("cnf-pf-debug") << "; set registering formula " << n << " proof rule = " << proof_id << std::endl;
   d_registering_assertion = n;
   d_registering_rule = proof_id;
 }
 
 void ProofManager::setRegisteredClauseId( ClauseId id ) {
-  Trace("cnf-pf-debug") << "set register clause id " << id << " " << d_registering_assertion << std::endl;
+  Trace("cnf-pf-debug") << "; set register clause id " << id << " " << d_registering_assertion << std::endl;
   if( !d_registering_assertion.isNull() ){
      d_clause_id_to_assertion[id] = d_registering_assertion.toExpr();
      d_clause_id_to_rule[id] = d_registering_rule;
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 7867f1ddc..6854f4940 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -364,12 +364,12 @@ void SatProof::printRes(ResChain* res) {
 /// registration methods
 
 ClauseId SatProof::registerClause(Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
-  Debug("cores") << "registerClause " << proof_id << std::endl;
+  Debug("cores") << "registerClause, proof id = " << proof_id << std::endl;
   Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
-    d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); 
+    d_clauseId.insert(ClauseIdMap::value_type(clause, newId));
     d_idClause.insert(IdCRefMap::value_type(newId, clause));
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());