1 files changed, 4 insertions, 0 deletions
diff --git a/src/smt/options.h b/src/smt/options.h
index 7ddaf5d4d..73c38545f 100644
--- a/src/smt/options.h
+++ b/src/smt/options.h
@@ -89,6 +89,9 @@ struct CVC4_PUBLIC Options {
   /** Whether we support SmtEngine::getAssignment() for this run. */
   bool produceAssignments;
 
+  /** Whether we do typechecking at all. */
+  bool typeChecking;
+
   /** Whether we do typechecking at Expr creation time. */
   bool earlyTypeChecking;
 
@@ -109,6 +112,7 @@ struct CVC4_PUBLIC Options {
     interactiveSetByUser(false),
     produceModels(false),
     produceAssignments(false),
+    typeChecking(true),
     earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
   }
 };/* struct Options */