diff options
Diffstat (limited to 'test/regress/CMakeLists.txt')
-rw-r--r-- | test/regress/CMakeLists.txt | 11 |
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 |