Mark QuantifierEliminationBenchmarks and QuantifierEliminationTodos w…

…ith NoRegression (#611)
ultimate-pa · Feb 27, 2023 · 5cbf4d7 · 5cbf4d7
1 parent ff99305
commit 5cbf4d7
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/...i_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationBenchmarks.java b/...i_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,13 +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 simply for benchmarking and should not run as regression tests.
+@Category(NoRegression.class)
 public class QuantifierEliminationBenchmarks {
 
 	/**

diff --git a/...de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/QuantifierEliminationTodos.java b/...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 {
 
 	/**