From ed5137ffd22b9dd0721869e7547b06bb8d4479ab Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 1 Nov 2016 11:23:42 +0000
Subject: [PATCH 1/2] build fix

---
 src/test/sorting_network.cpp | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index a64d3a70f..81340651a 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -22,7 +22,7 @@ struct ast_ext {
     ast_ext(ast_manager& m):m(m) {}
     typedef expr* T;
     typedef expr_ref_vector vector;
-    T mk_ite(T a, T b, T c) { 
+    T mk_ite(T a, T b, T c) {
         return m.mk_ite(a, b, c);
     }
     T mk_le(T a, T b) {
@@ -34,7 +34,7 @@ struct ast_ext {
     }
     T mk_default() {
         return m.mk_false();
-    }        
+    }
 };
 
 
@@ -164,17 +164,17 @@ struct ast_ext2 {
 
     literal mk_false() { return m.mk_false(); }
     literal mk_true() { return m.mk_true(); }
-    literal mk_max(literal a, literal b) { 
-        return trail(m.mk_or(a, b)); 
+    literal mk_max(literal a, literal b) {
+        return trail(m.mk_or(a, b));
     }
     literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
-    literal mk_not(literal a) { if (m.is_not(a,a)) return a; 
-        return trail(m.mk_not(a)); 
+    literal mk_not(literal a) { if (m.is_not(a,a)) return a;
+        return trail(m.mk_not(a));
     }
     std::ostream& pp(std::ostream& out, literal lit) {
         return out << mk_pp(lit, m);
     }
-    literal fresh() { 
+    literal fresh() {
         return trail(m.mk_fresh_const("x", m.mk_bool_sort()));
     }
     void mk_clause(unsigned n, literal const* lits) {
@@ -200,7 +200,7 @@ static void test_sorting_eq(unsigned n, unsigned k) {
     // equality:
     std::cout << "eq " << k << "\n";
     solver.push();
-    result = sn.eq(k, in.size(), in.c_ptr());
+    result = sn.eq(true, k, in.size(), in.c_ptr());
     solver.assert_expr(result);
     for (unsigned i = 0; i < ext.m_clauses.size(); ++i) {
         solver.assert_expr(ext.m_clauses[i].get());
@@ -210,7 +210,7 @@ static void test_sorting_eq(unsigned n, unsigned k) {
 
     solver.push();
     for (unsigned i = 0; i < k; ++i) {
-        solver.assert_expr(in[i].get());        
+        solver.assert_expr(in[i].get());
     }
     res = solver.check();
     SASSERT(res == l_true);
@@ -256,7 +256,7 @@ static void test_sorting_le(unsigned n, unsigned k) {
     SASSERT(res == l_true);
 
     for (unsigned i = 0; i < k; ++i) {
-        solver.assert_expr(in[i].get());        
+        solver.assert_expr(in[i].get());
     }
     res = solver.check();
     SASSERT(res == l_true);
@@ -304,7 +304,7 @@ void test_sorting_ge(unsigned n, unsigned k) {
 
     solver.push();
     for (unsigned i = 0; i < n - k; ++i) {
-        solver.assert_expr(m.mk_not(in[i].get()));        
+        solver.assert_expr(m.mk_not(in[i].get()));
     }
     res = solver.check();
     SASSERT(res == l_true);
@@ -350,10 +350,10 @@ void test_at_most_1(unsigned n, bool full) {
     for (unsigned i = 0; i < n; ++i) {
         in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
     }
-    
+
     ast_ext2 ext(m);
     psort_nw<ast_ext2> sn(ext);
-    expr_ref result1(m), result2(m);    
+    expr_ref result1(m), result2(m);
     result1 = sn.le(full, 1, in.size(), in.c_ptr());
     result2 = naive_at_most1(in);
 
@@ -368,12 +368,12 @@ void test_at_most_1(unsigned n, bool full) {
     if (full) {
         solver.push();
         solver.assert_expr(m.mk_not(m.mk_eq(result1, result2)));
-        
+
         std::cout << result1 << "\n";
-        
+
         res = solver.check();
         SASSERT(res == l_false);
-    
+
         solver.pop(1);
     }
 

From 026309a325e0357bf62f63f690702ce676bdf000 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 1 Nov 2016 14:21:06 +0000
Subject: [PATCH 2/2] bugfix for disequality propagation in smt_context

---
 src/smt/smt_context.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 154f3a6a3..6b3d92602 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1112,6 +1112,7 @@ namespace smt {
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
             theory_id  t1 = r1->m_th_var_list.get_th_id();
+            if (t1 == null_theory_id) return false;
             return get_theory(t1)->use_diseqs();
         }