summaryrefslogtreecommitdiff
path: root/test/regress/CMakeLists.txt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/CMakeLists.txt')
-rw-r--r--test/regress/CMakeLists.txt11
1 files changed, 9 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b08b2f6f5..bffb3e8cb 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -109,6 +109,7 @@ set(regress_0_tests
regress0/arrays/issue3813-massign-assert.smt2
regress0/arrays/issue3814.smt2
regress0/arrays/issue4927-unsat-cores.smt2
+ regress0/arrays/issue7596-define-array-uminus.smt2
regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
regress0/arrays/x2.smtv1.smt2
regress0/arrays/x3.smtv1.smt2
@@ -659,11 +660,14 @@ set(regress_0_tests
regress0/ho/issue6536.smt2
regress0/ho/ite-apply-eq.smt2
regress0/ho/lambda-equality-non-canon.smt2
+ regress0/ho/lazy-lambda-model.smt2
regress0/ho/match-middle.smt2
regress0/ho/modulo-func-equality.smt2
regress0/ho/qgu-fuzz-ho-1-dd.smt2
regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
regress0/ho/shadowing-defs.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
regress0/ho/simple-matching-partial.smt2
regress0/ho/simple-matching.smt2
regress0/ho/trans.smt2
@@ -1083,6 +1087,7 @@ set(regress_0_tests
regress0/seq/issue5665-invalid-model.smt2
regress0/seq/issue6337-seq.smt2
regress0/seq/len_simplify.smt2
+ regress0/seq/proj-issue340.smt2
regress0/seq/seq-2var.smt2
regress0/seq/seq-ex1.smt2
regress0/seq/seq-ex2.smt2
@@ -1599,9 +1604,11 @@ set(regress_1_tests
regress1/bags/fuzzy3.smt2
regress1/bags/fuzzy4.smt2
regress1/bags/fuzzy5.smt2
+ regress1/bags/fuzzy6.smt2
regress1/bags/intersection_min1.smt2
regress1/bags/intersection_min2.smt2
regress1/bags/issue5759.smt2
+ regress1/bags/map-lazy-lam.smt2
regress1/bags/map1.smt2
regress1/bags/map2.smt2
regress1/bags/map3.smt2
@@ -1726,8 +1733,10 @@ set(regress_1_tests
regress1/fmf/with-ind-104-core.smt2
regress1/gensys_brn001.smt2
regress1/ho/bug_freeVar_BDD_General_data_270.p
+ regress1/ho/bug_freevar_PHI004^4-delta.smt2
regress1/ho/bound_var_bug.p
regress1/ho/fta0328.lfho.p
+ regress1/ho/ho-fun-sharing-dd.smt2
regress1/ho/issue3136-fconst-bool-bool.smt2
regress1/ho/issue4065-no-rep.smt2
regress1/ho/issue4092-sinf.smt2
@@ -2803,8 +2812,6 @@ set(regression_disabled_tests
###
regress1/bug472.smt2
regress1/datatypes/non-simple-rec-set.smt2
- # disabled temporarily until lazy lambda handling is merged
- regress1/ho/bug_freevar_PHI004^4-delta.smt2
# results in an assertion failure (see issue #1650).
regress1/ho/hoa0102.smt2
# after disallowing solving for terms with quantifiers
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback