diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-29 20:13:52 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-06 15:40:36 -0400 |
| commit | 5c42662fe5cea3051341c8292202357e2a5e7dd3 (patch) | |
| tree | 94aa636b95c7a81594a3d82f236263c91b0f6d0f /src/smt | |
| parent | 0dce010bea47bc6a318eece2bd92ed2305b64c21 (diff) | |
Sets translate, and other short fixes
- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f9ac1e9db..33496ac3b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3444,7 +3444,8 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin Trace("smt") << "--- model-post expected " << expectedType << endl; // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType)); + Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType), + "Run with -t smt for details."); // ensure it's a constant Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); |