From 8194c44801d30c0e0aa6129490e0523851b24209 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 9 Feb 2016 16:57:50 -0600
Subject: Fix regression, minor change to output.

---
 src/theory/quantifiers/term_database.cpp | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'src/theory/quantifiers')

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 ];
 }
-- 
cgit v1.2.3