Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

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;	
+    }
 }

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();
+	return v.ToBoolArray();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
     }
 
     /**
@@ -315,11 +311,7 @@ public class Fixedpoint extends Z3Object
 
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
                 getContext().nCtx(), getNativeObject()));
-        int n = v.size();
+	return v.ToBoolArray();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
     }
 
     /**

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));        
+        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);
+        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;
     }

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();
+	return assrts.ToBoolArray();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
-        return res;
     }
 
     /**

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]);
         }

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());
+                    lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
-                    upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                    upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
                 }
                 else if (gcds.is_zero()) {
                     gcds = abs_ncoeff;