From a7b3dfb3aff3a1e06322006e8d3a7cf291945760 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Mar 2020 14:17:04 +0100 Subject: [PATCH] try now #3202 Signed-off-by: Nikolaj Bjorner --- src/api/java/Solver.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index 209cfc561..ac7f8434d 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -264,7 +264,7 @@ public class Solver extends Z3Object { for (BoolExpr asm : assumptions) asms.push(asm); for (Expr v : variables) vars.push(v); int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject()); - for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr)result.get(i)); + for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject())); return lboolToStatus(Z3_lbool.fromInt(r)); }