diff --git a/sas2011-testcases/AmortizedQueue.scala b/sas2011-testcases/AmortizedQueue.scala index 9c049989dd5a734e213307d14a609bf95bfdc474..387bebc6d58c46e47d48891bbb2d98dffd95ff50 100644 --- a/sas2011-testcases/AmortizedQueue.scala +++ b/sas2011-testcases/AmortizedQueue.scala @@ -76,7 +76,7 @@ object AmortizedQueue { asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil())) } else true - } // holds + } holds @induct def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = { diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala index 46fb91033c9b3ce5bc3ceb7f1b4535615f3dae3e..03bd51ba74d17a90c24ea18a25f0f7651dae5f26 100644 --- a/src/purescala/FairZ3Solver.scala +++ b/src/purescala/FairZ3Solver.scala @@ -248,9 +248,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac var forceStop : Boolean = false def stopCallback() : Unit = { - reporter.error(" - Timeout reached.") - forceStop = true - z3.softCheckCancel + if(!foundDefinitiveAnswer) { + reporter.error(" - Timeout reached.") + forceStop = true + z3.softCheckCancel + } } val timer : Option[Timer] = Settings.solverTimeout.map(t => new Timer(stopCallback, t))