From 4b8eacfcb281e5b4393f862dd38990801483b770 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Jun 2012 15:14:28 +0200
Subject: [PATCH] clearer error message for big int from Z3
---
src/main/scala/leon/FairZ3Solver.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 88d696f5b..1111b374d 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -1304,6 +1304,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
case Z3NumeralAST(Some(v)) => IntLiteral(v)
+ case Z3NumeralAST(None) => {
+ reporter.info("Cannot read exact model from Z3: Integer does not fit in machine word")
+ reporter.info("Exiting procedure now")
+ sys.exit(0)
+ }
case other @ _ => {
System.err.println("Don't know what this is " + other)
System.err.println("REVERSE FUNCTION MAP:")
--
GitLab