From 519d308b8645525dbe1822a25210bb509a9a1723 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 28 Nov 2012 14:59:39 +0000 Subject: [PATCH] Java API: bugfixes Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 4 ++-- src/api/java/Context.java | 18 +++++------------- 2 files changed, 7 insertions(+), 15 deletions(-) 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();