Fix Travis for unit test compilation errors. (#1651)

make units does not fail if we have compile error for a unit test, however, make check does.
-Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings.

Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds.

diff --git a/.travis.yml b/.travis.yml
index e8c858d18aa2ac96b72baafd5decb2286488b4c2..94cee00ab529327f64057dcfadc07140a826810e 100644 (file)
--- a/.travis.yml
+++ b/.travis.yml
@@ -81,9 +81,7 @@ script:
        error "DISTCHECK (WITH NEWTHEORY TESTS) FAILED";
    }
    makeCheck() {
-     make V=1 -j2 units || error "BUILD/UNIT TEST FAILED";
-     make V=1 -j2 systemtests || error "BUILD/SYSTEM TEST FAILED";
-     make V=1 -j2 regress0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/REGRESSION TEST FAILED";
+     make V=1 -j2 check REGRESSION_LEVEL=0 CVC4_REGRESSION_ARGS='--no-early-exit' || error "BUILD/UNIT/SYSTEM/REGRESSION TEST FAILED"
    }
    makeExamples() {
      make V=1 -j2 examples || error "COULD NOT BUILD EXAMPLES${normal}";

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 2ef4f42bf6e6bf860195a4abac835288a42788e6..59a4d85907901b796230a0a9ee75b7c207a40e66 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -69,8 +69,9 @@ Theory::Theory(TheoryId id,
       d_careGraph(NULL),
       d_quantEngine(NULL),
       d_extTheory(NULL),
-      d_checkTime(getStatsPrefix(id) + "::checkTime"),
-      d_computeCareGraphTime(getStatsPrefix(id) + "::computeCareGraphTime"),
+      d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
+      d_computeCareGraphTime(getStatsPrefix(id) + name
+                             + "::computeCareGraphTime"),
       d_sharedTerms(satContext),
       d_out(&out),
       d_valuation(valuation),

diff --git a/test/regress/Makefile.levels b/test/regress/Makefile.levels
index ecfb0c2e59eb0739b56bde1650ff4a704363ce28..30bf4ca09e781493561311096c89b27ed7eb3c1d 100644 (file)
--- a/test/regress/Makefile.levels
+++ b/test/regress/Makefile.levels
@@ -1,5 +1,8 @@
 # This Makefile fragment allows one to use "make check" but also specify
 # a regression level.
+ifeq ($(REGRESSION_LEVEL),0)
+SUBDIRS = regress0
+endif
 ifeq ($(REGRESSION_LEVEL),1)
 SUBDIRS += regress1
 endif

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 167100ff018df946e28ba78bc14aa5125525383b..3d5f2702dec1554adbedcd1592b17ea2d4425f87 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -81,6 +81,7 @@ AM_CPPFLAGS = \
        $(TEST_CPPFLAGS)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(TEST_CXXFLAGS)
 AM_LDFLAGS = $(TEST_LDFLAGS) $(READLINE_LIBS) $(LIBS)
+CXXFLAGS=-Wno-suggest-override
 
 AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
 AM_CXXFLAGS_BLACK = -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index 633941b2b18dfe6a62d7e855462fe9ced2979a30..b70adc6885f221ac7b1223d07d8199bfcc3da47a 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -43,7 +43,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
@@ -60,7 +60,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
@@ -77,7 +77,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
@@ -94,7 +94,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -112,10 +112,10 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -125,10 +125,10 @@ public:
     info = LogicInfo("QF_AUFBV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -138,10 +138,10 @@ public:
     info = LogicInfo("QF_AUFLIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -155,10 +155,10 @@ public:
     info = LogicInfo("QF_AX");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -168,10 +168,10 @@ public:
     info = LogicInfo("QF_BV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -181,7 +181,7 @@ public:
     info = LogicInfo("QF_IDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -198,7 +198,7 @@ public:
     info = LogicInfo("QF_LIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -215,7 +215,7 @@ public:
     info = LogicInfo("QF_LRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -232,7 +232,7 @@ public:
     info = LogicInfo("QF_NIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -249,7 +249,7 @@ public:
     info = LogicInfo("QF_NRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -266,7 +266,7 @@ public:
     info = LogicInfo("QF_RDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isPure( THEORY_ARITH ) );
@@ -284,7 +284,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( !info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -297,7 +297,7 @@ public:
     info = LogicInfo("QF_UFBV");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -311,7 +311,7 @@ public:
     info = LogicInfo("QF_UFIDL");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -328,7 +328,7 @@ public:
     info = LogicInfo("QF_UFLIA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -345,7 +345,7 @@ public:
     info = LogicInfo("QF_UFLRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -361,7 +361,7 @@ public:
     info = LogicInfo("QF_UFNRA");
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -378,7 +378,7 @@ public:
     info = LogicInfo("UFLRA");
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -395,7 +395,7 @@ public:
     info = LogicInfo("UFNIA");
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.isSharingEnabled() );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isPure( THEORY_ARITH ) );
@@ -414,7 +414,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( !info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
@@ -432,7 +432,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
@@ -455,7 +455,7 @@ public:
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
@@ -463,7 +463,7 @@ public:
     TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAYS ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException );
@@ -480,7 +480,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) );
@@ -488,7 +488,7 @@ public:
     TS_ASSERT( ! info.isPure( THEORY_BOOL ) );
     TS_ASSERT( ! info.isPure( THEORY_UF ) );
     TS_ASSERT( ! info.isPure( THEORY_ARITH ) );
-    TS_ASSERT( ! info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( ! info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( ! info.isPure( THEORY_BV ) );
     TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) );
     TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) );
@@ -539,7 +539,7 @@ public:
     info.disableTheory(THEORY_SEP);
     info.lock();
     TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
-    TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+    TS_ASSERT( info.isPure( THEORY_ARRAYS ) );
     TS_ASSERT( ! info.isQuantified() );
 
     // check all-excluded logic
@@ -551,7 +551,7 @@ public:
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isPure( THEORY_BOOL ) );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
@@ -570,7 +570,7 @@ public:
     TS_ASSERT( !info.isSharingEnabled() );
     TS_ASSERT( !info.isQuantified() );
     TS_ASSERT( info.isPure( THEORY_BOOL ) );
-    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
@@ -590,7 +590,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
@@ -609,7 +609,7 @@ public:
     TS_ASSERT( !info.isPure( THEORY_BOOL ) );
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isQuantified() );
-    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+    TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAYS ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index d480bbb75ef781f1739b5a84cad2a841aa73b8ad..e931949fd2f6603f38ff76b6ea3d86b5ebe12b59 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -206,17 +206,17 @@ public:
     return RewriteResponse(REWRITE_DONE, n);
   }
 
-  std::string identify() const throw() {
+  std::string identify() const override {
     return "Fake" + d_id;
   }
 
-  void presolve() { Unimplemented(); }
+  void presolve() override { Unimplemented(); }
 
-  void preRegisterTerm(TNode) { Unimplemented(); }
+  void preRegisterTerm(TNode) override { Unimplemented(); }
   void registerTerm(TNode) { Unimplemented(); }
-  void check(Theory::Effort) { Unimplemented(); }
-  void propagate(Theory::Effort) { Unimplemented(); }
-  Node explain(TNode) { Unimplemented(); }
+  void check(Theory::Effort) override { Unimplemented(); }
+  void propagate(Theory::Effort) override { Unimplemented(); }
+  Node explain(TNode) override { Unimplemented(); }
   Node getValue(TNode n) { return Node::null(); }
 };/* class FakeTheory */
 
@@ -241,7 +241,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite {
 
 public:
 
-  void setUp() {
+  void setUp() override {
     d_em = new ExprManager();
     d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
@@ -263,11 +263,11 @@ public:
     d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
     d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF);
     d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH);
-    d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY);
+    d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAYS> >(THEORY_ARRAYS);
     d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV);
   }
 
-  void tearDown() {
+  void tearDown() override {
     delete d_nullChannel;
 
     delete d_scope;