summaryrefslogtreecommitdiff
path: root/src/main/interactive_shell.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r--src/main/interactive_shell.cpp16
1 files changed, 8 insertions, 8 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b0934c0ee..719c8f61d 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -5,7 +5,7 @@
** Major contributors: mdeters
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -64,9 +64,9 @@ static const std::string cvc_commands[] = {
#include "main/cvc_tokens.h"
};/* cvc_commands */
-static const std::string smt_commands[] = {
-#include "main/smt_tokens.h"
-};/* smt_commands */
+static const std::string smt1_commands[] = {
+#include "main/smt1_tokens.h"
+};/* smt1_commands */
static const std::string smt2_commands[] = {
#include "main/smt2_tokens.h"
@@ -105,10 +105,10 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
commandsBegin = cvc_commands;
commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
break;
- case output::LANG_SMTLIB:
- d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib";
- commandsBegin = smt_commands;
- commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
+ case output::LANG_SMTLIB_V1:
+ d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
+ commandsBegin = smt1_commands;
+ commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
break;
case output::LANG_SMTLIB_V2:
d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback