From b4f72c81457712929405f397b89c02bd8ca264c3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 22 May 2015 08:24:45 -0700 Subject: [PATCH] Revert "Change ASTVector to Expr[] in interpolation result" --- src/api/java/InterpolationContext.java | 11 ++--------- 1 file changed, 2 insertions(+), 9 deletions(-) diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java index 25f132fa7..667c91a53 100644 --- a/src/api/java/InterpolationContext.java +++ b/src/api/java/InterpolationContext.java @@ -90,7 +90,7 @@ public class InterpolationContext extends Context public class ComputeInterpolantResult { public Z3_lbool status = Z3_lbool.Z3_L_UNDEF; - public Expr[] interp = null; + public ASTVector interp = null; public Model model = null; }; @@ -110,14 +110,7 @@ public class InterpolationContext extends Context Native.LongPtr n_i = new Native.LongPtr(); Native.LongPtr n_m = new Native.LongPtr(); res.status =Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m)); - if (res.status == Z3_lbool.Z3_L_FALSE) - { - ASTVector seq = new ASTVector(this, n_i.value); - int n = seq.size(); - res.interp = new Expr[n]; - for (int i = 0; i < n; i++) - res.interp[i] = Expr.create(this, seq.get(i).getNativeObject()); - } + if (res.status == Z3_lbool.Z3_L_FALSE) res.interp = new ASTVector(this, n_i.value); if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value); return res; }