Revert "make smtlib-model-format default for yices-smt2"

This reverts commit 7320e76.

doc/manual/manual.tex

@@ -3703,7 +3703,7 @@ \subsubsection*{Model Format}
 To use this format, you must invoke \texttt{yices-smt2} as follows
 \begin{small}
 \begin{lstlisting}[language=sh]
-   yices-smt2 --yices-model-format
+   yices-smt2 --smt2-model-format
 \end{lstlisting}
 \end{small}
 
@@ -3856,7 +3856,7 @@ \subsubsection*{All Command-line Options}
   after all commands have been executed (i.e., after reaching the
   command \texttt{(exit)} or the end of the input file).
 
-\item[--yices-model-format] Display models in the Yices model format.
+\item[--smt2-model-format] Display models in the SMT-LIB~2 format.
 
 \item[--bvconst-in-decimal] Prints bit-vector constants as numbers
   (using the SMT-LIB~2 decimal syntax), instead of constants in binary

doc/yices-smt2.1

@@ -53,8 +53,8 @@ to true.
 .B \-\-mcsat
 Force use of the MCSAT solver.
 .TP
-.B \-\-yices-model-format
-Print models in the Yices model format (instead of the SMT-LIB format)..
+.B \-\-smt2-model-format
+Print models in the SMT-LIB format (instead of the default Yices format)..
 .TP
 .B \-\-bvconst-in-decimal
 Print bitvector constants using the SMT-LIB decimal format, instead of the binary format.

src/frontend/yices_smt2.c

@@ -154,7 +154,7 @@ typedef enum optid {
   verbosity_opt,           // set verbosity on the command line
   incremental_opt,         // enable incremental mode
   interactive_opt,         // enable interactive mode
-  yicesformat_opt,         // use the Yices model format for models
+  smt2format_opt,          // use SMT-LIB2 format for models
   bvdecimal_opt,           // use (_ bv<xxx> n) for bit-vector constants
   timeout_opt,             // give a timeout
   delegate_opt,            // use an external sat solver
@@ -203,7 +203,7 @@ static option_desc_t options[NUM_OPTIONS] = {
   { "timeout", 't', MANDATORY_INT, timeout_opt },
   { "incremental", '\0', FLAG_OPTION, incremental_opt },
   { "interactive", '\0', FLAG_OPTION, interactive_opt },
-  { "yices-model-format", '\0', FLAG_OPTION, yicesformat_opt },
+  { "smt2-model-format", '\0', FLAG_OPTION, smt2format_opt },
   { "bvconst-in-decimal", '\0', FLAG_OPTION, bvdecimal_opt },
   { "delegate", '\0', MANDATORY_STRING, delegate_opt },
   { "dimacs", '\0', MANDATORY_STRING, dimacs_opt },
@@ -267,7 +267,7 @@ static void print_help(const char *progname) {
          "    --stats, -s               Print statistics once all commands have been processed\n"
          "    --incremental             Enable support for push/pop\n"
          "    --interactive             Run in interactive mode (ignored if a filename is given)\n"
-         "    --yices-model-format      Display models in the Yices model format (default = false)\n"
+         "    --smt2-model-format       Display models in the SMT-LIB 2 format (default = false)\n"
          "    --bvconst-in-decimal      Display bit-vector constants as decimal numbers (default = false)\n"
          "    --delegate=<satsolver>    Use an external SAT solver (can be cadical, cryptominisat, kissat, or y2sat)\n"
          "    --dimacs=<filename>       Bitblast and export to a file (in DIMACS format)\n"
@@ -374,7 +374,7 @@ static void parse_command_line(int argc, char *argv[]) {
   filename = NULL;
   incremental = false;
   interactive = false;
-  smt2_model_format = true;
+  smt2_model_format = false;
   bvdecimal = false;
   show_stats = false;
   verbosity = 0;
@@ -523,8 +523,8 @@ static void parse_command_line(int argc, char *argv[]) {
         }
         break;
 
-      case yicesformat_opt:
-        smt2_model_format = false;
+      case smt2format_opt:
+        smt2_model_format = true;
         break;
 
       case bvdecimal_opt:

tests/regress/coverage/smtlib/QF_RDL/SMT-Temporal-Planning-Benchmarks/cooking09.smt2.options

@@ -0,0 +1 @@
+--smt2-model-format

tests/regress/coverage/smtlib/QF_RDL/SMT-Temporal-Planning-Benchmarks/tms-2-3-light-03.smt2.options

@@ -0,0 +1 @@
+--smt2-model-format

tests/regress/mcsat/bool/assumptions/test01.smt2.options

@@ -1 +1 @@
---mcsat --yices-model-format --trace mcsat::interpolant::check
+--mcsat --trace mcsat::interpolant::check

tests/regress/mcsat/bool/assumptions/test01m.smt2.options

@@ -1 +1 @@
---mcsat --yices-model-format --trace mcsat::interpolant::check
+--mcsat --trace mcsat::interpolant::check

tests/regress/mcsat/bv/assumptions/issue233.smt2.options

@@ -1 +1 @@
---mcsat --incremental --yices-model-format --trace mcsat::interpolant::check
+--mcsat --incremental --trace mcsat::interpolant::check

tests/regress/mcsat/bv/assumptions/test01m.smt2.options

@@ -1 +1 @@
---mcsat --yices-model-format --trace mcsat::interpolant::check
+--mcsat --trace mcsat::interpolant::check

tests/regress/mcsat/lra/assumptions/test01m.smt2.options

@@ -1 +1 @@
---mcsat --yices-model-format --trace mcsat::interpolant::check
+--mcsat --trace mcsat::interpolant::check

tests/regress/mcsat/nra/incremental/incremental00.smt2.options

@@ -1 +1 @@
---incremental --yices-model-format
+--incremental

tests/regress/mcsat/nra/incremental/incremental02.smt2.options

@@ -1 +1 @@
---incremental --yices-model-format
+--incremental

tests/regress/wd/example_mdl.smt2.options

@@ -0,0 +1 @@
+--smt2-model-format

tests/regress/wd/example_mdl2.smt2.options

@@ -1 +1 @@
---bvconst-in-decimal
+--smt2-model-format --bvconst-in-decimal