diff options
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 28 |
1 files changed, 28 insertions, 0 deletions
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 |