diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-22 22:01:36 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-22 22:01:36 +0000 |
| commit | 2a57acc989a917a58dbecb2944c8438140a5627c (patch) | |
| tree | 5b0263c188b1fa7475fc5ffb82914f55f2b37e82 /src/smt | |
| parent | 2499bd64a5ac688573ebbcd6114983f64a8094eb (diff) | |
Fixing SmtEngine::getValue() by adding a NodeManagerScope (thanks Tim for finding this)
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 376a8a531..c28ee7064 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -596,6 +596,7 @@ Expr SmtEngine::simplify(const Expr& e) { Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); + NodeManagerScope nms(d_nodeManager); Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point Debug("smt") << "SMT getValue(" << e << ")" << endl; if(!Options::current()->produceModels) { |