From df2a569d25afdd15edd6e9fa495f9d8238e4886c Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 24 Oct 2016 13:29:17 +0100
Subject: [PATCH 1/2] Replaced antiquated header with modern equivalent.

---
 src/cmd_context/check_logic.cpp | 34 ++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index d9fe9ab72..d598dfa39 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -24,7 +24,7 @@ Revision History:
 #include"datatype_decl_plugin.h"
 #include"ast_pp.h"
 #include"for_each_expr.h"
-#include<strstream>
+#include<sstream>
 
 struct check_logic::imp {
     ast_manager & m;
@@ -189,7 +189,7 @@ struct check_logic::imp {
         else {
             m_unknown_logic = true;
         }
-        
+
         m_logic = logic;
     }
 
@@ -237,7 +237,7 @@ struct check_logic::imp {
         }
     }
 
-    void operator()(var * n) { 
+    void operator()(var * n) {
         if (!m_quantifiers)
             fail("logic does not support quantifiers");
         check_sort(m.get_sort(n));
@@ -279,7 +279,7 @@ struct check_logic::imp {
             }
         }
     }
-    
+
     // check if the divisor is a numeral
     void check_div(app * n) {
         SASSERT(n->get_num_args() == 2);
@@ -328,8 +328,8 @@ struct check_logic::imp {
                     return false;
                 non_numeral = arg;
             }
-            if (non_numeral == 0) 
-                return true; 
+            if (non_numeral == 0)
+                return true;
             if (is_diff_var(non_numeral))
                 return true;
             if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))
@@ -338,10 +338,10 @@ struct check_logic::imp {
         }
         return true;
     }
-    
+
     bool is_diff_arg(expr * t) {
         if (is_diff_var(t))
-            return true; 
+            return true;
         if (is_numeral(t))
             return true;
         if (m_a_util.is_add(t) || m_a_util.is_sub(t))
@@ -366,7 +366,7 @@ struct check_logic::imp {
         expr * t1 = to_app(lhs)->get_arg(0);
         expr * t2 = to_app(lhs)->get_arg(1);
         if (is_diff_var(t1) && is_diff_var(t2))
-            return; 
+            return;
         if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) {
             // QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c)
             if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args())
@@ -391,7 +391,7 @@ struct check_logic::imp {
                 check_diff_arg(n);
         }
     }
-    
+
     void operator()(app * n) {
         sort * s = m.get_sort(n);
         check_sort(s);
@@ -415,18 +415,18 @@ struct check_logic::imp {
             if (!m_ints || !m_reals) {
                 if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n))
                     fail("logic does not support casting operators");
-            }                
+            }
         }
         else if (fid == m_bv_util.get_family_id()) {
-            // nothing to check... 
+            // nothing to check...
         }
         else if (fid == m_ar_util.get_family_id()) {
-            // nothing to check... 
+            // nothing to check...
             if (m_diff)
                 check_diff_args(n);
         }
         else if (fid == m.get_basic_family_id()) {
-            // nothing to check... 
+            // nothing to check...
             if (m_diff) {
                 if (m.is_eq(n))
                     check_diff_predicate(n);
@@ -449,8 +449,8 @@ struct check_logic::imp {
             fail(strm.str().c_str());
         }
     }
-    
-    void operator()(quantifier * n) { 
+
+    void operator()(quantifier * n) {
         if (!m_quantifiers)
             fail("logic does not support quantifiers");
     }
@@ -490,7 +490,7 @@ struct check_logic::imp {
 check_logic::check_logic() {
     m_imp = 0;
 }
-   
+
 check_logic::~check_logic() {
     if (m_imp)
         dealloc(m_imp);

From 79f1d7b4d40781932c44aaaa31f13d9ce7e1865f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 24 Oct 2016 15:27:47 +0100
Subject: [PATCH 2/2] fixed GCC build issue in tests

---
 src/test/sorting_network.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index 8b2aadee3..a64d3a70f 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -416,7 +416,7 @@ static void test_at_most1() {
     for (unsigned i = 0; i < 5; ++i) {
         in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
     }
-    in[4] = in[3];
+    in[4] = in[3].get();
 
     ast_ext2 ext(m);
     psort_nw<ast_ext2> sn(ext);