diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 9c6504493..e08a75e7f 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -119,4 +119,12 @@ public class ASTVector extends Z3Object
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
+
+    BoolExpr[] ToBoolArray() {
+        int n = size();
+        BoolExpr[] res = new BoolExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = new BoolExpr(getContext(), get(i).getNativeObject());
+        return res;	
+    }
 }
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index c9d14288b..daa0f4e3f 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -298,11 +298,7 @@ public class Fixedpoint extends Z3Object
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
                 getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+	return v.ToBoolArray();
     }
 
     /**
@@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
+	return v.ToBoolArray();
     }
 
     /**
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 667c91a53..50c6a223a 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 ASTVector interp = null;
+        public BoolExpr[] interp = null;
         public Model model = null;
     };
     
@@ -109,8 +109,10 @@ public class InterpolationContext extends Context
         ComputeInterpolantResult res = new ComputeInterpolantResult();
         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) res.interp = new ASTVector(this, n_i.value);
+        res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
+        if (res.status == Z3_lbool.Z3_L_FALSE) {
+	    res.interp = (new ASTVector(this, n_i.value)).ToBoolArray();
+	}
         if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index e4ba9de42..7c4c1f4b9 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -190,11 +190,7 @@ public class Solver extends Z3Object
     {
         ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = assrts.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
-        return res;
+	return assrts.ToBoolArray();
     }
 
     /**
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index f510f4070..2debdaf42 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -966,7 +966,7 @@ public:
         get_linear_coefficients(t,coeffs);
         if(coeffs.size() == 0)
             return make_int("1"); // arbitrary
-        rational d = coeffs[0];
+        rational d = abs(coeffs[0]);
         for(unsigned i = 1; i < coeffs.size(); i++){
             d = gcd(d,coeffs[i]);
         }
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index 45c615e0c..893b5d87a 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -777,8 +777,8 @@ namespace smt {
                         // u += ncoeff * lower_bound(v).get_rational();
                         u.addmul(ncoeff, lower_bound(v).get_rational());
                     }
-                    lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
-                    upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                    lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
+                    upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
                 }
                 else if (gcds.is_zero()) {
                     gcds = abs_ncoeff;