From 36a4edc812e62b2b17b41dda13adb69829230325 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Tue, 19 May 2015 18:32:31 +0200
Subject: [PATCH] correct implementation of div and mod in fairz3
---
.../scala/leon/solvers/z3/AbstractZ3Solver.scala | 15 +++++++++++++--
1 file changed, 13 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index c2aea200c..9c9dbd09e 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -568,8 +568,19 @@ trait AbstractZ3Solver
case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
case Minus(l, r) => z3.mkSub(rec(l), rec(r))
case Times(l, r) => z3.mkMul(rec(l), rec(r))
- case Division(l, r) => z3.mkDiv(rec(l), rec(r))
- case Modulo(l, r) => z3.mkMod(rec(l), rec(r))
+ case Division(l, r) => {
+ val rl = rec(l)
+ val rr = rec(r)
+ z3.mkITE(
+ z3.mkGE(rl, z3.mkNumeral("0", typeToSort(IntegerType))),
+ z3.mkDiv(rl, rr),
+ z3.mkUnaryMinus(z3.mkDiv(z3.mkUnaryMinus(rl), rr))
+ )
+ }
+ case Modulo(l, r) => {
+ val q = rec(Division(l, r))
+ z3.mkSub(rec(l), z3.mkMul(rec(r), q))
+ }
case UMinus(e) => z3.mkUnaryMinus(rec(e))
case BVPlus(l, r) => z3.mkBVAdd(rec(l), rec(r))
case BVMinus(l, r) => z3.mkBVSub(rec(l), rec(r))
--
GitLab