diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index 5fdd53d70..fe326ab22 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -80,8 +80,8 @@ namespace smt {
                 expr * arg2   = m_app2->get_arg(i);
                 if (arg1 != arg2) {
                     app * eq  = ctx.mk_eq_atom(arg1, arg2);
-                    app * neq = m.mk_not(eq);
-                    if (std::find(lits.begin(), lits.end(), neq) == lits.end()) {
+                    app_ref neq(m.mk_not(eq), m);
+                    if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) {
                         lits.push_back(neq);
                         prs.push_back(mk_hypothesis(m, eq, false, arg1, arg2));
                     }
@@ -398,7 +398,7 @@ namespace smt {
     }
 
     literal dyn_ack_manager::mk_eq(expr * n1, expr * n2) {
-		app_ref eq(m_context.mk_eq_atom(n1, n2), m);
+		app_ref eq(m.mk_eq(n1, n2), m);
         m_context.internalize(eq, true);
         literal l = m_context.get_literal(eq);
         TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: "; 
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a69014c4e..16ed92546 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3028,9 +3028,11 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
     if (n1 != n2 && m_util.is_seq(e1)) {
         theory_var v1 = n1->get_th_var(get_id());
         theory_var v2 = n2->get_th_var(get_id());
-        if (m_find.find(v1) == m_find.find(v2)) {
+        if (v1 == null_theory_var || v2 == null_theory_var)
             return;
-        }
+        if (m_find.find(v1) == m_find.find(v2)) 
+            return;
+        
         m_find.merge(v1, v2);
         expr_ref o1(e1, m);
         expr_ref o2(e2, m);
@@ -3049,7 +3051,8 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
     enode* n2 = get_enode(v2);    
     expr_ref e1(n1->get_owner(), m);
     expr_ref e2(n2->get_owner(), m);
-    SASSERT(n1->get_root() != n2->get_root());
+    if (n1->get_root() == n2->get_root())
+        return;
     if (m_util.is_re(n1->get_owner())) {        
         m_regex.propagate_ne(e1, e2);
         return;