add test

Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>

src/main/java/de/tla2bAst/ExpressionTranslator.java

@@ -216,6 +216,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants {
 		searchVarInSyntaxTree(expr);
         
         // this code seems to assume that there is no variable clash between outer and nested variables
+        // I guess the parser will then generate "Multiply-defined symbol ..." errors
 		for (int i = 0; i < noVariables.size(); i++) {
 			variables.remove(noVariables.get(i));
 		}

src/test/java/de/tla2b/expression/ComplexExpressionTest.java

@@ -84,5 +84,12 @@ public class ComplexExpressionTest {
 		compareExpr("CHOOSE({x|x:0..100 & x**3 - 20*x**2 + 7*x = 14388})",
 				    "CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
 	}
+	@Test
+	public void testConstraintCHOOSENested() throws Exception {
+		compareExpr("CHOOSE({y|y : 0 .. 100 & y = CHOOSE({x|x : 0 .. 100 & x ** 3 - 20 * x ** 2 + 7 * x = 14388})})",
+				    "CHOOSE y \\in 0..100: y = CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
+	}
+	// Note that for:  CHOOSE x \in 0..100: x = CHOOSE x \in 0..100: x^3 - 20*x^2 + 7*x = 14388
+	//   we get an error: Multiply-defined symbol 'x': this definition or declaration conflicts 
 
 }