SMT-LIBv2 compliance updates:

* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
  TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default

Also:

* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection

(this commit was certified error- and warning-free by the test-and-commit script.)

16 files changed, 302 insertions, 111 deletions

diff --git a/config/readline.m4 b/config/readline.m4
index 6cfe6a982..30d285b29 100644
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -3,8 +3,9 @@
 # Look for readline and link it in, but allow user to disable.
 AC_DEFUN([CVC4_CHECK_FOR_READLINE], [
 AC_MSG_CHECKING([whether user requested readline support])
-AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
 LIBREADLINE=
+have_libreadline=0
+READLINE_LIBS=
 if test "$with_readline" = no; then
   AC_MSG_RESULT([no, readline disabled by user])
 else
@@ -13,16 +14,15 @@ else
   else
     AC_MSG_RESULT([yes, readline enabled by user])
   fi
-  AC_CHECK_LIB([readline], [readline],
-               [AC_CHECK_HEADER([readline/readline.h],
-                  [READLINE_LIBS="-lreadline -lncurses -ltermcap -ltinfo"],
-                  [if test "$with_readline" != check; then
-                     AC_MSG_FAILURE([cannot find libreadline!])
-                   fi])],
-               [if test "$with_readline" != check; then
-                  AC_MSG_FAILURE([cannot find libreadline!])
-                fi], [-lncurses -ltermcap -ltinfo])
+  READLINE_LIBS=
+  CVC4_TRY_READLINE_WITH([])
+  CVC4_TRY_READLINE_WITH([-ltinfo])
+  CVC4_TRY_READLINE_WITH([-lncurses -ltermcap])
+  CVC4_TRY_READLINE_WITH([-lncurses -ltermcap -ltinfo])
   if test -z "$READLINE_LIBS"; then
+    if test "$with_readline" != check; then
+      AC_MSG_FAILURE([cannot find libreadline! (or can't get it to work)])
+    fi
     with_readline=no
   else
     # make sure it works in static builds, too
@@ -34,7 +34,7 @@ else
       LDFLAGS="-static $LDFLAGS"
       LIBS="$READLINE_LIBS $LIBS"
       AC_LINK_IFELSE([AC_LANG_PROGRAM([#include <readline/readline.h>],
-                                     [readline("")])],
+                                      [readline("")])],
         [ AC_MSG_RESULT([yes, it works])
           with_readline=yes ],
         [ AC_MSG_RESULT([no])
@@ -50,13 +50,23 @@ else
     fi
   fi
   if test "$with_readline" = yes; then
-    HAVE_LIBREADLINE=1
+    have_libreadline=1
   else
-    HAVE_LIBREADLINE=0
+    have_libreadline=0
     READLINE_LIBS=
   fi
-  AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], ${HAVE_LIBREADLINE}, [Define to 1 to use libreadline])
-  AC_SUBST([READLINE_LIBS])
 fi
 ])# CVC4_CHECK_FOR_READLINE
 
+# CVC4_TRY_READLINE_WITH(LIBS)
+# ----------------------------
+# Try AC_CHECK_LIB(readline) with the given linking libraries
+AC_DEFUN([CVC4_TRY_READLINE_WITH], [
+if test -z "$READLINE_LIBS"; then
+  AC_CHECK_LIB([readline], [readline],
+               [AC_CHECK_HEADER([readline/readline.h],
+                  [READLINE_LIBS="-lreadline $1"],
+                  [])],
+               [], [$1])
+fi
+])# CVC4_TRY_READLINE_WITH
diff --git a/configure.ac b/configure.ac
index 310cd4095..3ef0ac689 100644
--- a/configure.ac
+++ b/configure.ac
@@ -852,7 +852,10 @@ fi
 # Checks for libraries.
 
 # Check for libreadline (defined in config/readline.m4)
+AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
 CVC4_CHECK_FOR_READLINE
+AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
+AC_SUBST([READLINE_LIBS])
 
 AC_SEARCH_LIBS([clock_gettime], [rt],
                [AC_DEFINE([HAVE_CLOCK_GETTIME], [1],
diff --git a/src/options/base_options b/src/options/base_options
index f7d1a77d4..cd1bec00a 100644
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -40,19 +40,33 @@
 #                     | :read-write
 #                     | :link linked-options..
 #
-#   alias smt-option-name = (smt-option-name[=argument])+
-#   alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#   common-alias ALIAS_SPECIFICATION
+#   alias ALIAS_SPECIFICATION
+#   expert-alias ALIAS_SPECIFICATION
+#   undocumented-alias ALIAS_SPECIFICATION
 #
-#     The alias command creates a new SmtEngine option name, or short option, or long option,
-#     and binds it to act the same way as if the options to the right of "=" were passed.
-#     For example, if there are options to --disable-warning-1 and --disable-warning-2, etc.,
-#     a useful alias might be:
+#       ALIAS_SPECIFICATION ::=   (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#                               | (-short-option=ARG | --long-option=ARG) = (-option[=ARG|argument] | --long-option[=ARG|argument])+
+#
+#     The alias command creates a new short or long option, and binds it
+#     to act the same way as if the options to the right of "=" were passed.
+#     For example, if there are options to --disable-warning-1 and
+#     --disable-warning-2, etc., a useful alias might be:
 #
 #       alias --disable-all-warnings = --disable-warning-1 --disable-warning-2
 #
-#     Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties,
-#     and SmtEngine aliases cannot set command-line properties.  For these things, you need a
-#     custom handler.
+#     It's also possible to pass an argument through to another option.
+#     This alias makes "--output-language" synonymous with "--output-lang".
+#     Without the "=L" parts, --output-language would not take an argument,
+#     and option processing would fail (because --output-lang expects one).
+#
+#       alias --output-language=L = --output-lang=L
+#
+#     You can also ignore such an argument:
+#
+#       alias --some-option=VALUE = --other-option --option2=foo --option3=bar
+#
+#     or use it for multiple options on the right-hand side, etc.
 #
 #   warning message
 #
@@ -74,9 +88,14 @@ option err std::ostream* :default &std::cerr :include <iostream>
 common-option inputLanguage input-language -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
  force input language (default is "auto"; see --lang help)
 common-option outputLanguage output-language --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
- force input language (default is "auto"; see --lang help)
+ force output language (default is "auto"; see --output-lang help)
 option languageHelp bool
 
+# Allow also --language and --output-language, it's a common mistake to
+# type these, but no need to document it.
+undocumented-alias --language=L = --lang=L
+undocumented-alias --output-language=L = --output-lang=L
+
 option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_options_handlers.h"
  the verbosity level of CVC4
 common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
@@ -86,6 +105,8 @@ common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
 
 common-option statistics statistics --stats bool
  give statistics on exit
+undocumented-alias --statistics = --stats
+undocumented-alias --no-statistics = --no-stats
 
 common-option parseOnly parse-only --parse-only bool :read-write
  exit after parsing input
@@ -104,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 --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental
+alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success --incremental --no-interactive
  SMT-LIBv2 compliance mode (implies other options)
 
 endmodule
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 93885d75f..9e5fb2b81 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -543,7 +543,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links
+      assignBool(options::$internal, option, true, NULL);$run_links
       break;
 "
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -552,12 +552,12 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-  $handler(option, optarg, smt);"
+  $handler(option, optionarg, smt);"
         done
       else
         run_handlers="
 #line $lineno \"$kf\"
-  handleOption<$type>(option, optarg);"
+  handleOption<$type>(option, optionarg);"
       fi
       if [ -n "$predicates" ]; then
         for predicate in $predicates; do
@@ -568,7 +568,7 @@ template <> void runBoolPredicates(options::${internal}__option_t, std::string o
       fi
       all_custom_handlers="${all_custom_handlers}
 #line $lineno \"$kf\"
-template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) {
+template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optionarg, SmtEngine* smt) {
 #line $lineno \"$kf\"
   options::${internal}__option_t::type retval = $run_handlers
 #line $lineno \"$kf\"
@@ -576,7 +576,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 }"
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
 #line $lineno \"$kf\"
-      assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links
+      assign(options::$internal, option, optionarg, NULL);$run_links
       break;
 "
     elif [ -n "$expect_arg" ]; then
@@ -589,7 +589,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);"
+      $handler(option, optionarg, smt);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -607,7 +607,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-      $handler(argv[old_optind == 0 ? 1 : old_optind], smt);"
+      $handler(option, smt);"
         done
       fi
       all_modules_option_handlers="${all_modules_option_handlers}${cases}
@@ -621,7 +621,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
     if [ "$type" = bool ]; then
       all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
 #line $lineno \"$kf\"
-      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate
+      assignBool(options::$internal, option, false, NULL);$run_links_alternate
       break;
 "
     else
@@ -646,7 +646,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links
+    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -655,7 +655,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optarg, smt);
+    $handler(\"$smtname\", optionarg, smt);
 "
         done
       fi
@@ -663,7 +663,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links
+    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
@@ -671,7 +671,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       for handler in $handlers; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", optarg, smt);
+    $handler(\"$smtname\", optionarg, smt);
 "
       done
       smt_setoption_handlers="${smt_setoption_handlers}
@@ -727,12 +727,34 @@ template <> void Options::assign(options::${internal}__option_t, std::string opt
   fi
 }
 
+function common-alias {
+  # common-alias -option[=arg] = (-option[=arg])+
+  handle_alias COMMON "$@"
+}
+
 function alias {
-  # alias (smtname | -option) = (smtname [arg] | -option [arg])+
+  # alias -option[=arg] = (-option[=arg])+
+  handle_alias STANDARD "$@"
+}
+
+function expert-alias {
+  # expert-alias -option[=arg] = (-option[=arg])+
+  handle_alias EXPERT "$@"
+}
+
+function undocumented-alias {
+  # undocumented-alias -option[=arg] = (-option[=arg])+
+  handle_alias UNDOCUMENTED "$@"
+}
+
+function handle_alias {
+  # handle_alias CATEGORY -option[=arg] = (-option[=arg])+
   check_module_seen
   check_doc
 
-  category=STANDARD
+  category="$1"
+  shift
+
   internal=-
   smtname=
   short_option=
@@ -752,16 +774,24 @@ function alias {
   options_already_documented=false
   alternate_options_already_documented=false
 
+  if [ "$category" = UNDOCUMENTED ]; then
+    expect_doc=false
+  else
+    expect_doc=true
+  fi
+  expect_doc_alternate=false
+
   if [ $# -lt 3 ]; then
     echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
     exit 1
   fi
-  options=
-  while [ $# -gt 0 -a "$1" != = ]; do
-    options="$options $1"
-    shift
-  done
-  if [ $# -eq 0 ]; then
+  if [ "$1" = '=' ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected option name" >&2
+    exit 1
+  fi
+  option="$1"
+  shift
+  if [ "$1" != '=' ]; then
     echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
     exit 1
   fi
@@ -771,42 +801,76 @@ function alias {
     exit 1
   fi
   cases=
-  for option in $options; do
-    if ! expr "$option" : - &>/dev/null; then
-      echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
-      exit 1
-    fi
-    if expr "$option" : -- &>/dev/null; then
+  if ! expr "$option" : - &>/dev/null; then
+    echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
+    exit 1
+  fi
+  if expr "$option" : -- &>/dev/null; then
+    if expr "$option" : '.*=' &>/dev/null; then
+      expect_arg_long=required_argument
+      arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
+      option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
+      echo "warning: not yet handling long-option alias =$arg" >&2
+    else
+      expect_arg_long=no_argument
+      arg=
       option="$(echo "$option" | sed 's,--,,')"
-      all_modules_long_options="${all_modules_long_options}
-  { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long },"
+    fi
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
       cases="${cases}
     case $n_long:// --$option"
-      let ++n_long
-      long_option="${long_option:+$long_option | --}$option"
-    else
-      if ! expr "$option" : '-.$' &>/dev/null; then
+    let ++n_long
+    long_option="${long_option:+$long_option | --}$option"
+  else
+    if ! expr "$option" : '-.$' &>/dev/null; then
+      if ! expr "$option" : '-.=' &>/dev/null; then
         echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
         exit 1
       fi
+      expect_arg=:
+      arg="$(echo "$option" | sed 's,[^=]*=,,')"
+      option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
+      echo "warning: not yet handling short-option alias =$arg" >&2
+    else
+      expect_arg=
+      arg=
       option="$(echo "$option" | sed 's,-,,')"
-      all_modules_short_options="${all_modules_short_options}$option"
+    fi
+    all_modules_short_options="${all_modules_short_options}$option$expect_arg"
       cases="${cases}
     case '$option':"
-      short_option="${short_option:+$short_option | -}$option"
-    fi
-  done
+    short_option="${short_option:+$short_option | -}$option"
+  fi
+
   while [ $# -gt 0 ]; do
+    linkopt="$1"
+    # on the RHS, we're looking for =ARG, where "ARG" is *exactly* what
+    # was given on the LHS
+    if expr "$linkopt" : '.*=' &>/dev/null; then
+      linkarg="$(echo "$linkopt" | sed 's,[^=]*=,,')"
+      if [ "$linkarg" = "$arg" ]; then
+        # we found =ARG
+        linkopt="$(echo "$linkopt" | sed 's,=.*,,')"
+      else
+        # false positive: =SOMETHING, where SOMETHING != ARG
+        linkarg=
+      fi
+    fi
     links="$links
 #line $lineno \"$kf\"
-      preemptGetopt(extra_argc, extra_argv, \"$1\");"
+      preemptGetopt(extra_argc, extra_argv, \"$linkopt\");"
+    if [ "$linkarg" ]; then
+      # include also the arg
+      links="$links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, optionarg.c_str());"
+    fi
     shift
   done
   all_modules_option_handlers="$all_modules_option_handlers$cases$links
       break;
 "
-  expect_doc=true
-  expect_doc_alternate=false
 }
 
 function warning {
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index bae0ef169..dd8a7af57 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -67,15 +67,15 @@ CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
  */
 template <class T, bool is_numeric, bool is_integer>
 struct OptionHandler {
-  static T handle(std::string option, std::string optarg);
+  static T handle(std::string option, std::string optionarg);
 };/* struct OptionHandler<> */
 
 /** Variant for integral C++ types */
 template <class T>
 struct OptionHandler<T, true, true> {
-  static T handle(std::string option, std::string optarg) {
+  static T handle(std::string option, std::string optionarg) {
     try {
-      Integer i(optarg, 10);
+      Integer i(optionarg, 10);
 
       if(! std::numeric_limits<T>::is_signed && i < 0) {
         // unsigned type but user gave negative argument
@@ -107,8 +107,8 @@ struct OptionHandler<T, true, true> {
 /** Variant for numeric but non-integral C++ types */
 template <class T>
 struct OptionHandler<T, true, false> {
-  static T handle(std::string option, std::string optarg) {
-    std::stringstream in(optarg);
+  static T handle(std::string option, std::string optionarg) {
+    std::stringstream in(optionarg);
     long double r;
     in >> r;
     if(! in.eof()) {
@@ -138,7 +138,7 @@ struct OptionHandler<T, true, false> {
 /** Variant for non-numeric C++ types */
 template <class T>
 struct OptionHandler<T, false, false> {
-  static T handle(std::string option, std::string optarg) {
+  static T handle(std::string option, std::string optionarg) {
     T::unsupported_handleOption_call___please_write_me;
     // The above line causes a compiler error if this version of the template
     // is ever instantiated (meaning that a specialization is missing).  So
@@ -151,14 +151,14 @@ struct OptionHandler<T, false, false> {
 
 /** Handle an option of type T in the default way. */
 template <class T>
-T handleOption(std::string option, std::string optarg) {
-  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg);
+T handleOption(std::string option, std::string optionarg) {
+  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optionarg);
 }
 
 /** Handle an option of type std::string in the default way. */
 template <>
-std::string handleOption<std::string>(std::string option, std::string optarg) {
-  return optarg;
+std::string handleOption<std::string>(std::string option, std::string optionarg) {
+  return optionarg;
 }
 
 /**
@@ -166,12 +166,12 @@ std::string handleOption<std::string>(std::string option, std::string optarg) {
  * If a user specifies a :handler or :predicates, it overrides this.
  */
 template <class T>
-typename T::type runHandlerAndPredicates(T, std::string option, std::string optarg, SmtEngine* smt) {
+typename T::type runHandlerAndPredicates(T, std::string option, std::string optionarg, SmtEngine* smt) {
   // By default, parse the option argument in a way appropriate for its type.
   // E.g., for "unsigned int" options, ensure that the provided argument is
   // a nonnegative integer that fits in the unsigned int type.
 
-  return handleOption<typename T::type>(option, optarg);
+  return handleOption<typename T::type>(option, optionarg);
 }
 
 template <class T>
@@ -384,6 +384,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
   for(;;) {
     int c = -1;
     optopt = 0;
+    std::string option, optionarg;
     Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl;
     if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
 #if HAVE_DECL_OPTRESET
@@ -400,6 +401,16 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
                       "+:${all_modules_short_options}",
                       cmdlineOptions, NULL);
       Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl;
+      if(optopt == 0 ||
+         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
+        // long option
+        option = argv[old_optind == 0 ? 1 : old_optind];
+        optionarg = (optarg == NULL) ? "" : optarg;
+      } else {
+        // short option
+        option = std::string("-") + char(optopt);
+        optionarg = (optarg == NULL) ? "" : optarg;
+      }
       if(optind >= extra_argc) {
         Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
         unsigned i = 1;
@@ -435,31 +446,25 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro
                       cmdlineOptions, NULL);
       main_optind = optind;
       Debug("options") << "[ next option will be at pos: " << optind << " ]" << std::endl;
-      if(optind < argc) Debug("options") << "next is option: " << argv[optind] << std::endl;
       if(c == -1) {
         Debug("options") << "done with option parsing" << std::endl;
         break;
       }
+      option = argv[old_optind == 0 ? 1 : old_optind];
+      optionarg = (optarg == NULL) ? "" : optarg;
     }
 
-    Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl;
+    Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl;
 
     switch(c) {
 ${all_modules_option_handlers}
 
-#line 451 "${template}"
+#line 463 "${template}"
 
     case ':':
       // This can be a long or short option, and the way to get at the
       // name of it is different.
-      if(optopt == 0 ||
-         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
-        // was a long option
-        throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
-      } else {
-        // was a short option
-        throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument");
-      }
+      throw OptionException(std::string("option `") + option + "' missing its required argument");
 
     case '?':
     default:
@@ -467,13 +472,13 @@ ${all_modules_option_handlers}
           !strncmp(argv[optind - 1], "--thread", 8) &&
           strlen(argv[optind - 1]) > 8 ) {
         if(! isdigit(argv[optind - 1][8])) {
-          throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
+          throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
         }
         std::vector<std::string>& threadArgv = d_holder->threadArgv;
         char *end;
         long tnum = strtol(argv[optind - 1] + 8, &end, 10);
         if(tnum < 0 || (*end != '\0' && *end != '=')) {
-          throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
+          throw OptionException(std::string("can't understand option `") + option + "': expected something like --threadN=\"--option1 --option2\", where N is a nonnegative integer");
         }
         if(threadArgv.size() <= size_t(tnum)) {
           threadArgv.resize(tnum + 1);
@@ -483,13 +488,13 @@ ${all_modules_option_handlers}
         }
         if(*end == '\0') { // e.g., we have --thread0 "foo"
           if(argc <= optind) {
-            throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+            throw OptionException(std::string("option `") + option + "' missing its required argument");
           }
           Debug("options") << "thread " << tnum << " gets option " << argv[optind] << std::endl;
           threadArgv[tnum] += argv[(*optind_ref)++];
         } else { // e.g., we have --thread0="foo"
           if(end[1] == '\0') {
-            throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+            throw OptionException(std::string("option `") + option + "' missing its required argument");
           }
           Debug("options") << "thread " << tnum << " gets option " << (end + 1) << std::endl;
           threadArgv[tnum] += end + 1;
@@ -498,14 +503,7 @@ ${all_modules_option_handlers}
         break;
       }
 
-      // This can be a long or short option, and the way to get at the name of it is different.
-      if(optopt == 0 ||
-         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
-        // was a long option
-        throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'");
-      } else { // was a short option
-        throw OptionException(std::string("can't understand option `-") + char(optopt) + "'");
-      }
+      throw OptionException(std::string("can't understand option `") + option + "'");
     }
   }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5950f568f..03aa7acc1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -584,6 +584,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = EXPR_MANAGER->mkAssociative(kind,args);
       } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
         expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
+      } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
+                   kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
+                   kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
+                 args.size() > 2 ) {
+        expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
       } else {
         PARSER_STATE->checkOperator(kind, args.size());
         expr = MK_EXPR(kind, args);
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6dbf4ed03..b14f6a9c8 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -73,7 +73,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
   if (depth == 0) {
     out << "(...)";
   } else {
-    depth --;
+    --depth;
   }
 
   // null
@@ -221,6 +221,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     case kind::APPLY:
       toStream(op, n.getOperator(), depth, types, true);
       break;
+    case kind::CHAIN:
+    case kind::DISTINCT: // chain and distinct not supported directly in CVC4, blast them away with the rewriter
+      toStream(out, theory::Rewriter::rewrite(n), depth, types, true);
+      return;
     case kind::SORT_TYPE:
     {
       string name;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 842325869..7f973aaee 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -208,6 +208,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY: break;
   case kind::EQUAL:
   case kind::DISTINCT: out << smtKindString(k) << " "; break;
+  case kind::CHAIN: break;
   case kind::TUPLE: break;
 
     // bool theory
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e28520e70..364a786cf 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1656,7 +1656,6 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.isNull() || e.getExprManager() == d_exprManager);
 
   SmtScope smts(this);
-
   finalOptionsAreSet();
   doPendingPops();
 
@@ -1725,7 +1724,6 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
 
   SmtScope smts(this);
-
   finalOptionsAreSet();
   doPendingPops();
 
@@ -2159,11 +2157,11 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
 
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
+  SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }
-  SmtScope smts(this);
   Trace("smt") << "SMT getAssertions()" << endl;
   if(!options::interactive()) {
     const char* msg =
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index deec881e4..187b29114 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -46,7 +46,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     Dump("benchmark") << SetOptionCommand(key, value);
   }
 
-  string optarg = value.getValue();
+  string optionarg = value.getValue();
 
   ${smt_setoption_handlers}
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 1218f3809..da31d157f 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,6 +300,8 @@ operator TUPLE 1: "a tuple"
 
 operator LAMBDA 2 "lambda"
 
+parameterized CHAIN BUILTIN 2: "chain operator"
+
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashFunction \
@@ -342,6 +344,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index f62140263..a23a1b8f2 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -51,6 +51,25 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
   return out;
 }
 
+Node TheoryBuiltinRewriter::blastChain(TNode in) {
+
+  Assert(in.getKind() == kind::CHAIN);
+
+  Kind chainedOp = in.getOperator().getConst<Kind>();
+
+  if(in.getNumChildren() == 2) {
+    // if this is the case exactly 1 pair will be generated so the
+    // AND is not required
+    return NodeManager::currentNM()->mkNode(chainedOp, in[0], in[1]);
+  } else {
+    NodeBuilder<> conj(kind::AND);
+    for(TNode::iterator i = in.begin(), j = i + 1; j != in.end(); ++i, ++j) {
+      conj << NodeManager::currentNM()->mkNode(chainedOp, *i, *j);
+    }
+    return conj;
+  }
+}
+
 }/* CVC4::theory::builtin namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index acf535388..b7199474b 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -32,22 +32,29 @@ namespace builtin {
 class TheoryBuiltinRewriter {
 
   static Node blastDistinct(TNode node);
+  static Node blastChain(TNode node);
 
 public:
 
-  static inline RewriteResponse postRewrite(TNode node) {
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  static inline RewriteResponse preRewrite(TNode node) {
+  static inline RewriteResponse doRewrite(TNode node) {
     switch(node.getKind()) {
     case kind::DISTINCT:
       return RewriteResponse(REWRITE_DONE, blastDistinct(node));
+    case kind::CHAIN:
+      return RewriteResponse(REWRITE_DONE, blastChain(node));
     default:
       return RewriteResponse(REWRITE_DONE, node);
     }
   }
 
+  static inline RewriteResponse postRewrite(TNode node) {
+    return doRewrite(node);
+  }
+
+  static inline RewriteResponse preRewrite(TNode node) {
+    return doRewrite(node);
+  }
+
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index b7fd3c351..97af23f67 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -24,6 +24,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "expr/expr.h"
+#include "theory/rewriter.h"
 
 #include <sstream>
 
@@ -168,6 +169,54 @@ public:
   }
 };/* class LambdaTypeRule */
 
+class ChainTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::CHAIN);
+
+    if(!check) {
+      return nodeManager->booleanType();
+    }
+
+    TypeNode tn;
+    try {
+      // Actually do the expansion to do the typechecking.
+      // Shouldn't be extra work to do this, since the rewriter
+      // keeps a cache.
+      tn = nodeManager->getType(Rewriter::rewrite(n), check);
+    } catch(TypeCheckingExceptionPrivate& e) {
+      std::stringstream ss;
+      ss << "Cannot typecheck the expansion of chained operator `" << n.getOperator() << "':"
+         << std::endl;
+      // indent the sub-exception for clarity
+      std::stringstream ss2;
+      ss2 << e;
+      std::string eStr = ss2.str();
+      for(size_t i = eStr.find('\n'); i != std::string::npos; i = eStr.find('\n', i)) {
+        eStr.insert(++i, "| ");
+      }
+      ss << "| " << eStr;
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+
+    // This check is intentionally != booleanType() rather than
+    // !(...isBoolean()): if we ever add a type compatible with
+    // Boolean (pseudobooleans or whatever), we have to revisit
+    // the above "!check" case where booleanType() is returned
+    // directly.  Putting this check here will cause a failure if
+    // it's ever relevant.
+    if(tn != nodeManager->booleanType()) {
+      std::stringstream ss;
+      ss << "Chains can only be formed over predicates; "
+         << "the operator here returns `" << tn << "', expected `"
+         << nodeManager->booleanType() << "'.";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+
+    return nodeManager->booleanType();
+  }
+};/* class ChainTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d531a79a4..50527e51a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -127,7 +127,8 @@ BUG_TESTS = \
 	bug322b.cvc \
 	bug339.smt2 \
 	bug365.smt2 \
-	bug382.smt2
+	bug382.smt2 \
+	bug383.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug383.smt2 b/test/regress/regress0/bug383.smt2
new file mode 100644
index 000000000..b0349c008
--- /dev/null
+++ b/test/regress/regress0/bug383.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(declare-fun f1 () Int)
+(declare-fun f2 () Int)
+(declare-fun f3 () Int)
+(assert (< 1 f1 f2 f3 5))
+(check-sat)
+(exit)