diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs
index 2f5cd0ce8..df90f9cd4 100644
--- a/src/api/dotnet/FuncDecl.cs
+++ b/src/api/dotnet/FuncDecl.cs
@@ -342,6 +342,5 @@ namespace Microsoft.Z3
             Context.CheckContextMatch<Expr>(args);
             return Expr.Create(Context, this, args);
         }
-
     }
 }
diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp
index 8d90f9583..ade667e34 100644
--- a/src/smt/smt_conflict_resolution.cpp
+++ b/src/smt/smt_conflict_resolution.cpp
@@ -1405,6 +1405,7 @@ namespace smt {
             switch (js.get_kind()) {
             case b_justification::CLAUSE: {
                 clause * cls = js.get_clause();
+                TRACE("unsat_core_bug", m_ctx.display_clause_detail(tout, cls););
                 unsigned num_lits = cls->get_num_literals();
                 unsigned i        = 0;
                 if (consequent != false_literal) {
@@ -1422,8 +1423,9 @@ namespace smt {
                     process_antecedent_for_unsat_core(~l);
                 }
                 justification * js = cls->get_justification();
-                if (js)
+                if (js) {
                     process_justification_for_unsat_core(js);
+                }
                 break;
             }
             case b_justification::BIN_CLAUSE:
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3f8845546..af8b9e395 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -3567,8 +3567,8 @@ void theory_seq::add_at_axiom(expr* e) {
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
     add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
 
-    add_axiom(i_ge_0, mk_eq(s, emp, false));
-    add_axiom(~i_ge_len_s, mk_eq(s, emp, false));
+    add_axiom(i_ge_0, mk_eq(e, emp, false));
+    add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
 }
 
 /**