From 5ef73c871ca159e4b4e55c1310a77a5a53ab3e22 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 25 Nov 2015 17:15:45 +0100
Subject: [PATCH] BUG Corrected: INT32 semantics
---
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 4 +---
1 file changed, 1 insertion(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 92f6bf354..c0249059a 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -583,11 +583,9 @@ trait AbstractZ3Solver extends Solver {
val integer = ts.substring(2, ts.length - 4)
tpe match {
case Int32Type =>
- if(integer == "2147483648") IntLiteral(-1) else
- IntLiteral(integer.toInt)
+ IntLiteral(integer.toLong.toInt)
case CharType => CharLiteral(integer.toInt.toChar)
case IntegerType =>
- if(integer == "2147483648") InfiniteIntegerLiteral(BigInt(-1)) else
InfiniteIntegerLiteral(BigInt(integer))
case _ =>
reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
--
GitLab