Skip to content
Snippets Groups Projects
Commit 4e9a690a authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

If there is an error already, don't send commands

parent fbae1d2b
Branches
Tags
No related merge requests found
...@@ -786,7 +786,7 @@ abstract class SMTLIBSolver(val context: LeonContext, ...@@ -786,7 +786,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
out.flush() out.flush()
} }
interpreter.eval(cmd) match { 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") reporter.warning(s"Unexpected error from $name solver: $msg")
// Store that there was an error. Now all following check() // Store that there was an error. Now all following check()
// invocations will return None // invocations will return None
...@@ -799,7 +799,7 @@ abstract class SMTLIBSolver(val context: LeonContext, ...@@ -799,7 +799,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
// Public solver interface // Public solver interface
override def assertCnstr(expr: Expr): Unit = { override def assertCnstr(expr: Expr): Unit = if(!hasError) {
variablesOf(expr).foreach(declareVariable) variablesOf(expr).foreach(declareVariable)
try { try {
val term = toSMT(expr)(Map()) val term = toSMT(expr)(Map())
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment