From b63e4a11733051728397f7d4ecb3b205fbd81dab Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 7 Oct 2010 22:54:43 +0000
Subject: type checking for define-fun in production builds; related to (and
 might resolve) bug 212

---
 src/util/options.h | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'src/util/options.h')

diff --git a/src/util/options.h b/src/util/options.h
index 9bb0b0a38..08de590d8 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -77,6 +77,12 @@ struct CVC4_PUBLIC Options {
    */
   bool interactiveSetByUser;
 
+  /** Whether we support SmtEngine::getValue() for this run. */
+  bool produceModels;
+
+  /** Whether we support SmtEngine::getAssignment() for this run. */
+  bool produceAssignments;
+
   Options() :
     binary_name(),
     statistics(false),
@@ -91,7 +97,9 @@ struct CVC4_PUBLIC Options {
     strictParsing(false),
     lazyDefinitionExpansion(false),
     interactive(false),
-    interactiveSetByUser(false) {
+    interactiveSetByUser(false),
+    produceModels(false),
+    produceAssignments(false) {
   }
 };/* struct Options */
 
-- 
cgit v1.2.3