From ea1a513414f0de19a45f58e5e43ccd9c3f290726 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 18:56:25 -0500 Subject: Enable some previously failing regressions (#7434) --- test/regress/CMakeLists.txt | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'test/regress/CMakeLists.txt') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cdd023a17..0d8123aa3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1653,6 +1653,7 @@ set(regress_1_tests regress1/fmf/issue6744-3-unc-bool-var.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 + regress1/fmf/ko-bound-set.cvc.smt2 regress1/fmf/loopy_coda.smt2 regress1/fmf/lst-no-self-rev-exp.smt2 regress1/fmf/memory_model-R_cpp-dd.cvc.smt2 @@ -1693,6 +1694,7 @@ set(regress_1_tests regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 + regress1/nl/approx-sqrt-unsat.smt2 regress1/nl/arctan2-expdef.smt2 regress1/nl/arrowsmith-050317.smt2 regress1/nl/bad-050217.smt2 @@ -1972,10 +1974,12 @@ set(regress_1_tests regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/qs-has-term.smt2 regress1/quantifiers/recfact.cvc.smt2 + regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 regress1/quantifiers/rew-to-0211-dd.smt2 regress1/quantifiers/ricart-agrawala6.smt2 regress1/quantifiers/set-choice-koikonomou.cvc.smt2 + regress1/quantifiers/set3.smt2 regress1/quantifiers/set8.smt2 regress1/quantifiers/seu169+1.smt2 regress1/quantifiers/seq-solved-enum.smt2 @@ -1986,6 +1990,7 @@ set(regress_1_tests regress1/quantifiers/smtlib46f14a.smt2 regress1/quantifiers/smtlibe99bbe.smt2 regress1/quantifiers/smtlibf957ea.smt2 + regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 @@ -2554,6 +2559,7 @@ set(regress_2_tests regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 regress2/quantifiers/cee-event-wrong-sat.smt2 + regress2/quantifiers/exp-trivially-dd3.smt2 regress2/quantifiers/gn-wrong-091018.smt2 regress2/quantifiers/issue3481-unsat1.smt2 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 @@ -2732,16 +2738,12 @@ set(regression_disabled_tests ### regress1/bug472.smt2 regress1/datatypes/non-simple-rec-set.smt2 - # TODO: fix models (projects #276) - regress1/fmf/ko-bound-set.cvc.smt2 # results in an assertion failure (see issue #1650). regress1/ho/hoa0102.smt2 # after disallowing solving for terms with quantifiers regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/SYO056^1.p - # slow on some builds after changes to tangent planes - regress1/nl/approx-sqrt-unsat.smt2 # times out after update to circuit propagator regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 # times out after update to tangent planes @@ -2758,12 +2760,6 @@ set(regression_disabled_tests regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build, ok with other builds: regress1/quantifiers/model_6_1_bv.smt2 - # timeout after changes to nonlinear on PR #5351 - regress1/quantifiers/rel-trigger-unusable.smt2 - # does not terminate/takes a long time when doing a coverage build with LFSC. - regress1/quantifiers/set3.smt2 - # changes to expand definitions, related to trigger selection for selectors - regress1/quantifiers/stream-x2014-09-18-unsat.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 @@ -2800,7 +2796,6 @@ set(regression_disabled_tests # previously sygus inference did not apply, now (correctly) times out regress1/sygus/issue3498.smt2 regress2/arith/miplib-opt1217--27.smt2 - regress2/quantifiers/exp-trivially-dd3.smt2 regress2/nl/dumortier-050317.smt2 # timeout on some builds after changes to justification heuristic regress2/nl/nt-lemmas-bad.smt2 -- cgit v1.2.3