Merge branch 'master' into issue7504issue7504

38 files changed, 407 insertions, 22 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 4811cca1b..f6c1cf8df 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -52,6 +52,7 @@ cvc5_add_api_test(two_solvers)
 cvc5_add_api_test(issue5074)
 cvc5_add_api_test(issue4889)
 cvc5_add_api_test(issue6111)
+cvc5_add_api_test(proj-issue306)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/proj-issue306.cpp b/test/api/proj-issue306.cpp
new file mode 100644
index 000000000..664536a0b
--- /dev/null
+++ b/test/api/proj-issue306.cpp
@@ -0,0 +1,21 @@
+#include "api/cpp/cvc5.h"
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("check-proofs", "true");
+  slv.setOption("proof-check", "eager");
+  Sort s1 = slv.getBooleanSort();
+  Sort s3 = slv.getStringSort();
+  Term t1 = slv.mkConst(s3, "_x0");
+  Term t3 = slv.mkConst(s1, "_x2");
+  Term t11 = slv.mkString("");
+  Term t14 = slv.mkConst(s3, "_x11");
+  Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1);
+  Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11);
+  Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42);
+  slv.assertFormula(t95);
+  slv.checkSatAssuming({t58});
+}
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 6052a057f..04a275741 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -422,6 +422,17 @@ def test_mk_floating_point(solver):
     with pytest.raises(RuntimeError):
         slv.mkFloatingPoint(3, 5, t1)
 
