Fix regression, minor change to output.

1 files changed, 10 insertions, 8 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8bc9689bd..560f68810 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -976,6 +976,16 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
   if( f.hasAttribute(InstLevelAttribute()) ){
     theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) );
   }
+
+  if( Trace.isOn("quantifiers-sk") ){
+    Trace("quantifiers-sk") << "Skolemize : ";
+    for( unsigned i=0; i<sk.size(); i++ ){
+      Trace("quantifiers-sk") << sk[i] << " ";
+    }
+    Trace("quantifiers-sk") << "for " << std::endl;
+    Trace("quantifiers-sk") << "   " << f << std::endl;
+  }
+
   return ret;
 }
 
@@ -1002,14 +1012,6 @@ Node TermDb::getSkolemizedBody( Node f ){
         d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] );
       }
     }
-    if( Trace.isOn("quantifiers-sk") ){
-      Trace("quantifiers-sk") << "Skolemize : ";
-      for( unsigned i=0; i<d_skolem_constants[f].size(); i++ ){
-        Trace("quantifiers-sk") << d_skolem_constants[f][i] << " ";
-      }
-      Trace("quantifiers-sk") << "for " << std::endl;
-      Trace("quantifiers-sk") << "   " << f << std::endl;
-    }
   }
   return d_skolem_body[ f ];
 }