Disable regression (#3761)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 16 Feb 2020 03:39:06 +0000 (21:39 -0600)
committerGitHub <noreply@github.com>
Sun, 16 Feb 2020 03:39:06 +0000 (19:39 -0800)
Should fix recurring issue with nightlies.

Also fixes a warning.

src/theory/theory_model_builder.cpp
test/regress/CMakeLists.txt

index 02dded8b3f98da87a5bf502f73f16bedc84237bf..e15211847170d34c24c25a1683ae0a3186a706de 100644 (file)
@@ -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
index ca50e2c83431420a7fa8229dda7f9f69ec3be9f7..42c145762a7138a910949be9390c7cf53edc92ae 100644 (file)
@@ -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
   ###