* Option --no-type-checking now disables type checks in SmtEngine

* Adding options --lazy-type-checking and --eager-type-checking
  to control type checking in NodeBuilder, which can now be enabled
  in production mode and disabled in debug mode
* Option --no-checking implies --no-type-checking
* Adding constructor SmtEngine(ExprManager* em) that uses default options

1 files changed, 3 insertions, 3 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1dada2e69..1c7c506ee 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -26,11 +26,11 @@
 #include "expr/node.h"
 #include "util/result.h"
 #include "util/decision_engine.h"
+#include "smt/options.h"
 
 namespace CVC4 {
 
 class TheoryEngine;
-class Options;
 
 namespace prop {
 
@@ -50,7 +50,7 @@ class PropEngine {
   bool d_inCheckSat;
 
   /** The global options */
-  const Options *d_options;
+  //const Options d_options;
 
   /** The decision engine we will be using */
   DecisionEngine *d_decisionEngine;
@@ -76,7 +76,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(const Options*, DecisionEngine*, TheoryEngine*, context::Context*);
+  PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&);
 
   /**
    * Destructor.