From c884427be2d7ef7714daab6929ad046dcd825908 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Mon, 23 Nov 2015 16:51:56 +0100
Subject: [PATCH] Corrected a bug in AbstractZ3Solver.scala when the BV is at
its maximum.
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 9 +++++++--
1 file changed, 7 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index e7224a950..92f6bf354 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -578,12 +578,17 @@ trait AbstractZ3Solver extends Solver {
}
case Z3NumeralIntAST(None) => {
val ts = t.toString
+ reporter.ifDebug(printer => printer(ts))(DebugSectionSynthesis)
if(ts.length > 4 && ts.substring(0, 2) == "bv" && ts.substring(ts.length - 4) == "[32]") {
val integer = ts.substring(2, ts.length - 4)
tpe match {
- case Int32Type => IntLiteral(integer.toInt)
+ case Int32Type =>
+ if(integer == "2147483648") IntLiteral(-1) else
+ IntLiteral(integer.toInt)
case CharType => CharLiteral(integer.toInt.toChar)
- case IntegerType => InfiniteIntegerLiteral(BigInt(integer.toInt))
+ case IntegerType =>
+ if(integer == "2147483648") InfiniteIntegerLiteral(BigInt(-1)) else
+ InfiniteIntegerLiteral(BigInt(integer))
case _ =>
reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
}
--
GitLab