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

2 files changed, 3 insertions, 1 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6453a84d5..d434799b7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -119,7 +119,7 @@ class NodeManager {
 
   /**
    * Whether to do early type checking (only effective in debug
-   * builds; other builds never do early type checking.
+   * builds; other builds never do early type checking).
    */
   const bool d_earlyTypeChecking;
 
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.";