From 71e5bffcd766d47a48d8510eb287b03ecb41e57a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 May 2015 18:24:23 +0200
Subject: [PATCH] Catch some errors
---
.../smtlib/SMTLIBCVC4QuantifiedTarget.scala | 14 ++++++++++++--
1 file changed, 12 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
index c9189acd5..9ac752c74 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedTarget.scala
@@ -95,7 +95,12 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
tfd.precondition getOrElse BooleanLiteral(true),
application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
)
- sendCommand(SMTAssert(quantifiedTerm(ForAll, term)))
+ try {
+ sendCommand(SMTAssert(quantifiedTerm(ForAll, term)))
+ } catch {
+ case _ : IllegalArgumentException =>
+ addError()
+ }
}
}
@@ -107,6 +112,11 @@ abstract class SMTLIBCVC4QuantifiedTarget(context: LeonContext, program: Program
// For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
override def assertCnstr(expr: Expr) =
- sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
+ try {
+ sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
+ } catch {
+ case _ : IllegalArgumentException =>
+ addError()
+ }
}
--
GitLab