8 files changed, 2 insertions, 34 deletions
diff --git a/test/regress/regress0/bug512.minimized.smt2 b/test/regress/regress0/bug512.minimized.smt2
index 0b19f26df..1a2aaf56f 100644
--- a/test/regress/regress0/bug512.minimized.smt2
+++ b/test/regress/regress0/bug512.minimized.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --tlimit-per 1000
 ; EXPECT: unknown
 (set-logic UF)
 (declare-sort T 0)
diff --git a/test/regress/regress0/bug519.smt2 b/test/regress/regress0/bug519.smt2
index 22fdff674..406cb0c1b 100644
--- a/test/regress/regress0/bug519.smt2
+++ b/test/regress/regress0/bug519.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: -mi
+; COMMAND-LINE: -mi --tlimit-per 1000
 ; EXPECT: unknown
 ; EXPECT: unsat
 
diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index 366204191..90a18f0e2 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -25,7 +25,6 @@ TESTS =	\
 	bitvec5.smt \
 	quant-Arrays_Q1-noinfer.smt2 \
 	quant-ex1.smt2 \
-	quant-ex1.disable_miniscope.smt2 \
 	uflia-xs-09-16-3-4-1-5.delta03.smt \
 	aufbv-fuzz01.smt \
 	bug347.smt \
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 93d513d9f..c478248da 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -28,10 +28,8 @@ TESTS =	\
 	bug269.smt2 \
 	burns13.smt2 \
 	burns4.smt2 \
-	ex1.smt2 \
 	ex3.smt2 \
 	ex6.smt2 \
-	ex7.smt2 \
 	opisavailable-12.smt2 \
 	ricart-agrawala6.smt2 \
 	set8.smt2 \
diff --git a/test/regress/regress0/quantifiers/ex1.smt2 b/test/regress/regress0/quantifiers/ex1.smt2
deleted file mode 100644
index 20230a6fa..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun f (U) U)
-(declare-fun p () Bool)
-(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex1.smt2.expect b/test/regress/regress0/quantifiers/ex1.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex1.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
deleted file mode 100644
index 11a83fdc4..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ /dev/null
@@ -1,13 +0,0 @@
-(set-logic AUFLIRA)
-(set-info :smt-lib-version 2.0)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-sort U 0)
-(declare-fun a () U)
-(declare-fun b () U)
-(declare-fun c () U)
-(declare-fun f (U) U)
-(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
-(check-sat)
-(get-info :reason-unknown)
-(exit)
diff --git a/test/regress/regress0/quantifiers/ex7.smt2.expect b/test/regress/regress0/quantifiers/ex7.smt2.expect
deleted file mode 100644
index 2bd8349de..000000000
--- a/test/regress/regress0/quantifiers/ex7.smt2.expect
+++ /dev/null
@@ -1,2 +0,0 @@
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)