From 66c20df4e0a03c5c54db6d4c412f39f4e07ba2c8 Mon Sep 17 00:00:00 2001 From: Nils Erik Flick Date: Thu, 17 Oct 2019 10:05:05 +0200 Subject: [PATCH] Z3 and floating points: use useFpForReals when translating greater-than/less-than expressions. --- .../nasa/jpf/symbc/numeric/solvers/ProblemZ3.java | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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);