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: [PATCH] Fix regression, minor change to output.

---
 src/theory/quantifiers/term_database.cpp | 18 ++++++++++--------
 test/regress/regress0/fmf/Makefile.am    |  2 +-
 2 files changed, 11 insertions(+), 9 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 ];
 }
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 48b732f26..8cff980a5 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -50,7 +50,7 @@ TESTS =	\
 	loopy_coda.smt2 \
 	fmc_unsound_model.smt2 \
 	am-bad-model.cvc \
-	nun-0208-to.cvc
+	nun-0208-to.smt2
 
 
 EXTRA_DIST = $(TESTS)
-- 
2.30.2