From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 22 Oct 2010 18:02:01 +0000 (+0000)
Subject: comment out the "interactive" check in SmtEngine::getValue() for now (resolves bug... 
X-Git-Tag: cvc5-1.0.0~8791
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=11cb621b7fde60a17386b7da4e383bc15e71ab27;p=cvc5.git

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

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.";