diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-05 20:59:18 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 17:50:09 -0400 |
| commit | e5044d89c715ac6c0d41a731b58a9c672d2d524e (patch) | |
| tree | 564d0fde03be9525b0912800849f92016b681192 /src/smt | |
| parent | b747578dee53489326bf53743cfc4f83c467cbfd (diff) | |
Fix declare-datatypes dumping bug (bug 385).
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 810715885..987220cc7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -419,11 +419,13 @@ public: d_smt.d_nodeManager->unsubscribeEvents(this); } - void nmNotifyNewSort(TypeNode tn) { + void nmNotifyNewSort(TypeNode tn, uint32_t flags) { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); - d_smt.addToModelCommandAndDump(c); + if((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) { + d_smt.addToModelCommandAndDump(c, flags); + } } void nmNotifyNewSortConstructor(TypeNode tn) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1da8d26da..3531f92e7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -336,7 +336,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, uint32_t flags = ExprManager::VAR_FLAG_NONE, bool userVisible = true, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT |