diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationBenchmarks.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationBenchmarks.java
index 274685de71c..29546909c3f 100644
--- a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationBenchmarks.java
+++ b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationBenchmarks.java
@@ -33,6 +33,7 @@
 import org.junit.Before;
 import org.junit.BeforeClass;
 import org.junit.Test;
+import org.junit.experimental.categories.Category;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel;
@@ -43,6 +44,7 @@
 import de.uni_freiburg.informatik.ultimate.logic.LoggingScript;
 import de.uni_freiburg.informatik.ultimate.logic.Logics;
 import de.uni_freiburg.informatik.ultimate.logic.Script;
+import de.uni_freiburg.informatik.ultimate.test.junitextension.categories.NoRegression;
 import de.uni_freiburg.informatik.ultimate.test.mocks.UltimateMocks;
 
 /**
@@ -50,6 +52,8 @@
  * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
  *
  */
+// These tests are simply for benchmarking and should not run as regression tests.
+@Category(NoRegression.class)
 public class QuantifierEliminationBenchmarks {
 
 	/**
diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationTodos.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationTodos.java
index d4c70b6e790..59981609aaa 100644
--- a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationTodos.java
+++ b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationTodos.java
@@ -33,6 +33,7 @@
 import org.junit.Before;
 import org.junit.BeforeClass;
 import org.junit.Test;
+import org.junit.experimental.categories.Category;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger.LogLevel;
@@ -43,14 +44,16 @@
 import de.uni_freiburg.informatik.ultimate.logic.LoggingScript;
 import de.uni_freiburg.informatik.ultimate.logic.Logics;
 import de.uni_freiburg.informatik.ultimate.logic.Script;
+import de.uni_freiburg.informatik.ultimate.test.junitextension.categories.NoRegression;
 import de.uni_freiburg.informatik.ultimate.test.mocks.UltimateMocks;
 
-
 /**
  *
  * @author Matthias Heizmann (heizmann@informatik.uni-freiburg.de)
  *
  */
+// These tests are work in progress and should not run as regression tests.
+@Category(NoRegression.class)
 public class QuantifierEliminationTodos {
 
 	/**