Call z3 to get model satisfying no conditions

src/main/scala/leon/synthesis/Rules.scala

@@ -164,8 +164,6 @@ class UnusedInput(synth: Synthesizer) extends Rule("UnusedInput", synth) {
 }
 
 class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", synth) {
-  def defaultValueFor(id: Identifier): Expr = IntLiteral(0)
-
   def isApplicable(task: Task): List[DecomposedTask] = {
     val p = task.problem
     val unconstr = p.xs.toSet -- variablesOf(p.phi)
@@ -174,7 +172,14 @@ class UnconstrainedOutput(synth: Synthesizer) extends Rule("Unconstr.Output", sy
       val sub = p.copy(xs = p.xs.filterNot(unconstr))
 
       val onSuccess: List[Solution] => Solution = { 
-        case List(s) => Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) defaultValueFor(id) else Variable(id) ))))
+        case List(s) => 
+          synth.solveSAT(And(unconstr.map(id => Equals(Variable(id), Variable(id))).toSeq)) match {
+            case (Some(true), model) =>
+              Solution(s.pre, LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) model(id) else Variable(id)))))
+            case _ =>
+              Solution.none
+          }
+        
         case _ => Solution.none
       }
 

testcases/Choose.scala

@@ -13,6 +13,8 @@ object ChooseTest {
   def c4(a: Int): (Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int) => x1 > a && x2 > a }
   def c5(a: Int): (Int, Int, Int, Int, Int) = choose{ (x1: Int, x2: Int, x3: Int, x4: Int, x5: Int) => x1 > a && x2 > a }
 
+  def z0(a: Int): (Int, Int, List) = choose{ (x1: Int, x2: Int, x3: List) => x1 > a && x2 > a }
+
 
   sealed abstract class List
   case class Nil() extends List