comment out the "interactive" check in SmtEngine::getValue() for now (resolves bug 224), and fix a comment in NodeManager header

1 files changed, 2 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d76a002e7..149c3620d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -490,11 +490,13 @@ Expr SmtEngine::getValue(const Expr& e)
   Assert(e.getExprManager() == d_exprManager);
   Type type = e.getType(d_typeChecking);// ensure expr is type-checked at this point
   Debug("smt") << "SMT getValue(" << e << ")" << endl;
+  /* FIXME - for SMT-LIBv2 compliance, we need to check this ?!
   if(!d_interactive) {
     const char* msg =
       "Cannot get value when not in interactive mode.";
     throw ModalException(msg);
   }
+  */
   if(!d_produceModels) {
     const char* msg =
       "Cannot get value when produce-models options is off.";