Correct handling of choose in verification.

- Choose expressions becomes uninterpreted functions under the same
  constraints.

- Fix bug with variablesOf considering choose binders as free.

- Silence evaluator errors when occuring with tentative lucky models.
  Note that choose expressions cannot be evaluated nor compiled.

src/main/scala/leon/purescala/TreeOps.scala

@@ -361,6 +361,7 @@ object TreeOps {
     def combine(s1: Set[Identifier], s2: Set[Identifier]) = s1 ++ s2
     def compute(t: Expr, s: Set[Identifier]) = t match {
       case Let(i,_,_) => s -- Set(i)
+      case Choose(is,_) => s -- is
       case MatchExpr(_, cses) => s -- (cses.map(_.pattern.binders).foldLeft(Set[Identifier]())((a, b) => a ++ b))
       case _ => s
     }

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -139,7 +139,7 @@ class FairZ3Solver(context : LeonContext)
     (solver.checkAssumptions(assumptions), solver.getModel, solver.getUnsatCore)
   }
 
-  private def validateModel(model: Z3Model, formula: Expr, variables: Set[Identifier]) : (Boolean, Map[Identifier,Expr]) = {
+  private def validateModel(model: Z3Model, formula: Expr, variables: Set[Identifier], silenceErrors: Boolean) : (Boolean, Map[Identifier,Expr]) = {
     if(!forceStop) {
 
       val functionsModel: Map[Z3FuncDecl, (Seq[(Seq[Z3AST], Z3AST)], Z3AST)] = model.getModelFuncInterpretations.map(i => (i._1, (i._2, i._3))).toMap
@@ -185,7 +185,11 @@ class FairZ3Solver(context : LeonContext)
           (false, asMap)
 
         case EvaluationResults.EvaluatorError(msg) => 
-          reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
+          if (silenceErrors) {
+            reporter.info("- Model leads to evaluator error: " + msg)
+          } else {
+            reporter.warning("Something went wrong. While evaluating the model, we got this : " + msg)
+          }
           (false, asMap)
 
       }
@@ -502,7 +506,7 @@ class FairZ3Solver(context : LeonContext)
             val z3model = solver.getModel
 
             if (this.checkModels) {
-              val (isValid, model) = validateModel(z3model, entireFormula, varsInVC)
+              val (isValid, model) = validateModel(z3model, entireFormula, varsInVC, silenceErrors = false)
 
               if (isValid) {
                 foundAnswer(Some(true), model)
@@ -588,7 +592,7 @@ class FairZ3Solver(context : LeonContext)
                   if (this.feelingLucky && !forceStop) {
                     // we might have been lucky :D
                     luckyTime.start
-                    val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC)
+                    val (wereWeLucky, cleanModel) = validateModel(solver.getModel, entireFormula, varsInVC, silenceErrors = true)
                     luckyTime.stop
 
                     if(wereWeLucky) {

src/main/scala/leon/solvers/z3/FunctionTemplate.scala

@@ -272,7 +272,18 @@ object FunctionTemplate {
           }
         }
 
-        case c @ Choose(_, _) => Variable(FreshIdentifier("choose", true).setType(c.getType))
+        case c @ Choose(ids, cond) =>
+          val cid = FreshIdentifier("choose", true).setType(c.getType)
+          exprVars += cid
+
+          val m: Map[Expr, Expr] = if (ids.size == 1) {
+            Map(Variable(ids.head) -> Variable(cid))
+          } else {
+            ids.zipWithIndex.map{ case (id, i) => Variable(id) -> TupleSelect(Variable(cid), i+1) }.toMap
+          }
+
+          storeGuarded(pathVar, replace(m, cond))
+          Variable(cid)
 
         case n @ NAryOperator(as, r) => r(as.map(a => rec(pathVar, a))).setType(n.getType)
         case b @ BinaryOperator(a1, a2, r) => r(rec(pathVar, a1), rec(pathVar, a2)).setType(b.getType)

src/test/resources/regression/verification/purescala/invalid/Choose1.scala

+import leon.Annotations._
+import leon.Utils._
+
+object Choose1 {
+    sealed abstract class List
+    case class Cons(head: Int, tail: List) extends List
+    case class Nil() extends List
+
+    def size(l: List) : Int = (l match {
+        case Nil() => 0
+        case Cons(_, t) => 1 + size(t)
+    }) ensuring(res => res >= 0)
+
+    def content(l: List) : Set[Int] = l match {
+      case Nil() => Set.empty[Int]
+      case Cons(x, xs) => Set(x) ++ content(xs)
+    }
+
+    def listOfSize(i: Int): List = {
+      require(i >= 0)
+
+      if (i == 0) {
+        Nil()
+      } else {
+        choose { (res: List) => size(res) == i-1 }
+      }
+    } ensuring ( size(_) == i )
+
+
+    def listOfSize2(i: Int): List = {
+      require(i >= 0)
+
+      if (i > 0) {
+        Cons(0, listOfSize(i-1))
+      } else {
+        Nil()
+      }
+    } ensuring ( size(_) == i )
+}

src/test/resources/regression/verification/purescala/valid/Choose1.scala

+import leon.Annotations._
+import leon.Utils._
+
+object Choose1 {
+    sealed abstract class List
+    case class Cons(head: Int, tail: List) extends List
+    case class Nil() extends List
+
+    def size(l: List) : Int = (l match {
+        case Nil() => 0
+        case Cons(_, t) => 1 + size(t)
+    }) ensuring(res => res >= 0)
+
+    def content(l: List) : Set[Int] = l match {
+      case Nil() => Set.empty[Int]
+      case Cons(x, xs) => Set(x) ++ content(xs)
+    }
+
+    def listOfSize(i: Int): List = {
+      require(i >= 0)
+
+      if (i == 0) {
+        Nil()
+      } else {
+        choose { (res: List) => size(res) == i }
+      }
+    } ensuring ( size(_) == i )
+
+
+    def listOfSize2(i: Int): List = {
+      require(i >= 0)
+
+      if (i > 0) {
+        Cons(0, listOfSize(i-1))
+      } else {
+        Nil()
+      }
+    } ensuring ( size(_) == i )
+}