* 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, 1 insertions, 8 deletions

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 8f790c211..8ed938351 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -128,18 +128,11 @@ int runCvc4(int argc, char* argv[]) {
     options.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
-  /* Early type checking can be turned off by --no-type-checking OR
-     --no-checking. We're assuming that earlyTypeChecking is not
-     explicitly set by the user. */
-  if(options.earlyTypeChecking) {
-    options.earlyTypeChecking = options.semanticChecks;
-  }
-
   // Create the expression manager
   ExprManager exprMgr(options.earlyTypeChecking);
 
   // Create the SmtEngine
-  SmtEngine smt(&exprMgr, &options);
+  SmtEngine smt(&exprMgr, options);
 
   // Auto-detect input language by filename extension
   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];