usability: remove --no-interactive from --smtlib option

diff --git a/src/options/base_options b/src/options/base_options
index 9f0ccc9a57f8f3e97e3bdc7913e3209d081c72ab..573a11d29332aa514573ff33e8f3be8092834ac3 100644 (file)
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -125,7 +125,7 @@ option - debug -d --debug=TAG argument :handler CVC4::options::addDebugTag
 option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
  print the "success" output required of SMT-LIBv2
 
-alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
+alias --smtlib = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental
  SMT-LIBv2 compliance mode (implies other options)
 undocumented-alias --smtlib2 = --smtlib