comment out the "interactive" check in SmtEngine::getValue() for now (resolves bug...

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6453a84d588023ecfb437a682e5a4d8691b483d2..d434799b7f3ab04ab3d43dcf2202f223954a966b 100644 (file)
--- 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 d76a002e76e53ec157c657dab43de16068919c86..149c3620d9f12256faaab4b1a2efd708d949cb92 100644 (file)
--- 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.";