From c83b4da35cea90527334b0d8e7ed343c4823436a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 15 Feb 2020 21:39:06 -0600 Subject: Disable regression (#3761) Should fix recurring issue with nightlies. Also fixes a warning. --- src/theory/theory_model_builder.cpp | 2 +- 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 ### -- cgit v1.2.3