From 8cb684c380a85ff0a4ffc824c07b95e1b813f608 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 9 Sep 2015 17:08:37 +0200
Subject: [PATCH] Catch Exception in getModel
---
src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
index 67909f60d..759dedbd8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala
@@ -187,7 +187,12 @@ class SMTLIBZ3Solver(context: LeonContext, program: Program) extends SMTLIBSolve
variables.getA(s) match {
case Some(id) =>
// EK: this is a little hack, we pass models for array functions as let-defs
- model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
+ try {
+ model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
+ } catch {
+ case _ : Unsupported =>
+
+ }
case _ => // function, should be handled elsewhere
}
}
--
GitLab