2 files changed, 4 insertions, 4 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 1d2e4ed8b..6d3a06b4b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -351,6 +351,7 @@ throw(OptionException) {
       break;
 
     case LAZY_TYPE_CHECKING:
+      typeChecking = true;
       earlyTypeChecking = false;
       break;
 
diff --git a/src/util/options.h b/src/util/options.h
index 350c031c7..8cf0b8446 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -29,9 +29,9 @@
 
 #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else
+#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif
+#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
 
 #include <iostream>
 #include <string>
@@ -178,10 +178,9 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
- 
-
 }/* CVC4 namespace */
 
 #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
 
 #endif /* __CVC4__OPTIONS_H */