Fix regression, minor change to output.

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 8bc9689bdccefd24d9a02b0b3179352d9e8f6e1f..560f68810c7cbb54b6e02c38d1b43f041806b7b7 100644 (file)
--- 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 48b732f26751bb0e3e97ea29b0772c1c5668f842..8cff980a57e43f93c2dc8fc33f0cf07579d9af44 100644 (file)
--- 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)