14 files changed, 64 insertions, 22 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fbf249e7f..290fca6bc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -37,6 +37,8 @@ set(regress_0_tests
   regress0/arith/issue3413.smt2
   regress0/arith/issue3480.smt2
   regress0/arith/issue3683.smt2
+  regress0/arith/issue4367.smt2
+  regress0/arith/issue4525.smt2
   regress0/arith/ite-lift.smt2
   regress0/arith/leq.01.smtv1.smt2
   regress0/arith/miplib.cvc
@@ -538,6 +540,7 @@ set(regress_0_tests
   regress0/ho/ho-matching-nested-app.smt2
   regress0/ho/ho-std-fmf.smt2
   regress0/ho/hoa0008.smt2
+  regress0/ho/issue4477.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2
@@ -737,6 +740,8 @@ set(regress_0_tests
   regress0/quantifiers/issue3655.smt2
   regress0/quantifiers/issue4086-infs.smt2
   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
+  regress0/quantifiers/issue4437-unc-quant.smt2
+  regress0/quantifiers/issue4476-ext-rew.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
@@ -1123,8 +1128,6 @@ set(regress_0_tests
   regress0/uflra/simple.03.cvc
   regress0/uflra/simple.04.cvc
   regress0/unconstrained/4481.smt2
-  regress0/unconstrained/4484.smt2
-  regress0/unconstrained/4486.smt2
   regress0/unconstrained/arith.smt2
   regress0/unconstrained/arith3.smt2
   regress0/unconstrained/arith4.smt2
@@ -1197,6 +1200,7 @@ set(regress_0_tests
 # Regression level 1 tests
 
 set(regress_1_tests
+  regress1/abduct-dt.smt2
   regress1/arith/arith-int-004.cvc
   regress1/arith/arith-int-011.cvc
   regress1/arith/arith-int-012.cvc
@@ -1312,6 +1316,7 @@ set(regress_1_tests
   regress1/fmf/issue3626.smt2
   regress1/fmf/issue3689.smt2
   regress1/fmf/issue4068-si-qf.smt2
+  regress1/fmf/issue4225-univ-fun.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/ko-bound-set.cvc
diff --git a/test/regress/README.md b/test/regress/README.md
index 28ccfb96b..0dc1d4eb8 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -12,7 +12,7 @@ By default, each invocation of CVC4 is done with a 10 minute timeout. To use a
 different timeout, set the `TEST_TIMEOUT` environment variable:
 
 ```
-TEST_TIMEOUT=0.5 make regress0
+TEST_TIMEOUT=0.5 ctest -L regress0
 ```
 
 This runs regression tests from level 0 with a 0.5 second timeout.
diff --git a/test/regress/regress0/arith/issue3480.smt2 b/test/regress/regress0/arith/issue3480.smt2
index 7609ad3e7..74ce8d32b 100644
--- a/test/regress/regress0/arith/issue3480.smt2
+++ b/test/regress/regress0/arith/issue3480.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --quiet
+; COMMAND-LINE: --theoryof-mode=type --quiet
 (set-logic QF_NIA)
 (declare-fun a () Int)
 (declare-fun b () Int)
diff --git a/test/regress/regress0/arith/issue4367.smt2 b/test/regress/regress0/arith/issue4367.smt2
new file mode 100644
index 000000000..abe5b09fd
--- /dev/null
+++ b/test/regress/regress0/arith/issue4367.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --incremental --check-unsat-cores
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic NRA)
+(declare-const r0 Real)
+(assert (! (forall ((q0 Bool) (q1 Real)) (= (* r0 r0) r0 r0)) :named IP_2))
+(assert (! (not (forall ((q2 Real)) (not (<= 55.033442 r0 55.033442 q2)))) :named IP_5))
+(push 1)
+(check-sat)
+(pop 1)
+(check-sat)
diff --git a/test/regress/regress0/arith/issue4525.smt2 b/test/regress/regress0/arith/issue4525.smt2
new file mode 100644
index 000000000..ae7e00990
--- /dev/null
+++ b/test/regress/regress0/arith/issue4525.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_NRAT)
+(assert (> (cot 0.0) (/ 1 0)))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress0/ho/issue4477.smt2 b/test/regress/regress0/ho/issue4477.smt2
new file mode 100644
index 000000000..7162d260c
--- /dev/null
+++ b/test/regress/regress0/ho/issue4477.smt2
@@ -0,0 +1,11 @@
+; REQUIRES: no-competition
+; SCRUBBER: grep -o "Symbol '->' not declared"
+; EXPECT: Symbol '->' not declared 
+; EXIT: 1
+(set-logic ALL)
+(declare-sort s 0)
+(declare-fun a () s)
+(declare-fun b () s)
+(declare-fun c (s) s)
+(assert (forall ((d (-> s s))) (distinct (d a) (c a) b)))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2 b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2
new file mode 100644
index 000000000..61f792999
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4437-unc-quant.smt2
@@ -0,0 +1,7 @@
+; EXPECT: (error "Parse Error: issue4437-unc-quant.smt2:6.15: Quantifier used in non-quantified logic.")
+; EXIT: 1
+(set-logic QF_AUFBVLIA)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (forall ((c (_ BitVec 8))) (= (bvashr c a) b)))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
new file mode 100644
index 000000000..c54254e67
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
@@ -0,0 +1,5 @@
+(set-logic NRA)
+(set-info :status sat)
+(set-option :ext-rewrite-quant true)
+(assert (exists ((a Real) (b Real)) (forall ((c Real)) (= (/ b (/ 1 c)) 0))))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2
index 028607093..19179f4d7 100644
--- a/test/regress/regress0/unconstrained/4481.smt2
+++ b/test/regress/regress0/unconstrained/4481.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --unconstrained-simp
-; EXPECT: unsat
+; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.")
+; EXIT: 1
 (set-logic ALL)
 (set-info :status unsat)
 (declare-fun a () Int)
diff --git a/test/regress/regress0/unconstrained/4484.smt2 b/test/regress/regress0/unconstrained/4484.smt2
deleted file mode 100644
index f2f11295b..000000000
--- a/test/regress/regress0/unconstrained/4484.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --unconstrained-simp
-; EXPECT: unsat
-(set-logic QF_NIRA)
-(set-info :status unsat)
-(declare-fun a () Real)
-(assert (= (to_int a) 2))
-(assert (= (to_int (/ a 2.0)) 2))
-(check-sat)
diff --git a/test/regress/regress0/unconstrained/4486.smt2 b/test/regress/regress0/unconstrained/4486.smt2
deleted file mode 100644
index 01771ce66..000000000
--- a/test/regress/regress0/unconstrained/4486.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --unconstrained-simp
-; EXPECT: sat
-(set-logic ALL)
-(set-info :status sat)
-(declare-fun x () Real)
-(assert (is_int x))
-(assert (is_int (+ x 1)))
-(check-sat)
diff --git a/test/regress/regress1/abduct-dt.smt2 b/test/regress/regress1/abduct-dt.smt2
new file mode 100644
index 000000000..d72d15a21
--- /dev/null
+++ b/test/regress/regress1/abduct-dt.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(assert (distinct x nil))
+(get-abduct A (= x (cons (head x) (tail x))))
diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2
new file mode 100644
index 000000000..9946a4567
--- /dev/null
+++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --finite-model-find --uf-ho
+; EXPECT: unknown
+(set-logic ALL)
+; this is not handled by fmf
+(assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0))))
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 63a95bb78..6109a01dd 100644
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.6)
-(set-logic QF_SLIA)
+(set-logic SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)