diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index a721c53d2..d0bdcf8d4 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -806,7 +806,6 @@ class JavaExample
     {
         System.out.println("BasicTests");
 
-        Symbol qi = ctx.MkSymbol(1);
         Symbol fname = ctx.MkSymbol("f");
         Symbol x = ctx.MkSymbol("x");
         Symbol y = ctx.MkSymbol("y");
@@ -2207,7 +2206,8 @@ class JavaExample
         } catch (Z3Exception ex)
         {
             System.out.println("Z3 Managed Exception: " + ex.getMessage());
-            System.out.println("Stack trace: " + ex.getStackTrace());
+            System.out.println("Stack trace: ");
+            ex.printStackTrace(System.out);            
         } catch (TestFailedException ex)
         {
             System.out.println("TEST CASE FAILED: " + ex.getMessage());
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index d289d956f..3519900cd 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2974,23 +2974,15 @@ public class Context extends IDisposable
 
 	void CheckContextMatch(Z3Object other) throws Z3Exception
 	{
-
-		if (this == other.Context())
-			throw new Z3Exception("Context mismatch");
+	    if (this != other.Context())
+		throw new Z3Exception("Context mismatch");
 	}
 
 	void CheckContextMatch(Z3Object[] arr) throws Z3Exception
 	{
-
-		if (arr != null)
-		{
-			for (Z3Object a : arr)
-			{
-				// It was an assume, now we added the precondition, and we made
-				// it into an assert
-				CheckContextMatch(a);
-			}
-		}
+	    if (arr != null)
+		for (Z3Object a : arr)
+		    CheckContextMatch(a);
 	}
 
 	private ASTDecRefQueue m_AST_DRQ = new ASTDecRefQueue();