diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 88d696f5bd41c4fe5091c1bc51ba1921ca6201fc..1111b374dffeb2c0d3793be29232e49a63e387cc 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:")