diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index b762f563129aa5f9d69371bccb95fc6237156a9b..cc283c12dafbbc5db94e35303412339364ebcbe3 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -76,7 +76,7 @@ public class TLC4B {
 		for (int i = 0; i < 10; i++) {
 			s += i;
 		}
-		
+
 		System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing")
 				+ " ms");
 		System.out.println("Translation time: " + StopWatch.getRunTime("Pure")
@@ -157,9 +157,26 @@ public class TLC4B {
 			} else if (args[index].toLowerCase().equals("-testscript")) {
 				TLC4BGlobals.setRunTestscript(true);
 			} else if (args[index].toLowerCase().equals("-notrace")) {
-
+				TLC4BGlobals.setCreateTraceFile(false);
 			} else if (args[index].toLowerCase().equals("-del")) {
 				TLC4BGlobals.setDeleteOnExit(true);
+			} else if (args[index].toLowerCase().equals("-maxint")) {
+				index = index + 1;
+				if (index == args.length) {
+					throw new TLC4BIOException(
+							"Error: Number requiered after option '-maxnint'.");
+				}
+				int maxint = Integer.parseInt(args[index]);
+				TLC4BGlobals.setMAX_INT(maxint);
+			} else if (args[index].toLowerCase().equals("-minint")) {
+				index = index + 1;
+				if (index == args.length) {
+					throw new TLC4BIOException(
+							"Error: Number requiered after option '-minint'.");
+				}
+				int minint = Integer.parseInt(args[index]);
+				TLC4BGlobals.setMIN_INT(minint);
+				;
 			} else if (args[index].toLowerCase().equals("-workers")) {
 				index = index + 1;
 				if (index == args.length) {
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 425a40569503c23db5e1080f0cfc533650d776f4..1be55ae44129252f15cea4bc8eafbba961a85bfe 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -926,7 +926,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		} else {
 			node.getPredicate().apply(this);
 		}
-		
+
 		tlaModuleString.append(" /\\ ");
 		node.getSubstitution().apply(this);
 		printUnchangedVariables(node, true);
@@ -1323,21 +1323,22 @@ public class TLAPrinter extends DepthFirstAdapter {
 	@Override
 	public void caseAIntSetExpression(AIntSetExpression node) {
 		inAIntSetExpression(node);
-		tlaModuleString.append("Int");
+		tlaModuleString.append("(" + TLC4BGlobals.getMIN_INT() + ".."
+				+ TLC4BGlobals.getMAX_INT() + ")");
 		outAIntSetExpression(node);
 	}
 
 	@Override
 	public void caseANatSetExpression(ANatSetExpression node) {
 		inANatSetExpression(node);
-		tlaModuleString.append("Nat");
+		tlaModuleString.append("(0.." + TLC4BGlobals.getMAX_INT() + ")");
 		outANatSetExpression(node);
 	}
 
 	@Override
 	public void caseANat1SetExpression(ANat1SetExpression node) {
 		inANat1SetExpression(node);
-		tlaModuleString.append("(Nat \\ {0})");
+		tlaModuleString.append("(1.." + TLC4BGlobals.getMAX_INT() + ")");
 		outANat1SetExpression(node);
 	}
 
@@ -2057,14 +2058,14 @@ public class TLAPrinter extends DepthFirstAdapter {
 	@Override
 	public void caseACardExpression(ACardExpression node) {
 		BType type = typechecker.getType(node.getExpression());
-		if(type instanceof FunctionType){
+		if (type instanceof FunctionType) {
 			tlaModuleString.append("Cardinality(DOMAIN(");
 			node.getExpression().apply(this);
 			tlaModuleString.append("))");
-		}else{
+		} else {
 			tlaModuleString.append("Cardinality(");
 			node.getExpression().apply(this);
-			tlaModuleString.append(")");	
+			tlaModuleString.append(")");
 		}
 	}
 
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 4a16b11c402cda773c6eff5597475a9af120dd5e..936163d177223e298929c0f93788de3091c566f2 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -108,9 +108,6 @@ public class TestUtil {
 		//parse check
 		translateTLA2B(name, b2tlaTranslator.getModuleString(),
 				b2tlaTranslator.getConfigString());
-		// de.tla2b.translation.Tla2BTranslator.translateString(name,
-		// b2tlaTranslator.getModuleString(),
-		// b2tlaTranslator.getConfigString());
 
 		assertEquals(expectedModule, b2tlaTranslator.getModuleString());
 		assertEquals(expectedConfig, b2tlaTranslator.getConfigString());