From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Dec 2013 21:04:14 +0000 (-0500)
Subject: Don't put define-funs in model output; bug 411 testcase no longer relevant.
X-Git-Tag: cvc5-1.0.0~7208
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=863dd51bd8b5d72d41006a02950de28fc1666f21;p=cvc5.git

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

diff --git a/NEWS b/NEWS
index 02779ed24..1ff3392ce 100644
--- 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 07b30a87e..eaaa201c3 100644
--- 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 1e3e7c112..1daa0d1e8 100644
--- 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
index 46ac4b544..000000000
--- 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)