Index: /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java
===================================================================
--- /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java	(revision 204)
+++ /ModelTranslator/src/de/uni_hildesheim/sse/trans/convert/MaxTermConverter.java	(revision 205)
@@ -1,12 +1,11 @@
 package de.uni_hildesheim.sse.trans.convert;
 
-import java.io.IOException;
-import java.io.PipedInputStream;
-import java.io.PipedOutputStream;
 import java.io.PrintStream;
 import java.io.StringWriter;
 import java.math.BigInteger;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Map;
+import java.util.Set;
 
 import org.apache.commons.io.output.WriterOutputStream;
@@ -47,4 +46,8 @@
     private static final int MIN_SIMPLYIFY_LENGTH = 18;
     
+    /**
+     * Should avoid that complex constraints are translated twice.
+     */
+    private Set<ConstraintSyntaxTree> complexConstraints = new HashSet<ConstraintSyntaxTree>();
     private Project project;
     private Map<AbstractVariable, Variable> variablesCache = new HashMap<AbstractVariable, Variable>();
@@ -97,25 +100,6 @@
         }
         
-        if (getSyntaxTreeLength(originalConstraint) >= MIN_SIMPLYIFY_LENGTH) {
-            LOGGER.info("Constraint is longer than " + MIN_SIMPLYIFY_LENGTH + ", trying to simplify");
-            
-            // pull in NOT's as far as possible
-            CSTNegater negater = new CSTNegater();
-            originalConstraint.accept(negater);
-            originalConstraint = negater.getResult();
-            
-            // expand to get closer to CNF
-            CSTExpander expander = new CSTExpander(MIN_SIMPLYIFY_LENGTH);
-            int numExpanded = 0;
-            do {
-                expander.clearResult();
-                originalConstraint.accept(expander);
-                if (expander.getResult() != null) {
-                    originalConstraint = expander.getResult();
-                    numExpanded++;
-                }
-            } while (expander.getResult() != null);
-            
-            LOGGER.info("Found " + numExpanded + " possible expansions to simplify constraint");
+        if (!handled && getSyntaxTreeLength(originalConstraint) >= MIN_SIMPLYIFY_LENGTH) {
+            originalConstraint = simplifyComplexConstraint(originalConstraint);
         }
         
@@ -131,46 +115,79 @@
         }
         
+        // Stop recursion and start translation!
         if (!handled) {
-            // Stop recursion!
-            
-            // Get an array of all variables in the constraint
-            DeclarationInConstraintFinderWithDepth finder =
+            if (!complexConstraints.contains(originalConstraint)) {
+                complexConstraints.add(originalConstraint);
+                
+                // Get an array of all variables in the constraint
+                DeclarationInConstraintFinderWithDepth finder =
                     new DeclarationInConstraintFinderWithDepth(originalConstraint);
-            AbstractVariable[] declarationArray = finder.getDeclarationsInOrder().toArray(new AbstractVariable[] {});
-            
-            StringWriter sWriter = new StringWriter();
-            WriterOutputStream outStream = new WriterOutputStream(sWriter);
-            new DebugConstraintTreeVisitor(new PrintStream(outStream));
-            LOGGER.info(sWriter.toString());
-            
-            for (AbstractVariable var : declarationArray) {
-                LOGGER.debug(var.getName());
-            }
-            
-            // Create a project which only contains our single Constraint
-            Project singleConstraintProject = new Project("SingleConstraintProject");
-            Constraint constraintCopy = null;
-            try {
-                constraintCopy = new Constraint(originalConstraint, singleConstraintProject);
-            } catch (CSTSemanticException e) {
-                // Cannot happen
-                LOGGER.exception(e);
-            }
-            singleConstraintProject.add(constraintCopy);
-            for (AbstractVariable var : declarationArray) {
-                singleConstraintProject.add(var);
-            }
-            
-            // Create a configuration object for the singleConstraintProject
-            Configuration config = new Configuration(singleConstraintProject);
-            
-            if (declarationArray.length >= 16) {
-    //            System.out.println("Handling big constraint: " + declarationArray.length);
-                handleBigConstraint(originalConstraint, declarationArray, config);
-    //            System.out.println("Done.");
+                AbstractVariable[] declarationArray = finder.getDeclarationsInOrder()
+                    .toArray(new AbstractVariable[] {});        
+                StringWriter sWriter = new StringWriter();
+                WriterOutputStream outStream = new WriterOutputStream(sWriter);
+                new DebugConstraintTreeVisitor(new PrintStream(outStream));
+                LOGGER.info(sWriter.toString());
+                
+                for (AbstractVariable var : declarationArray) {
+                    LOGGER.debug(var.getName());
+                }
+                
+                // Create a project which only contains our single Constraint
+                Project singleConstraintProject = new Project("SingleConstraintProject");
+                Constraint constraintCopy = null;
+                try {
+                    constraintCopy = new Constraint(originalConstraint, singleConstraintProject);
+                } catch (CSTSemanticException e) {
+                    // Cannot happen
+                    LOGGER.exception(e);
+                }
+                singleConstraintProject.add(constraintCopy);
+                for (AbstractVariable var : declarationArray) {
+                    singleConstraintProject.add(var);
+                }
+                
+                // Create a configuration object for the singleConstraintProject
+                Configuration config = new Configuration(singleConstraintProject);
+                
+                if (declarationArray.length >= 16) {
+                    handleBigConstraint(originalConstraint, declarationArray, config);
+                } else {
+                    handleSmallConstraint(originalConstraint, declarationArray, config);
+                }
             } else {
-                handleSmallConstraint(originalConstraint, declarationArray, config);
-            }
-        }
+                LOGGER.info("Nothing to do, constraint was already part of another translation step.");
+            }
+        }
+    }
+
+    /**
+     * Tries to rewrite/split constraints with more than {@value #MIN_SIMPLYIFY_LENGTH} variables to constraints
+     * with less variables.
+     * @param originalConstraint A constraint with at least {@value #MIN_SIMPLYIFY_LENGTH} variables.
+     * @return A constraint which maybe be more in CNF form as before, maybe the same constraint as before.
+     */
+    private ConstraintSyntaxTree simplifyComplexConstraint(ConstraintSyntaxTree originalConstraint) {
+        LOGGER.info("Constraint is longer than " + MIN_SIMPLYIFY_LENGTH + ", trying to simplify");
+        
+        // pull in NOT's as far as possible
+        CSTNegater negater = new CSTNegater();
+        originalConstraint.accept(negater);
+        originalConstraint = negater.getResult();
+        
+        // expand to get closer to CNF
+        CSTExpander expander = new CSTExpander(MIN_SIMPLYIFY_LENGTH);
+        int numExpanded = 0;
+        do {
+            expander.clearResult();
+            originalConstraint.accept(expander);
+            if (expander.getResult() != null) {
+                originalConstraint = expander.getResult();
+                numExpanded++;
+            }
+        } while (expander.getResult() != null);
+        
+        LOGGER.info("Found " + numExpanded + " possible expansions to simplify constraint");
+        return originalConstraint;
     }