Question builder will now try to instantiate always different terminal values...

Question builder will now try to instantiate always different terminal values for better comparison.
Corrected benchmark out of order to not depend on each other;

src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala

@@ -144,18 +144,33 @@ class QuestionBuilder[T <: Expr](
   /** Make all generic values unique.
     * Duplicate generic values are not suitable for disambiguating questions since they remove an order. */
   def makeGenericValuesUnique(a: Expr): Expr = {
-    var genVals = Set[GenericValue]()
-    @tailrec @inline def freshGenericValue(g: GenericValue): GenericValue = {
-      if(genVals contains g)
-        freshGenericValue(GenericValue(g.tp, g.id + 1))
-      else {
-        genVals += g
-        g
-      }
+    var genVals = Set[Expr with Terminal]()
+    def freshenValue(g: Expr with Terminal): Option[Expr with Terminal] = g match {
+      case g: GenericValue => Some(GenericValue(g.tp, g.id + 1))
+      case StringLiteral(s) =>
+        val i = s.lastIndexWhere { c => c < '0' || c > '9' }
+        val prefix = s.take(i+1)
+        val suffix = s.drop(i+1)
+        Some(StringLiteral(prefix + (if(suffix == "") "0" else (suffix.toInt + 1).toString)))
+      case InfiniteIntegerLiteral(i) => Some(InfiniteIntegerLiteral(i+1))
+      case IntLiteral(i) => if(i == Integer.MAX_VALUE) None else Some(IntLiteral(i+1))
+      case CharLiteral(c) => if(c == Char.MaxValue) None else Some(CharLiteral((c+1).toChar))
+      case otherLiteral => None
+    }
+    @tailrec @inline def freshValue(g: Expr with Terminal): Expr with Terminal = {
+          if(genVals contains g)
+            freshenValue(g) match {
+              case None => g
+              case Some(v) => freshValue(v)
+            }
+          else {
+            genVals += g
+            g
+          }
     }
     ExprOps.postMap{ e => e match {
-      case g@GenericValue(tpe, i) =>
-        Some(freshGenericValue(g))
+      case g:Expr with Terminal =>
+        Some(freshValue(g))
       case _ => None
     }}(a)
   }

testcases/web/synthesis/25_String_OutOfOrder.scala

@@ -5,13 +5,13 @@ import leon.collection.ListOps._
 import leon.lang.synthesis._
 
 object OutOfOrderToString {
-  def argumentsToString(i: Int, j: Int): String = {
+  def arguments(i: Int, j: Int): String = {
     ???
   } ensuring { (res: String) => ((i, j), res) passes {
     case (1, 2) => "2, 1"
   } }
   
-  def tupleToString(i: (Int, Int)): String = {
+  def tuple(i: (Int, Int)): String = {
     ???
   } ensuring { (res: String) => (i, res) passes {
     case (1, 2) => "2, 1"
@@ -27,7 +27,7 @@ object OutOfOrderToString {
     }
   }
   
-  def listPairToString(l : List[(Int, Int)]): String =  {
+  def listPair(l : List[(Int, Int)]): String =  {
     ???[String]
   } ensuring {
     (res : String) => (l, res) passes {
@@ -36,7 +36,7 @@ object OutOfOrderToString {
     }
   }
   
-  def reverselistPairToString(l: List[(Int, Int)]): String = {
+  def reverselistPair(l: List[(Int, Int)]): String = {
     ???
   } ensuring { (res: String) => (l, res) passes {
     case Cons((1, 2), Cons((3,4), Nil())) => "4 -> 3, 2 -> 1"
@@ -44,7 +44,7 @@ object OutOfOrderToString {
   
   case class Rule(input: Int, applied: Option[Int])
   
-  def ruleToString(r : Rule): String =  {
+  def rule(r : Rule): String =  {
     ???
   } ensuring {
     (res : String) => (r, res) passes {