diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 13:52:34 -0500 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 13:57:50 -0500 |
| commit | 761c1e709a5c3a8013d1da19ca7083cc8e9b2ed3 (patch) | |
| tree | a56da902cfe38e260fc5cb8a59f11bacfeeecfdf /src/smt/smt_engine.cpp | |
| parent | f156fc77b30142dcf33d15bdd04c11056281c3ba (diff) | |
portfolio: fix export of emptyset
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4ab8cb548..9abd6e165 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1439,9 +1439,9 @@ void SmtEngine::defineFunction(Expr func, stringstream ss; ss << "Declared type of defined constant does not match its definition\n" << "The constant : " << func << "\n" - << "Declared type : " << funcType << "\n" + << "Declared type : " << funcType << " " << Type::getTypeNode(funcType)->getId() << "\n" << "The definition : " << formula << "\n" - << "Definition type: " << formulaType; + << "Definition type: " << formulaType << " " << Type::getTypeNode(formulaType)->getId(); throw TypeCheckingException(func, ss.str()); } } |