From 38ca9ddfeb1f07bad5264d2879c440a007acfdc8 Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Fri, 30 Nov 2018 08:42:01 +0700
Subject: [PATCH 1/2] Swapped significand and exponent in call to
 Context.mkFPNumeral.

Fixes #973.
---
 src/api/java/Context.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ede494598..ee7536eeb 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3447,7 +3447,7 @@ public class Context implements AutoCloseable {
      **/                     
     public FPNum mkFP(boolean sgn, int exp, int sig, FPSort s)
     {
-        return mkFPNumeral(sgn, sig, exp, s);
+        return mkFPNumeral(sgn, exp, sig, s);
     }
 
     /**
@@ -3460,7 +3460,7 @@ public class Context implements AutoCloseable {
      **/                     
     public FPNum mkFP(boolean sgn, long exp, long sig, FPSort s)
     {
-        return mkFPNumeral(sgn, sig, exp, s);
+        return mkFPNumeral(sgn, exp, sig, s);
     }
 
 

From afc9de960c6d495da52700f2ef3e6e534454c03d Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Fri, 30 Nov 2018 08:42:28 +0700
Subject: [PATCH 2/2] Improve JavaDoc.

---
 src/api/java/Context.java | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ee7536eeb..20c1c3737 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3356,7 +3356,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Create a numeral of FloatingPoint sort from a float.
+     * Create a numeral of FloatingPoint sort from a double.
      * @param v numeral value.
      * @param s FloatingPoint sort.
      * @throws Z3Exception 
@@ -3368,7 +3368,7 @@ public class Context implements AutoCloseable {
 
     /**
      * Create a numeral of FloatingPoint sort from an int.
-     * * @param v numeral value.
+     * @param v numeral value.
      * @param s FloatingPoint sort.
      * @throws Z3Exception 
      **/                    
@@ -3380,8 +3380,8 @@ public class Context implements AutoCloseable {
     /**
      * Create a numeral of FloatingPoint sort from a sign bit and two integers.
      * @param sgn the sign.
-     * @param sig the significand.
      * @param exp the exponent.
+     * @param sig the significand.
      * @param s FloatingPoint sort.
      * @throws Z3Exception 
      **/            
@@ -3393,8 +3393,8 @@ public class Context implements AutoCloseable {
     /**
      * Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
      * @param sgn the sign.
-     * @param sig the significand.
      * @param exp the exponent.
+     * @param sig the significand.
      * @param s FloatingPoint sort.
      * @throws Z3Exception 
      **/
@@ -3415,7 +3415,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Create a numeral of FloatingPoint sort from a float.
+     * Create a numeral of FloatingPoint sort from a double.
      * @param v numeral value.
      * @param s FloatingPoint sort.
      * @throws Z3Exception