No commit message

No commit message

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 = {

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))