Fix bug #461 for Z3

Author: daniel-raffler

src/org/sosy_lab/java_smt/solvers/z3/Z3NumeralFormulaManager.java

@@ -82,7 +82,16 @@ protected Long subtract(Long pNumber1, Long pNumber2) {
 
   @Override
   protected Long divide(Long pNumber1, Long pNumber2) {
-    return Native.mkDiv(z3context, pNumber1, pNumber2);
+    // If one of the arguments is rational and the other integer, add an explicit cast
+    long sort1 = Native.getSort(z3context, pNumber1);
+    long sort2 = Native.getSort(z3context, pNumber2);
+    long arg1 = pNumber1;
+    long arg2 = pNumber2;
+    if (sort1 != sort2) {
+      arg1 = (sort1 == formulaCreator.getIntegerType()) ? Native.mkInt2real(z3context, arg1) : arg1;
+      arg2 = (sort2 == formulaCreator.getIntegerType()) ? Native.mkInt2real(z3context, arg2) : arg2;
+    }
+    return Native.mkDiv(z3context, arg1, arg2);
   }
 
   @Override