Don't put define-funs in model output; bug 411 testcase no longer relevant.

diff --git a/NEWS b/NEWS
index 02779ed2451f4f8d0dee155025fbe5c5cd126e13..1ff3392ce15642b898720738494599fecbc560f5 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -20,6 +20,8 @@ Changes since 1.2
   zero means no error---but the result could be sat, unsat, or unknown---and
   nonzero means error.
 * bv2nat/int2bv functionality
+* User-defined symbols (define-funs) are no longer reported in the output
+  of get-model commands.
 
 Changes since 1.1
 =================

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 07b30a87e2b0dc02eee39f3fe97d45a46bcc5368..eaaa201c31d1033b0d57e195cd324d825fd8266d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1306,7 +1306,7 @@ void SmtEngine::defineFunction(Expr func,
   ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream()))
      << func;
   DefineFunctionCommand c(ss.str(), func, formals, formula);
-  addToModelCommandAndDump(c, ExprManager::VAR_FLAG_NONE, true, "declarations");
+  addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
   SmtScope smts(this);
 
@@ -3609,7 +3609,9 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool
   // decouple SmtEngine and ExprManager if the user does a few
   // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
   // and expects to find their cardinalities in the model.
-  if(/* userVisible && */ (!d_fullyInited || options::produceModels())) {
+  if(/* userVisible && */
+     (!d_fullyInited || options::produceModels()) &&
+     (flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
     doPendingPops();
     if(flags & ExprManager::VAR_FLAG_GLOBAL) {
       d_modelGlobalCommands.push_back(c.clone());

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 1e3e7c1124942ae065693d0d90600c0fb22c9511..1daa0d1e88d4c8147348d27a2a80efa8e95b522a 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -136,7 +136,6 @@ BUG_TESTS = \
        bug382.smt2 \
        bug383.smt2 \
        bug398.smt2 \
-       bug411.smt2 \
        bug421.smt2 \
        bug421b.smt2 \
        bug425.cvc \

diff --git a/test/regress/regress0/bug411.smt2 b/test/regress/regress0/bug411.smt2
deleted file mode 100644 (file)
index 46ac4b5..0000000
--- a/test/regress/regress0/bug411.smt2
+++ /dev/null
@@ -1,9 +0,0 @@
-; EXPECT: sat
-; EXPECT: (model
-; EXPECT: (define-fun x () Int 5)
-; EXPECT: )
-(set-option :produce-models true)
-(set-logic QF_UFLIA)
-(define-fun x () Int 5)
-(check-sat)
-(get-model)