From 4e9a690a03c00c2ee9ae8662587bb676e08cf729 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 11 May 2015 15:26:19 +0200
Subject: [PATCH] If there is an error already, don't send commands
---
src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 60da64f87..5106a6049 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -786,7 +786,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
out.flush()
}
interpreter.eval(cmd) match {
- case err@ErrorResponse(msg) if !interrupted =>
+ case err@ErrorResponse(msg) if !hasError && !interrupted =>
reporter.warning(s"Unexpected error from $name solver: $msg")
// Store that there was an error. Now all following check()
// invocations will return None
@@ -799,7 +799,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
// Public solver interface
- override def assertCnstr(expr: Expr): Unit = {
+ override def assertCnstr(expr: Expr): Unit = if(!hasError) {
variablesOf(expr).foreach(declareVariable)
try {
val term = toSMT(expr)(Map())
--
GitLab