From 9f30d3ef48a175166b6b270d966f0f409ee385cc Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 7 May 2015 17:19:31 +0200
Subject: [PATCH] Improve unsupported handling in SMTLIB
---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 21 ++++++++++++-------
1 file changed, 14 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 54ed63031..8371a52e8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -682,9 +682,13 @@ trait SMTLIBTarget {
out.write("\n")
out.flush()
}
- if (hasError) Unsupported else interpreter.eval(cmd) match {
+ interpreter.eval(cmd) match {
case err@ErrorResponse(msg) if !interrupted =>
- reporter.fatalError("Unexpected error from smt-"+targetName+" solver: "+msg)
+ reporter.warning(s"Unexpected error from $name solver: $msg")
+ // Store that there was an error. Now all following check()
+ // invocations will return None
+ addError()
+ err
case res => res
}
}
@@ -703,11 +707,14 @@ trait SMTLIBTarget {
}
- override def check: Option[Boolean] = sendCommand(CheckSat()) match {
- case CheckSatStatus(SatStatus) => Some(true)
- case CheckSatStatus(UnsatStatus) => Some(false)
- case CheckSatStatus(UnknownStatus) => None
- case e => None
+ override def check: Option[Boolean] = {
+ if (hasError) None
+ else sendCommand(CheckSat()) match {
+ case CheckSatStatus(SatStatus) => Some(true)
+ case CheckSatStatus(UnsatStatus) => Some(false)
+ case CheckSatStatus(UnknownStatus) => None
+ case e => None
+ }
}
override def getModel: Map[Identifier, Expr] = {
--
GitLab