Only report error if the solver hasn't been aborted

jad-hamza · jad-hamza · commit 165133d546d7 · 2021-05-01T12:32:29.000+02:00
diff --git a/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala b/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala
@@ -831,7 +831,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
   }).recover {
     case e @ (_: InternalSolverError | _: Unsupported) =>
       if (reporter.isDebugEnabled) reporter.debug(e)
-      else if (!silentErrors) reporter.error(e.getMessage)
+      else if (!silentErrors && !abort) reporter.error(e.getMessage)
       config.cast(Unknown)
   }.get)
 }

Original file line number	Diff line number	Diff line change
`@@ -831,7 +831,7 @@ trait AbstractUnrollingSolver extends Solver { self =>`
`831`	`831`	`}).recover {`
`832`	`832`	`case e @ (_: InternalSolverError \| _: Unsupported) =>`
`833`	`833`	`if (reporter.isDebugEnabled) reporter.debug(e)`
`834`		`- else if (!silentErrors) reporter.error(e.getMessage)`
	`834`	`+ else if (!silentErrors && !abort) reporter.error(e.getMessage)`
`835`	`835`	`config.cast(Unknown)`
`836`	`836`	`}.get)`
`837`	`837`	`}`