Commit d081abe9 authored by Anastasiia's avatar Anastasiia

change timeout for dReal

parent d2d2b5c9
...@@ -80,7 +80,7 @@ class DRealInterpreter(executable: String, args: Array[String]) ...@@ -80,7 +80,7 @@ class DRealInterpreter(executable: String, args: Array[String])
} (ExecutionContext.global) } (ExecutionContext.global)
try { try {
Await.result(f, 5.second) // TODO parameter? Await.result(f, 3.second) // TODO parameter?
} catch { } catch {
case e: TimeoutException => CheckSatStatus(UnknownStatus) case e: TimeoutException => CheckSatStatus(UnknownStatus)
} finally { } finally {
......
...@@ -203,9 +203,9 @@ abstract class SMTLibSolver(val context: Context) { ...@@ -203,9 +203,9 @@ abstract class SMTLibSolver(val context: Context) {
res match { res match {
case CheckSatStatus(SatStatus) => Some(true) case CheckSatStatus(SatStatus) => Some(true)
case CheckSatStatus(UnsatStatus) => Some(false) case CheckSatStatus(UnsatStatus) => Some(false)
case CheckSatStatus(UnknownStatus) => reporter.warning(s"solver says $res") case CheckSatStatus(UnknownStatus) => reporter.debug(s"solver says $res")
None None
case e => reporter.warning(s"solver CRIES $res") case e => reporter.debug(s"solver CRIES $res")
None None
} }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment