Unification fails in case two terms' children's sizes are different

reactor/code/src/jetbrains/mps/unification/Unification.java

@@ -64,6 +64,9 @@ public class Unification {
                     while(scit.hasNext() && tcit.hasNext()) {
                         if (!unifClosure(scit.next(), tcit.next())) return false;
                     }
+                    if (scit.hasNext() != tcit.hasNext()) {
+                        return false; // children lists are of different size
+                    }
                 }
                 else {
                     return false; // symbol clash

reactor/tests/src/jetbrains/mps/unification/SolverTests.java

@@ -60,20 +60,20 @@ public class SolverTests {
                 bind(var("Y"), term("c"))
         );
         assertUnifiesWithBindings(
-                parse("a{b X Y Z}"),
-                parse("a{X Y Z b{e}}"),
+                parse("a{b{c} X Y Z}"),
+                parse("a{X Y Z b{c}}"),
 
-                bind(var("X"), term("b")),
-                bind(var("Y"), term("b")),
-                bind(var("Z"), term("b"))
+                bind(var("X"), parse("b{c}")),
+                bind(var("Y"), parse("b{c}")),
+                bind(var("Z"), parse("b{c}"))
         );
         assertUnifiesWithBindings(
-                parse("a{b Z Y X}"),
-                parse("a{Z Y X b{e}}"),
+                parse("a{b{c} Z Y X}"),
+                parse("a{Z Y X b{c}}"),
 
-                bind(var("X"), term("b")),
-                bind(var("Y"), term("b")),
-                bind(var("Z"), term("b"))
+                bind(var("X"), parse("b{c}")),
+                bind(var("Y"), parse("b{c}")),
+                bind(var("Z"), parse("b{c}"))
         );
     }
 
@@ -149,7 +149,7 @@ public class SolverTests {
     @Test
     public void test8() throws Exception {
         assertUnifiesWithBindings(
-                parseTerm("a{b{c d} e{f g} }"),
+                parseTerm("a{b{c d} e{f} }"),
                 parseTerm("a{b{X Y} e{Z} }"),
 
                 bind(var("X"), parseTerm("c")),
@@ -158,13 +158,32 @@ public class SolverTests {
         );
     }
 
+    @Test
+    public void test9() throws Exception {
+        assertUnifiesWithBindings(
+                parseTerm("a{b{c d} e{X} }"),
+                parseTerm("a{b{X Y} e{Z} }"),
+
+                bind(var("X"), parseTerm("c")),
+                bind(var("Y"), parseTerm("d")),
+                bind(var("Z"), parseTerm("c"))
+        );
+    }
+
     @Test
     public void testFail1() throws Exception {
         assertUnifificationFails(
                 term("a"),
                 term("b")
         );
+    }
 
+    @Test
+    public void testFail2() throws Exception {
+        assertUnifificationFails(
+                parse("a{b c}"),
+                parse("a{X}")
+        );
     }
 
 }