+def test_mk_cardinality_constraint(solver):
+    su = solver.mkUninterpretedSort("u")
+    si = solver.getIntegerSort()
+    solver.mkCardinalityConstraint(su, 3)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.mkCardinalityConstraint(si, 3))
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.mkCardinalityConstraint(su, 0))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkCardinalityConstraint(su, 3)
 
 def test_mk_empty_set(solver):
     slv = pycvc5.Solver()
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5dd456b9f..a3fd70683 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -449,6 +449,7 @@ set(regress_0_tests
   regress0/cores/issue4971-2.smt2
   regress0/cores/issue4971-3.smt2
   regress0/cores/issue5079.smt2
+  regress0/cores/issue5234-uc-ua.smt2
   regress0/cores/issue5238.smt2
   regress0/cores/issue5902.smt2
   regress0/cores/issue5908.smt2
@@ -650,12 +651,16 @@ set(regress_0_tests
   regress0/ho/issue4990-care-graph.smt2
   regress0/ho/issue5233-part1-usort-owner.smt2
   regress0/ho/issue5371.smt2
+  regress0/ho/issue5741-1-cg-model.smt2
+  regress0/ho/issue5741-3-cg-model.smt2
+  regress0/ho/issue5744-cg-model.smt2
   regress0/ho/issue6526.smt2
   regress0/ho/issue6536.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
   regress0/ho/match-middle.smt2
   regress0/ho/modulo-func-equality.smt2
+  regress0/ho/qgu-fuzz-ho-1-dd.smt2
   regress0/ho/shadowing-defs.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2
@@ -774,6 +779,7 @@ set(regress_0_tests
   regress0/options/set-and-get-options.smt2
   regress0/options/statistics.smt2
   regress0/options/stream-printing.smt2
+  regress0/options/version.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
@@ -856,8 +862,11 @@ set(regress_0_tests
   regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/open-pf-rederivation.smt2
+  regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
+  regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
+  regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
   regress0/proofs/scope.smt2
   regress0/proofs/trust-subs-eq-open.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
@@ -890,6 +899,7 @@ set(regress_0_tests
   regress0/push-pop/issue1986.smt2
   regress0/push-pop/issue2137.min.smt2
   regress0/push-pop/issue6535-inc-solve.smt2
+  regress0/push-pop/issue7479-global-decls.smt2
   regress0/push-pop/quant-fun-proc-unfd.smt2
   regress0/push-pop/real-as-int-incremental.smt2
   regress0/push-pop/simple_unsat_cores.smt2
@@ -992,6 +1002,8 @@ set(regress_0_tests
   regress0/rels/join-eq-u.cvc.smt2
   regress0/rels/joinImg_0.cvc.smt2
   regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+  regress0/rels/qgu-fuzz-relations-1.smt2
+  regress0/rels/qgu-fuzz-relations-1-dd.smt2
   regress0/rels/rel_1tup_0.cvc.smt2
   regress0/rels/rel_complex_0.cvc.smt2
   regress0/rels/rel_complex_1.cvc.smt2
@@ -1234,6 +1246,7 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/parser-syms.cvc.smt2
+  regress0/strings/proj-issue316-regexp-ite.smt2
   regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
@@ -1452,6 +1465,7 @@ set(regress_0_tests
   regress0/unconstrained/geq.smt2
   regress0/unconstrained/gt.smt2
   regress0/unconstrained/issue4644.smt2
+  regress0/unconstrained/issue4656-bool-term-vars.smt2
   regress0/unconstrained/ite.smt2
   regress0/unconstrained/leq.smt2
   regress0/unconstrained/lt.smt2
@@ -1569,9 +1583,14 @@ set(regress_1_tests
   regress1/bags/duplicate_removal1.smt2
   regress1/bags/duplicate_removal2.smt2
   regress1/bags/emptybag1.smt2
+  regress1/bags/fuzzy1.smt2
+  regress1/bags/fuzzy2.smt2
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
+  regress1/bags/map1.smt2
+  regress1/bags/map2.smt2
+  regress1/bags/map3.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
   regress1/bags/union_disjoint.smt2
@@ -1700,6 +1719,9 @@ set(regress_1_tests
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
   regress1/ho/issue4134-sinf.smt2
+  regress1/ho/issue4758.smt2
+  regress1/ho/issue5078-small.smt2
+  regress1/ho/issue5201-1.smt2
   regress1/ho/issue5741-3.smt2
   regress1/ho/NUM638^1.smt2
   regress1/ho/NUM925^1.p
@@ -1796,6 +1818,7 @@ set(regress_1_tests
   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
   regress1/proofs/qgu-fuzz-1-strings-pp.smt2
+  regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
   regress1/proofs/quant-alpha-eq.smt2
   regress1/proofs/sat-trivial-cycle.smt2
   regress1/proofs/unsat-cores-proofs.smt2
@@ -1954,6 +1977,7 @@ set(regress_1_tests
   regress1/quantifiers/issue6699-nc-shadow.smt2
   regress1/quantifiers/issue6775-vts-int.smt2
   regress1/quantifiers/issue6845-nl-lemma-tc.smt2
+  regress1/quantifiers/issue7385-sygus-inst-i.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
@@ -2257,6 +2281,7 @@ set(regress_1_tests
   regress1/strings/issue6653-4-rre.smt2
   regress1/strings/issue6653-rre.smt2
   regress1/strings/issue6653-rre-small.smt2
+  regress1/strings/issue6766-re-elim-bv.smt2
   regress1/strings/issue6777-seq-nth-eval-cm.smt2
   regress1/strings/issue6913.smt2
   regress1/strings/issue6973-dup-lemma-conc.smt2
@@ -2272,6 +2297,7 @@ set(regress_1_tests
   regress1/strings/nf-ff-contains-abs.smt2
   regress1/strings/no-lazy-pp-quant.smt2
   regress1/strings/non_termination_regular_expression4.smt2
+  regress1/strings/non-terminating-rewrite-aent.smt2
   regress1/strings/norn-13.smt2
   regress1/strings/norn-360.smt2
   regress1/strings/norn-ab.smt2
@@ -2280,6 +2306,7 @@ set(regress_1_tests
   regress1/strings/nt6-dd.smt2
   regress1/strings/nterm-re-inter-sigma.smt2
   regress1/strings/open-pf-merge.smt2
+  regress1/strings/pattern1.smt2
   regress1/strings/pierre150331.smt2
   regress1/strings/policy_variable.smt2
   regress1/strings/pre_ctn_no_skolem_share.smt2
@@ -2631,6 +2658,7 @@ set(regress_2_tests
   regress2/sygus/pbe_bvurem.sy
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
+  regress2/sygus/qgu-bools.sy
   regress2/sygus/real-grammar-neg.sy
   regress2/sygus/sets-fun-test.sy
   regress2/sygus/sumn_recur_synth.sy
diff --git a/test/regress/regress0/cores/issue5234-uc-ua.smt2 b/test/regress/regress0/cores/issue5234-uc-ua.smt2
new file mode 100644
index 000000000..ab31ec71f
--- /dev/null
+++ b/test/regress/regress0/cores/issue5234-uc-ua.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; EXPECT: ()
+(set-option :incremental true)
+(set-option :check-unsat-cores true)
+(set-option :produce-unsat-assumptions true)
+(set-logic ALL)
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(assert (distinct a b c))
+(check-sat-assuming (c))
+(get-unsat-assumptions)
diff --git a/test/regress/regress0/ho/issue5741-1-cg-model.smt2 b/test/regress/regress0/ho/issue5741-1-cg-model.smt2
new file mode 100644
index 000000000..8989acdc4
--- /dev/null
+++ b/test/regress/regress0/ho/issue5741-1-cg-model.smt2
@@ -0,0 +1,18 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun a ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+(declare-fun c () (_ BitVec 1))
+(declare-fun d () (_ BitVec 32))
+(declare-fun e () (_ BitVec 32))
+(declare-fun f () (_ BitVec 32))
+(declare-fun g ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun h () (_ BitVec 32))
+(declare-fun i () (_ BitVec 32))
+(declare-fun j () (_ BitVec 1))
+(declare-fun k () (_ BitVec 32))
+(assert (= b (a d e)))
+(assert (= f (g h i)))
+(assert (distinct j (ite (= i k) (_ bv1 1) (_ bv0 1))))
+(assert (= (ite (= i b) (_ bv1 1) (_ bv0 1)) j (ite (= c (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(check-sat)
diff --git a/test/regress/regress0/ho/issue5741-3-cg-model.smt2 b/test/regress/regress0/ho/issue5741-3-cg-model.smt2
new file mode 100644
index 000000000..abc4b76a6
--- /dev/null
+++ b/test/regress/regress0/ho/issue5741-3-cg-model.smt2
@@ -0,0 +1,5 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun p ((_ BitVec 17) (_ BitVec 16)) Bool)
+(assert (p (_ bv0 17) ((_ sign_extend 15) (ite (p (_ bv0 17) (_ bv0 16)) (_ bv1 1) (_ bv0 1)))))
+(check-sat)
diff --git a/test/regress/regress0/ho/issue5744-cg-model.smt2 b/test/regress/regress0/ho/issue5744-cg-model.smt2
new file mode 100644
index 000000000..5650351cd
--- /dev/null
+++ b/test/regress/regress0/ho/issue5744-cg-model.smt2
@@ -0,0 +1,7 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun r4 () Real)
+(declare-fun ufrb5 (Real Real Real Real Real) Bool)
+(assert (ufrb5 0.0 0.0 0.0 0.0 0))
+(assert (ufrb5 (+ r4 r4) 0.0 1 0.0 0.0))
+(check-sat)
diff --git a/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2 b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2
new file mode 100644
index 000000000..840db92a9
--- /dev/null
+++ b/test/regress/regress0/ho/qgu-fuzz-ho-1-dd.smt2
@@ -0,0 +1,6 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-const b (-> Int Int Int))
+(declare-const c (-> Int Int))
+(assert (and (= c (b 1)) (= c (b 0)) (> (b 1 0) 0) (> 0 (b 0 1)) (= 0 (c (b 0 0)))))
+(check-sat)
diff --git a/test/regress/regress0/options/version.smt2 b/test/regress/regress0/options/version.smt2
new file mode 100644
index 000000000..755b6ccca
--- /dev/null
+++ b/test/regress/regress0/options/version.smt2
@@ -0,0 +1,3 @@
+; COMMAND-LINE: --version
+; EXPECT: This is cvc5 version
+; SCRUBBER: grep -o "This is cvc5 version"
\ No newline at end of file
diff --git a/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 b/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
new file mode 100644
index 000000000..0f7f89651
--- /dev/null
+++ b/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const __ (_ BitVec 1))
+(set-option :incremental true)
+(check-sat-assuming ((bvsgt ((_ sign_extend 42) (bvcomp ((_ zero_extend 10) __) ((_ zero_extend 10) __))) (_ bv0 43))))
+(check-sat-assuming ((bvsgt ((_ sign_extend 42) (bvcomp ((_ zero_extend 10) __) ((_ zero_extend 10) __))) (_ bv0 43))))
\ No newline at end of file
diff --git a/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
new file mode 100644
index 000000000..27836734b
--- /dev/null
+++ b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (and (= a (ite (or c d) d a)) (not (ite d a false)) (ite c a d)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2 b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
new file mode 100644
index 000000000..8eef0674b
--- /dev/null
+++ b/test/regress/regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (and (or d (ite c false true)) (not (= d (or b c))) (= d (ite c d (not d)))))
+(check-sat)
diff --git a/test/regress/regress0/push-pop/issue7479-global-decls.smt2 b/test/regress/regress0/push-pop/issue7479-global-decls.smt2
new file mode 100644
index 000000000..ddf89960e
--- /dev/null
+++ b/test/regress/regress0/push-pop/issue7479-global-decls.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -i
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :global-declarations true)
+(define-fun y () Bool (> 0 0))
+(assert y)
+(push)
+(check-sat)
diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2
new file mode 100644
index 000000000..52ee0b1c0
--- /dev/null
+++ b/test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun d () (Tuple Int Int))
+(assert (= (as emptyset (Set (Tuple Int Int))) (join (singleton (tuple 1 0)) (singleton d))))
+(check-sat)
diff --git a/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2 b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2
new file mode 100644
index 000000000..b489ce65b
--- /dev/null
+++ b/test/regress/regress0/rels/qgu-fuzz-relations-1.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Set (Tuple Int Int)))
+(declare-fun b () (Set (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert (and (= b (singleton (tuple 1 0))) (= a (join b (transpose a))) (= a (join b (tclosure a))) (= a (join b (singleton d)))))
+(check-sat)
diff --git a/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2 b/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2
new file mode 100644
index 000000000..e19accd36
--- /dev/null
+++ b/test/regress/regress0/strings/proj-issue316-regexp-ite.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --theoryof-mode=type
+; COMMAND-LINE: --theoryof-mode=term
+; SCRUBBER: grep -o "ITE branches of type RegLan are currently not supported"
+; EXPECT: ITE branches of type RegLan are currently not supported
+; EXIT: 1 
+(set-logic QF_SLIA)
+(declare-const b Bool)
+(declare-const x String)
+(assert (str.in_re x (ite b re.none re.allchar)))
+(check-sat)
diff --git a/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2
new file mode 100644
index 000000000..cd6154464
--- /dev/null
+++ b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLIA)
+(set-info :status unsat)
+(declare-fun a (Bool) Bool)
+(declare-fun b (Bool) Bool)
+(declare-fun c (Bool) Bool)
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+(declare-fun f () Bool)
+(assert (distinct (a d) (a e)))
+(assert (distinct (b e) (b f)))
+(assert (distinct (c f) (c d)))
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy1.smt2 b/test/regress/regress1/bags/fuzzy1.smt2
new file mode 100644
index 000000000..f9fee0ec4
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int) ; c here is zero
+(assert
+  (and
+    (= b (difference_subtract b a)) ; b is empty
+    (= a (bag (tuple c 0) 1)))) ; a = {|(<0, 0>, 1)|}
+(check-sat)
diff --git a/test/regress/regress1/bags/fuzzy2.smt2 b/test/regress/regress1/bags/fuzzy2.smt2
new file mode 100644
index 000000000..31da47f53
--- /dev/null
+++ b/test/regress/regress1/bags/fuzzy2.smt2
@@ -0,0 +1,15 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () (Bag (Tuple Int Int)))
+(declare-fun b () (Bag (Tuple Int Int)))
+(declare-fun c () Int)
+(declare-fun d () (Tuple Int Int))
+(assert
+  (let ((D (bag d c))) ; when c = zero, then D is empty
+    (and
+      (= a (bag (tuple 1 1) c)) ; when c = zero, then a is empty
+      (= a (union_max a D))
+      (= a (difference_subtract a (bag d 1)))
+      (= a (union_disjoint a D))
+      (= a (intersection_min a D)))))
+(check-sat)
diff --git a/test/regress/regress1/bags/map.smt2 b/test/regress/regress1/bags/map1.smt2
index 54d671415..54d671415 100644
--- a/test/regress/regress1/bags/map.smt2
+++ b/test/regress/regress1/bags/map1.smt2
diff --git a/test/regress/regress1/bags/map2.smt2 b/test/regress/regress1/bags/map2.smt2
new file mode 100644
index 000000000..faed04caa
--- /dev/null
+++ b/test/regress/regress1/bags/map2.smt2
@@ -0,0 +1,9 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(declare-fun f (Int) Int)
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(check-sat)
diff --git a/test/regress/regress1/bags/map3.smt2 b/test/regress/regress1/bags/map3.smt2
new file mode 100644
index 000000000..637815fa5
--- /dev/null
+++ b/test/regress/regress1/bags/map3.smt2
@@ -0,0 +1,10 @@
+(set-logic HO_ALL)
+(set-info :status unsat)
+(set-option :fmf-bound true)
+(declare-fun A () (Bag Int))
+(declare-fun B () (Bag Int))
+(define-fun f ((x Int)) Int (+ x 1))
+(assert (= B (bag.map f A)))
+(assert (= (bag.count (- 2) B) 57))
+(assert (= A (as emptybag (Bag Int)) ))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue4758.smt2 b/test/regress/regress1/ho/issue4758.smt2
new file mode 100644
index 000000000..dab284c11
--- /dev/null
+++ b/test/regress/regress1/ho/issue4758.smt2
@@ -0,0 +1,6 @@
+(set-logic HO_ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b (Real Real) Real)
+(assert (> (b a 0) (b (- a) 1)))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue5078-small.smt2 b/test/regress/regress1/ho/issue5078-small.smt2
new file mode 100644
index 000000000..21077434a
--- /dev/null
+++ b/test/regress/regress1/ho/issue5078-small.smt2
@@ -0,0 +1,8 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(assert (= (a d 0) (a 0 1)))
+(assert (= d (mod e 3)))
+(check-sat)
diff --git a/test/regress/regress1/ho/issue5201-1.smt2 b/test/regress/regress1/ho/issue5201-1.smt2
new file mode 100644
index 000000000..9f6e058da
--- /dev/null
+++ b/test/regress/regress1/ho/issue5201-1.smt2
@@ -0,0 +1,20 @@
+(set-logic HO_QF_UFLIA)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b (Int Int) Int)
+(declare-fun c (Int Int) Int)
+(declare-fun d () Int)
+(declare-fun e () Int)
+(declare-fun f () Int)
+(declare-fun g () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun k () Int)
+(assert (= d (b j d) a))
+(assert (= e (c e i)))
+(assert (= (b k f) a))
+(assert (= d (+ g 4)))
+(assert (= j (* g 5)))
+(assert (= e (+ g 5)))
+(assert (= k 0))
+(check-sat)
diff --git a/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2 b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
new file mode 100644
index 000000000..b55fb3d49
--- /dev/null
+++ b/test/regress/regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-const x Int)
+(declare-fun b () (Array Int Int))
+(declare-fun y () Int)
+(assert (and (= b (store b x y)) (= b (store b y y)) (= y (ite (> y 0) 0 y)) (= (store b 0 0) (store (store b y 1) 1 1))))
+(check-sat)
diff --git a/test/regress/regress1/push-pop/arith_lra_01.smt2 b/test/regress/regress1/push-pop/arith_lra_01.smt2
index 02e22d685..b16bbdda0 100644
--- a/test/regress/regress1/push-pop/arith_lra_01.smt2
+++ b/test/regress/regress1/push-pop/arith_lra_01.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-produce-proofs
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: sat
diff --git a/test/regress/regress1/push-pop/fuzz_3_6.smt2 b/test/regress/regress1/push-pop/fuzz_3_6.smt2
index 4ad684402..1901016c2 100644
--- a/test/regress/regress1/push-pop/fuzz_3_6.smt2
+++ b/test/regress/regress1/push-pop/fuzz_3_6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental --no-produce-proofs
+; COMMAND-LINE: --incremental
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat
diff --git a/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2 b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
new file mode 100644
index 000000000..26fc1cf7e
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue7385-sygus-inst-i.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic NIRA)
+(push)
+(assert (exists ((q29 Int) (q30 Bool) (q35 Bool)) (= (= 0 q29) (= q35 q30))))
+(push)
+(pop)
+(pop)
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 7249e87aa..465408cc5 100644
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-unsat-cores --no-produce-proofs
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 
 ; Note we require disabling proofs/unsat cores due to timeouts in nightlies
diff --git a/test/regress/regress1/strings/issue6766-re-elim-bv.smt2 b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
new file mode 100644
index 000000000..13677838b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6766-re-elim-bv.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert
+ (str.in_re (str.++ a (ite (str.in_re (str.++ a "BA" b) (re.++ (re.* (str.to_re "A")) (str.to_re "B"))) b a))
+  (re.diff (re.* (str.to_re "A")) (str.to_re ""))))
+(check-sat)
diff --git a/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2 b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
new file mode 100644
index 000000000..211209255
--- /dev/null
+++ b/test/regress/regress1/strings/non-terminating-rewrite-aent.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(assert 
+(let ((_let_1 (str.len a))) (let ((_let_2 (str.len b))) (let ((_let_3 (+ _let_1 (* (- 1) _let_2)))) (let ((_let_4 (ite (>= _let_3 1) (str.substr a 0 _let_3) (str.substr b 0 (+ (* (- 1) _let_1) _let_2))))) (let ((_let_5 (str.len _let_4))) (let ((_let_6 (str.len c))) (let ((_let_7 (+ _let_6 (* (- 1) _let_5)))) (let ((_let_8 (ite (>= _let_7 0) (str.substr c _let_5 _let_7) (str.substr _let_4 _let_6 (+ (* (- 1) _let_6) _let_5))))) (let ((_let_9 (str.len _let_8))) (let ((_let_10 (ite (>= _let_1 _let_9) (str.substr a _let_9 (- _let_1 _let_9)) (str.substr _let_8 _let_1 (- _let_9 _let_1))))) (and (= _let_8 (str.++ a _let_10)) (not (= "" _let_10)) (>= (str.len _let_10) 1))))))))))))
+)
+(check-sat)
diff --git a/test/regress/regress1/strings/pattern1.smt2 b/test/regress/regress1/strings/pattern1.smt2
new file mode 100644
index 000000000..b75fdb9be
--- /dev/null
+++ b/test/regress/regress1/strings/pattern1.smt2
@@ -0,0 +1,73 @@
+(set-option :produce-models true)
+(set-logic QF_SLIA)
+(set-info :status sat)
+(declare-const x String)
+
+(assert
+ (str.in_re
+  x
+  (re.++
+   (str.to_re "pref")
+   (re.* re.allchar)
+   (str.to_re "a")
+   (re.* re.allchar)
+   (str.to_re "b")
+   (re.* re.allchar)
+   (str.to_re "c")
+   (re.* re.allchar)
+   (str.to_re "d")
+   (re.* re.allchar)
+   (str.to_re "e")
+   (re.* re.allchar)
+   (str.to_re "f")
+   (re.* re.allchar)
+   (str.to_re "g")
+   (re.* re.allchar)
+   (str.to_re "h")
+   (re.* re.allchar)
+   (str.to_re "i")
+   (re.* re.allchar)
+   (str.to_re "j")
+   (re.* re.allchar)
+   (str.to_re "k")
+   (re.* re.allchar)
+   (str.to_re "l")
+   (re.* re.allchar)
+   (str.to_re "m")
+   (re.* re.allchar)
+   (str.to_re "n")
+   (re.* re.allchar)
+   (str.to_re "o")
+   (re.* re.allchar)
+   (str.to_re "p")
+   (re.* re.allchar)
+   (str.to_re "q")
+   (re.* re.allchar)
+   (str.to_re "r")
+   (re.* re.allchar)
+   (str.to_re "s")
+   (re.* re.allchar)
+   (str.to_re "t")
+   (re.* re.allchar)
+   (str.to_re "u")
+   (re.* re.allchar)
+   (str.to_re "v")
+   (re.* re.allchar)
+   (str.to_re "w")
+   (re.* re.allchar)
+   (str.to_re "x")
+   (re.* re.allchar)
+   (str.to_re "y")
+   (re.* re.allchar)
+   (str.to_re "z")
+   (re.* re.allchar))))
+
+(assert
+ (or
+  (= x "pref0a-b-c-de")
+  (str.in_re x (re.++ (str.to_re "prefix") (re.* re.allchar)))
+  (str.in_re x (re.++ (re.* re.allchar) (str.to_re "test") (re.* re.allchar)))))
+
+(check-sat)
+
+
diff --git a/test/regress/regress2/sygus/qgu-bools.sy b/test/regress/regress2/sygus/qgu-bools.sy
new file mode 100644
index 000000000..35445e927
--- /dev/null
+++ b/test/regress/regress2/sygus/qgu-bools.sy
@@ -0,0 +1,21 @@
+; COMMAND-LINE: --sygus-query-gen=unsat --sygus-abort-size=2
+; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
+; SCRUBBER: grep -v -E '(\(define-fun|\(query)'
+; EXIT: 1
+(set-logic ALL)
+(synth-fun P ((a Bool) (b Bool) (c Bool)) Bool
+((Start Bool))
+(
+(Start Bool (
+a
+b
+c
+(not Start)
+(= Start Start)
+(or Start Start)
+(ite Start Start Start)
+))
+))
+
+
+(check-synth)
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 35e718b0f..8e22b04a8 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -260,7 +260,7 @@ class DumpTester(Tester):
                 "--parse-only",
                 "-o",
                 "raw-benchmark",
-                f"--output-lang={ext_to_lang[benchmark_info.benchmark_ext]}",
+                "--output-lang={}".format(ext_to_lang[benchmark_info.benchmark_ext]),
             ]
             dump_output, _, _ = run_process(
                 [benchmark_info.cvc5_binary]
@@ -282,7 +282,7 @@ class DumpTester(Tester):
                 command_line_args=benchmark_info.command_line_args
                 + [
                     "--parse-only",
-                    f"--lang={ext_to_lang[benchmark_info.benchmark_ext]}",
+                    "--lang={}".format(ext_to_lang[benchmark_info.benchmark_ext]),
                 ],
                 benchmark_basename=tmpf.name,
                 expected_output="",
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 8511827a8..1f88add2d 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -387,16 +387,6 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
   }
 
-  @Test void mkUninterpretedConst() throws CVC5ApiException
-  {
-    assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1));
-    Solver slv = new Solver();
-    assertThrows(
-        CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  }
-
   @Test void mkAbstractValue() throws CVC5ApiException
   {
     assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
@@ -434,6 +424,20 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
   }
 
+  @Test void mkCardinalityConstraint() throws CVC5ApiException
+  {
+    Sort su = d_solver.mkUninterpretedSort("u");
+    Sort si = d_solver.getIntegerSort();
+    assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+  }
+
   @Test void mkEmptySet() throws CVC5ApiException
   {
     Solver slv = new Solver();
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 32122e619..bcac315a7 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -248,8 +248,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
       a,
       d_nodeManager->mkNode(kind::PLUS, x, d_nodeManager->mkConst(Rational(1))),
       x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "A" (+ x (str.len s2)) x) -> ""
   n = d_nodeManager->mkNode(
@@ -258,8 +257,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
       d_nodeManager->mkNode(
           kind::PLUS, x, d_nodeManager->mkNode(kind::STRING_LENGTH, s)),
       x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "A" x y) -> (str.substr "A" x y)
   n = d_nodeManager->mkNode(kind::STRING_SUBSTR, a, x, y);
@@ -271,14 +269,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
                             abcd,
                             d_nodeManager->mkNode(kind::PLUS, x, three),
                             x);
-  res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, empty);
+  sameNormalForm(n, empty);
 
   // (str.substr "ABCD" (+ x 2) x) -> (str.substr "ABCD" (+ x 2) x)
   n = d_nodeManager->mkNode(
       kind::STRING_SUBSTR, abcd, d_nodeManager->mkNode(kind::PLUS, x, two), x);
   res = sr.rewriteSubstr(n);
-  ASSERT_EQ(res, n);
+  sameNormalForm(res, n);
 
   // (str.substr (str.substr s x x) x x) -> ""
   n = d_nodeManager->mkNode(kind::STRING_SUBSTR,