diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Solver.scala index 67909f60d321851802e8b9f800ecfebda7e35d9b..759dedbd8229c909a5755be064d369cf6332762f 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 } }