diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 954f0a85a..a74ab90c1 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1048,7 +1048,6 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
         return s2;
     }
     std::ostringstream buffer;
-    SASSERT(false);
     buffer << "Sorts " << mk_pp(s1, *m_manager) << " and " << mk_pp(s2, *m_manager) << " are incompatible";
     throw ast_exception(buffer.str().c_str());
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index e286add3f..5472583ff 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -584,9 +584,9 @@ bool theory_seq::check_extensionality() {
             for (unsigned i = 0; i < seqs.size(); ++i) {
                 enode* n2 = get_enode(seqs[i]);
                 expr* o2 = n2->get_owner();
-				if (m.get_sort(o1) != m.get_sort(o2)) {
-					continue;
-				}
+                if (m.get_sort(o1) != m.get_sort(o2)) {
+                    continue;
+                }
                 if (m_exclude.contains(o1, o2)) {
                     continue;
                 }