From bbfd9dd19f03c62db5fc14b6e9db48af96842dfc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 28 Nov 2012 22:20:36 +0000 Subject: [PATCH] Java API: bugfixes Signed-off-by: Christoph M. Wintersteiger --- examples/java/JavaExample.java | 18 +++++++++++------- src/api/java/Context.java | 6 +++--- src/api/java/Expr.java | 4 ---- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index d0bdcf8d4..7e403fecd 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -882,10 +882,10 @@ class JavaExample Expr inum = rn.Numerator(); Expr iden = rn.Denominator(); System.out.println("Numerator: " + inum + " Denominator: " + iden); - if (inum.toString() != "42" || iden.toString() != "43") + if (!inum.toString().equals("42") || !iden.toString().equals("43")) throw new TestFailedException(); - if (rn.ToDecimalString(3) != "0.976?") + if (!rn.ToDecimalString(3).toString().equals("0.976?")) throw new TestFailedException(); BigIntCheck(ctx, ctx.MkReal("-1231231232/234234333")); @@ -895,23 +895,23 @@ class JavaExample String bn = "1234567890987654321"; - if (ctx.MkInt(bn).BigInteger().toString() != bn) + if (!ctx.MkInt(bn).BigInteger().toString().equals(bn)) throw new TestFailedException(); - if (ctx.MkBV(bn, 128).BigInteger().toString() != bn) + if (!ctx.MkBV(bn, 128).BigInteger().toString().equals(bn)) throw new TestFailedException(); - if (ctx.MkBV(bn, 32).BigInteger().toString() == bn) + if (ctx.MkBV(bn, 32).BigInteger().toString().equals(bn)) throw new TestFailedException(); // Error handling test. try { - Expr plus_ri = ctx.MkAdd(new ArithExpr[] { ctx.MkInt(1), - ctx.MkReal(2) }); + IntExpr i = ctx.MkInt("0.5"); throw new TestFailedException(); // unreachable } catch (Z3Exception e) { + System.out.println("GOT: " + e.getMessage()); } } @@ -2211,9 +2211,13 @@ class JavaExample } catch (TestFailedException ex) { System.out.println("TEST CASE FAILED: " + ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); } catch (Exception ex) { System.out.println("Unknown Exception: " + ex.getMessage()); + System.out.println("Stack trace: "); + ex.printStackTrace(System.out); } } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b903f71e0..c3fbeab15 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -86,7 +86,6 @@ public class Context extends IDisposable **/ public BoolSort BoolSort() throws Z3Exception { - if (m_boolSort == null) m_boolSort = new BoolSort(this); return m_boolSort; @@ -97,7 +96,6 @@ public class Context extends IDisposable **/ public IntSort IntSort() throws Z3Exception { - if (m_intSort == null) m_intSort = new IntSort(this); return m_intSort; @@ -106,8 +104,10 @@ public class Context extends IDisposable /** * Retrieves the Real sort of the context. **/ - public RealSort RealSort() + public RealSort RealSort() throws Z3Exception { + if (m_realSort== null) + m_realSort = new RealSort(this); return m_realSort; } diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 88e67d82e..a67d94e7e 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -1786,8 +1786,6 @@ public class Expr extends AST return new RatNum(ctx, obj); case Z3_BV_SORT: return new BitVecNum(ctx, obj); - case Z3_UNKNOWN_SORT: - throw new Z3Exception("Unknown Sort"); default: ; } } @@ -1806,8 +1804,6 @@ public class Expr extends AST return new ArrayExpr(ctx, obj); case Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); - case Z3_UNKNOWN_SORT: - throw new Z3Exception("Unknown Sort"); default: ; }