diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-15 21:39:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-15 19:39:06 -0800 |
| commit | c83b4da35cea90527334b0d8e7ed343c4823436a (patch) | |
| tree | 7ea4cf4f032a508cf5e5299e99fe491ca1e6bafd | |
| parent | 569ec5f0ae1ed35e13cc6f581a2d292f7492387e (diff) | |
Disable regression (#3761)
Should fix recurring issue with nightlies.
Also fixes a warning.
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 7 |
2 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 02dded8b3..e15211847 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -968,7 +968,7 @@ void TheoryEngineModelBuilder::computeAssignableInfo( bool evaluable = false; // Set to true if a term in the current equivalence class has been given an // assignment exclusion set. - bool hasESet = false; + bool hasESet CVC4_UNUSED = false; // Set to true if we found that a term in the current equivalence class has // been given an assignment exclusion set, and we have not seen this term // as part of a previous assignment exclusion group. In other words, when diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ca50e2c83..42c145762 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1450,7 +1450,6 @@ set(regress_1_tests regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 regress1/quantifiers/mix-coeff.smt2 - regress1/quantifiers/model_6_1_bv.smt2 regress1/quantifiers/mutualrec2.cvc regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 regress1/quantifiers/nl-pow-trick.smt2 @@ -2291,9 +2290,11 @@ set(regression_disabled_tests regress1/nl/NAVIGATION2.smt2 # sat or unknown in different builds regress1/nl/issue3307.smt2 - # ajreynol: disabled these since they give different error messages on - # production and debug: + # ajreynol: different error messages on production and debug: regress1/quantifiers/macro-subtype-param.smt2 + # times out with competition build: + regress1/quantifiers/model_6_1_bv.smt2 + # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 ### |