diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 23:25:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-01 23:25:04 -0500 |
| commit | e3d4f6da2307659999e5eb5894d63982e8d487c5 (patch) | |
| tree | 06a161168a6ab0aefd2fc1dd370a75538187017f /src/smt/smt_engine.cpp | |
| parent | ce9e2004b59a48c54b78536a53e66de8be94ab7c (diff) | |
| parent | 1b89c8628eee3d081e91bf99745a16a21c40bf8a (diff) | |
Merge branch 'master' into rm_svnrm_svn
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cfafd63c4..116d2fe23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -759,12 +759,15 @@ public: } } - void nmNotifyNewSortConstructor(TypeNode tn) override + void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); - d_smt.addToModelCommandAndDump(c); + if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) + { + d_smt.addToModelCommandAndDump(c); + } } void nmNotifyNewDatatypes(const std::vector<DatatypeType>& dtts) override |