From ee9827023a806f0d192986cc0593ee5673d718a1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 22 Sep 2015 18:40:04 +0200
Subject: [PATCH] Be defensive with bodyless FunDefs
---
.../leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 382122cba..9704fceba 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -40,7 +40,9 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
val s = super.declareFunction(tfd)
try {
- val bodyAssert = SMTAssert(Equals(s: Term, toSMT(tfd.body.get)(Map())))
+ val bodyAssert = tfd.body map { bd =>
+ SMTAssert(Equals(s: Term, toSMT(bd)(Map())))
+ }
val specAssert = tfd.postcondition map { post =>
val term = implies(
@@ -50,7 +52,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
SMTAssert(toSMT(term)(Map()))
}
- Seq(bodyAssert) ++ specAssert
+ bodyAssert ++ specAssert
} catch {
case _ : SolverUnsupportedError =>
addError()
--
GitLab