diff --git a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3.java b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3.java
index 738249b6..0ca0bb34 100644
--- a/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3.java
+++ b/src/main/gov/nasa/jpf/symbc/numeric/solvers/ProblemZ3.java
@@ -354,7 +354,11 @@ public Object lt(Object exp, long value){
 
 	public Object lt(Object exp1, Object exp2){
 		try{
-			return  ctx.mkLt((ArithExpr)exp1,(ArithExpr)exp2);
+			if (useFpForReals) {
+			    return  ctx.mkFPLt((FPExpr)exp1,(FPExpr)exp2);
+			} else {
+				return  ctx.mkLt((ArithExpr)exp1,(ArithExpr)exp2);
+			}
 		} catch (Exception e) {
 			e.printStackTrace();
 			throw new RuntimeException("## Error Z3: Exception caught in Z3 JNI: \n" + e);
@@ -405,7 +409,11 @@ public Object gt(Object exp, long value){
 
 	public Object gt(Object exp1, Object exp2){
 		try{
-			return  ctx.mkGt((ArithExpr)exp1,(ArithExpr)exp2);
+			if (useFpForReals) {
+	            return  ctx.mkFPGt((FPExpr)exp1,(FPExpr)exp2);
+		    } else {
+			    return  ctx.mkGt((ArithExpr)exp1,(ArithExpr)exp2);
+		    }
 		} catch (Exception e) {
 			e.printStackTrace();
 			throw new RuntimeException("## Error Z3: Exception caught in Z3 JNI: \n" + e);