Extending the interface of Solver to support counter-example generation.

src/main/scala/leon/Extensions.scala

 package leon
 
+import purescala.Common._
 import purescala.Trees._
 import purescala.Definitions._
 
@@ -20,6 +21,8 @@ object Extensions {
     // should halt as soon as possible with any result (Unknown is ok) as soon as forceStop is true
     def solve(expression: Expr) : Option[Boolean]
 
+    def solveOrGetCounterexample(expression : Expr) : (Option[Boolean],Map[Identifier,Expr]) = (solve(expression), Map.empty)
+
     def isUnsat(expression: Expr) : Option[Boolean] = solve(negate(expression))
     def superseeds : Seq[String] = Nil
 

src/main/scala/leon/FairZ3Solver.scala

@@ -478,6 +478,11 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
 
   def solve(vc: Expr) = decide(vc, true)
 
+  override def solveOrGetCounterexample(vc : Expr) : (Option[Boolean],Map[Identifier,Expr]) = {
+    restartZ3
+    decideWithModel(vc, true)
+  }
+
   def solveWithBounds(vc: Expr, fv: Boolean) : (Option[Boolean], Map[Identifier,Expr]) = {
     restartZ3
     boundValues

src/main/scala/leon/TrivialSolver.scala

@@ -18,5 +18,4 @@ class TrivialSolver(reporter: Reporter) extends Solver(reporter) {
     case And(exs) if exs.contains(BooleanLiteral(false)) => Some(false)
     case _ => None
   }
-
 }