diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/Justify.scala
index fcb927be935b57b415d7044930c8310769bb4ecf..2c3ff9a32cdea24a3d0b0da50a540081a2187e1b 100644
--- a/testcases/synthesis/Justify.scala
+++ b/testcases/synthesis/Justify.scala
@@ -40,20 +40,39 @@ object Justify {
    * justifying     lines     by
    * inserting extra  blanks  is
    * one  task of a text editor.
-
-   *
-   * This version is a simpler one, in which we are just trying to determine parameters that can then
-   * be mecanically used to build the justified text. Also we do not distinguish on even/odd line number.
-   * 
    */
-  def justify(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int) = {
+  def justify(n: Int, z: Int, s: Int, words: IntList): IntList = {
     require(n >= 0 && s >= 0 && z >= 1)
 
     //here p and q are as defined above. t is used to find the index of the word where
     //we switch from p spaces to q spaces.
     val (res, p, q, t) = choose((justifiedWords: IntList, p: Int, q: Int, t: Int) => 
       p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n && 
-      p*(t - 1) + q*(n-t) == s //this constraint is probably going to be an issue since it is non linear
+      p*(t-1) + q*(n-t) == s && //this constraint is probably going to be an issue since it is non linear
+      ((z % 2 == 1 && q == p + 1) || (z % 2 == 0 && p == q + 1)) &&
+      justifiedWords == addSpaces(words, p, q, t, n, 0) //this is likely to be problematic as well
+    )
+
+    res
+  }
+
+  def addSpaces(words: IntList, p: Int, q: Int, t: Int, n: Int, i: Int): IntList = words match {
+    case IntNil() => IntNil()
+    case IntCons(head, tail) =>
+      if(i <= t) IntCons(head + p*(i-1), addSpaces(tail, p, q, t, n, i+1))
+      else if(i > t && i <= n) IntCons(head + p*(t-1) + q*(i-t), addSpaces(tail, p, q, t, n, i+1))
+      else IntNil() //this should never happen
+  }
+
+  /*
+   * This version is a simpler one, in which we are just trying to determine parameters that can then
+   * be mecanically used to build the justified text. Also we do not distinguish on even/odd line number.
+   */
+  def simpleJustify(n: Int, z: Int, s: Int, words: IntList): (Int, Int, Int) = {
+    require(n >= 0 && s >= 0 && z >= 1)
+
+    val (p, q, t) = choose((p: Int, q: Int, t: Int) => 
+      p >= 0 && q >= 0 && p == q+1 && t >= 1 && t <= n && p*(t - 1) + q*(n-t) == s
     )
 
     //actually, we could simply use the parameter to program the ocnstruction of the List, rather than explicitly synthesizing it