5 files changed, 83 insertions, 8 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 6430814a5..5fcc8833a 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -3,7 +3,8 @@ TEST_EXTENSIONS = .class
 CPLUSPLUS_TESTS = \
 	boilerplate \
 	ouroborous \
-	two_smt_engines
+	two_smt_engines \
+	smt2_compliance
 #	cvc3_main
 
 TESTS = $(CPLUSPLUS_TESTS)
diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
new file mode 100644
index 000000000..65dd52193
--- /dev/null
+++ b/test/system/smt2_compliance.cpp
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/*! \file smt2_compliance.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** 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
+ ** information.\endverbatim
+ **
+ ** \brief A test of SMT-LIBv2 commands, checks for compliant output
+ **
+ ** A test of SMT-LIBv2 commands, checks for compliant output.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <cassert>
+
+#include "smt/options.h"
+#include "parser/parser.h"
+#include "expr/expr_manager.h"
+#include "expr/command.h"
+#include "smt/smt_engine.h"
+#include "parser/parser_builder.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace std;
+
+void testGetInfo(SmtEngine& smt, const char* s);
+
+int main() {
+  Options opts;
+  opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
+  opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2);
+
+  cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+
+  ExprManager em(opts);
+  SmtEngine smt(&em);
+
+  testGetInfo(smt, ":error-behavior");
+  testGetInfo(smt, ":name");
+  testGetInfo(smt, ":authors");
+  testGetInfo(smt, ":version");
+  testGetInfo(smt, ":status");
+  testGetInfo(smt, ":reason-unknown");
+  testGetInfo(smt, ":arbitrary-undefined-keyword");
+  testGetInfo(smt, ":56");// legal
+  testGetInfo(smt, ":<=");// legal
+  testGetInfo(smt, ":->");// legal
+  testGetInfo(smt, ":all-statistics");
+
+  return 0;
+}
+
+void testGetInfo(SmtEngine& smt, const char* s) {
+  ParserBuilder pb(smt.getExprManager(), "<internal>", smt.getExprManager()->getOptions());
+  Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
+  assert(p != NULL);
+  Command* c = p->nextCommand();
+  assert(c != NULL);
+  cout << c << endl;
+  stringstream ss;
+  c->invoke(&smt, ss);
+  assert(p->nextCommand() == NULL);
+  delete p;
+
+  cout << ss.str() << endl << endl;
+}
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 7773644da..d905923e2 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -26,7 +26,7 @@
 #include "main/interactive_shell.h"
 #include "parser/parser_builder.h"
 #include "util/language.h"
-#include "util/options.h"
+#include "options/options.h"
 
 using namespace CVC4;
 using namespace std;
@@ -59,9 +59,9 @@ private:
     d_exprManager = new ExprManager;
     d_sin = new stringstream;
     d_sout = new stringstream;
-    d_options.in = d_sin;
-    d_options.out = d_sout;
-    d_options.inputLanguage = language::input::LANG_CVC4;
+    d_options.set(options::in, d_sin);
+    d_options.set(options::out, d_sout);
+    d_options.set(options::inputLanguage, language::input::LANG_CVC4);
   }
 
   void tearDown() {
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 91af11561..01879ec49 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -27,7 +27,7 @@
 #include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
 #include "expr/command.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/output.h"
 #include "util/language.h"
 
@@ -184,7 +184,7 @@ protected:
 
   void setUp() {
     d_exprManager = new ExprManager;
-    d_options.parseOnly = true;
+    d_options.set(options::parseOnly, true);
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index ee637daac..eb6e5eefb 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -38,7 +38,7 @@
 #include "smt/smt_engine_scope.h"
 #include "util/rational.h"
 #include "util/integer.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/Assert.h"
 
 using namespace CVC4;