Fix more cases of rewritten explanations in strings for bug 784. Minor.

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 8e9939f61fa40ebd40191e8b566546399afbdbdf..0faf7b176c6ee56b5d0c68ef59a7b6510e6d7a7a 100644 (file)
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -164,7 +164,7 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
 Node TheorySepRewriter::preSkolemEmp( Node n, bool pol, std::map< bool, std::map< Node, Node > >& visited ) {
   std::map< Node, Node >::iterator it = visited[pol].find( n );
   if( it==visited[pol].end() ){
-    Trace("ajr-temp") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
+    Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl;
     Node ret = n;
     if( n.getKind()==kind::SEP_EMP ){
       if( !pol ){

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b0a9e6a1fea6c20f6a3e7cc6fd031364f146ec7c..5f05003c63785e12fc8cab65f842c85ab0cfd5bd 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3973,10 +3973,10 @@ Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) {
 
 Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) {
   if(d_regexp_ant.find(atom) == d_regexp_ant.end()) {
-    return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, ant, atom) );
+    return NodeManager::currentNM()->mkNode(kind::AND, ant, atom);
   } else {
     Node n = d_regexp_ant[atom];
-    return Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, ant, n) );
+    return NodeManager::currentNM()->mkNode(kind::AND, ant, n);
   }
 }
 
@@ -4490,7 +4490,7 @@ void TheoryStrings::checkMemberships() {
                 }
               }
             }
-            antec = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp)) );
+            antec = NodeManager::currentNM()->mkNode(kind::AND, antec, mkExplain(rnfexp));
             Node conc = nvec.size()==1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec);
             conc = Rewriter::rewrite(conc);
             sendLemma( antec, conc, "REGEXP_Unfold" );
@@ -4630,7 +4630,7 @@ bool TheoryStrings::checkPDerivative( Node x, Node r, Node atom, bool &addedLemm
     switch(d_regexp_opr.delta(r, exp)) {
       case 0: {
         Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
-        antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
+        antec = NodeManager::currentNM()->mkNode(kind::AND, antec, antnf);
         sendLemma(antec, exp, "RegExp Delta");
         addedLemma = true;
         d_regexp_ccached.insert(atom);
@@ -4642,7 +4642,7 @@ bool TheoryStrings::checkPDerivative( Node x, Node r, Node atom, bool &addedLemm
       }
       case 2: {
         Node antec = mkRegExpAntec(atom, x.eqNode(d_emptyString));
-        antec = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, antec, antnf));
+        antec = NodeManager::currentNM()->mkNode(kind::AND, antec, antnf);
         Node conc = Node::null();
         sendLemma(antec, conc, "RegExp Delta CONFLICT");
         addedLemma = true;
@@ -4671,7 +4671,7 @@ bool TheoryStrings::checkPDerivative( Node x, Node r, Node atom, bool &addedLemm
       }
     }*/
     Node sREant = mkRegExpAntec(atom, d_true);
-    sREant = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf));
+    sREant = NodeManager::currentNM()->mkNode(kind::AND, sREant, antnf);
     if(deriveRegExp( x, r, sREant )) {
       addedLemma = true;
       d_regexp_ccached.insert(atom);