From b5fe473c3ac99b012d6cc945bd5ca0109e9f7f3b Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 1 Jun 2016 17:50:45 -0400
Subject: [PATCH] fix compilation errors after merge

---
 src/parsers/smt2/smt2parser.cpp | 3 ---
 src/smt/theory_str.cpp          | 4 ++++
 src/smt/theory_str.h            | 1 +
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index c203b2faa..c8e9a78b6 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1767,9 +1767,6 @@ namespace smt2 {
                         case scanner::BV_TOKEN:
                             parse_bv_numeral();
                             break;
-                        case scanner::STRING_TOKEN:
-                            parse_string();
-                            break;
                         case scanner::LEFT_PAREN:
                             push_expr_frame(m_num_expr_frames == 0 ? 0 : static_cast<expr_frame*>(m_stack.top()));
                             break;
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index f7d31a80b..b65b799b1 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4962,4 +4962,8 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
 
 void theory_str::finalize_model(model_generator & mg) {}
 
+void theory_str::display(std::ostream & out) const {
+    out << "TODO: theory_str display" << std::endl;
+}
+
 }; /* namespace smt */
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 45c5f3e06..ecd7e443f 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -220,6 +220,7 @@ namespace smt {
         virtual ~theory_str();
 
         virtual char const * get_name() const { return "strings"; }
+        virtual void display(std::ostream & out) const;
     protected:
         virtual bool internalize_atom(app * atom, bool gate_ctx);
         virtual bool internalize_term(app * term);