2 files changed, 31 insertions, 36 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 08146760f..35211a49a 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -16,30 +16,29 @@
 
 #include "compat/cvc3_compat.h"
 
-#include "expr/kind.h"
-#include "expr/command.h"
+#include <algorithm>
+#include <cassert>
+#include <iostream>
+#include <iterator>
+#include <sstream>
+#include <string>
 
-#include "util/rational.h"
-#include "util/integer.h"
+#include "base/output.h"
+#include "expr/kind.h"
+#include "expr/predicate.h"
+#include "expr/sexpr.h"
+#include "options/expr_options.h"
+#include "options/parser_options.h"
+#include "options/smt_options.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+#include "smt_util/command.h"
 #include "util/bitvector.h"
 #include "util/hash.h"
+#include "util/integer.h"
+#include "util/rational.h"
 #include "util/subrange_bound.h"
-#include "util/predicate.h"
-#include "util/output.h"
-
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-
-#include "parser/options.h"
-#include "smt/options.h"
-#include "expr/options.h"
 
-#include <iostream>
-#include <string>
-#include <sstream>
-#include <algorithm>
-#include <iterator>
-#include <cassert>
 
 using namespace std;
 
@@ -2498,8 +2497,8 @@ void ValidityChecker::loadFile(const std::string& fileName,
   CVC4::Options opts = d_em->getOptions();
   stringstream langss;
   langss << lang;
-  d_smt->setOption("input-language", langss.str());
-  d_smt->setOption("interactive-mode", string(interactive ? "true" : "false"));
+  d_smt->setOption("input-language", CVC4::SExpr(langss.str()));
+  d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false));
   CVC4::parser::ParserBuilder parserBuilder(d_em, fileName, opts);
   CVC4::parser::Parser* p = parserBuilder.build();
   p->useDeclarationsFrom(d_parserContext);
@@ -2513,8 +2512,8 @@ void ValidityChecker::loadFile(std::istream& is,
   CVC4::Options opts = d_em->getOptions();
   stringstream langss;
   langss << lang;
-  d_smt->setOption("input-language", langss.str());
-  d_smt->setOption("interactive-mode", string(interactive ? "true" : "false"));
+  d_smt->setOption("input-language", CVC4::SExpr(langss.str()));
+  d_smt->setOption("interactive-mode", CVC4::SExpr(interactive ? true : false));
   CVC4::parser::ParserBuilder parserBuilder(d_em, "[stream]", opts);
   CVC4::parser::Parser* p = parserBuilder.withStreamInput(is).build();
   d_parserContext = p;
diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index 0fa4a7ce5..5fefa6871 100644
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -48,23 +48,19 @@
 #define _cvc3__include__queryresult_h_
 #define _cvc3__include__formula_value_h_
 
-#include "expr/expr_manager.h"
+#include <stdlib.h>
+#include <map>
+#include <utility>
+
+#include "base/exception.h"
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "expr/type.h"
-
+#include "parser/parser.h"
 #include "smt/smt_engine.h"
-
-#include "util/rational.h"
-#include "util/integer.h"
-
-#include "util/exception.h"
 #include "util/hash.h"
-
-#include "parser/parser.h"
-
-#include <stdlib.h>
-#include <map>
-#include <utility>
+#include "util/integer.h"
+#include "util/rational.h"
 
 //class CInterface;