From 30d21b25af6ee619e5f53d1ca8821b710fad4cb7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 24 Jun 2013 12:52:07 -0500
Subject: Add options for symmetry breaking in uf+ss totality axiom approach,
 option for using clique lemmas instead of splitting on demand, option for
 simplifying models in fmf-fmc, minor fixes for rewrite engine

---
 src/theory/quantifiers/rewrite_engine.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/theory/quantifiers/rewrite_engine.cpp')

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 5a35e3808..84d465579 100755
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -36,7 +36,7 @@ void RewriteEngine::check( Theory::Effort e ) {
     for( unsigned i=0; i<d_rr_quant.size(); i++ ) {
       addedLemmas += checkRewriteRule( d_rr_quant[i] );
     }
-    Trace("rewrite-engine") << "Rewrite engine generated " << addedLemmas << " lemmas." << std::endl;
+    Trace("inst-engine") << "Rewrite engine added " << addedLemmas << " lemmas." << std::endl;
     if (addedLemmas==0) {
     }else{
       //otherwise, the search will continue
@@ -85,7 +85,7 @@ int RewriteEngine::checkRewriteRule( Node f ) {
         bool trueInModel = false;
 
         if( !trueInModel ){
-          Trace("rewrite-engine-inst") << "Add instantiation : " << m << std::endl;
+          Trace("rewrite-engine-inst-debug") << "Add instantiation : " << m << std::endl;
           if( d_quantEngine->addInstantiation( f, m ) ){
             addedLemmas++;
             Trace("rewrite-engine-inst-debug") << "success" << std::endl;
-- 
cgit v1.2.3