From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 23 Aug 2018 23:28:21 +0000 (-0700)
Subject: Add missing overrides in unit tests (#2362)
X-Git-Tag: cvc5-1.0.0~4729
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=11a34205808098e503f145b2a779078dd509729e;p=cvc5.git

Add missing overrides in unit tests (#2362)
---

diff --git a/test/unit/base/map_util_black.h b/test/unit/base/map_util_black.h
index 6d2d2bbc7..39567d6ac 100644
--- a/test/unit/base/map_util_black.h
+++ b/test/unit/base/map_util_black.h
@@ -38,8 +38,8 @@ using std::string;
 class MapUtilBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp() {}
-  void tearDown() {}
+  void setUp() override {}
+  void tearDown() override {}
 
   // Returns a map containing {"key"->"value", "other"->"entry"}.
   static const std::map<string, string>& DefaultMap()
diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h
index 7545fa808..8a31f70ca 100644
--- a/test/unit/context/cdlist_black.h
+++ b/test/unit/context/cdlist_black.h
@@ -40,9 +40,9 @@ class CDListBlack : public CxxTest::TestSuite {
   Context* d_context;
 
  public:
-  void setUp() { d_context = new Context(); }
+  void setUp() override { d_context = new Context(); }
 
-  void tearDown() { delete d_context; }
+  void tearDown() override { delete d_context; }
 
   // test at different sizes.  this triggers grow() behavior differently.
   // grow() was completely broken in revision 256
diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 8cc1b73c2..2d2b3f409 100644
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -31,14 +31,15 @@ class CDMapBlack : public CxxTest::TestSuite {
   Context* d_context;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     d_context = new Context;
     // Debug.on("context");
     // Debug.on("gc");
     // Debug.on("pushpop");
   }
 
-  void tearDown() { delete d_context; }
+  void tearDown() override { delete d_context; }
 
   // Returns the elements in a CDHashMap.
   static std::map<int, int> GetElements(const CDHashMap<int, int>& map) {
diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h
index 232eb55a8..0f111cd61 100644
--- a/test/unit/context/cdmap_white.h
+++ b/test/unit/context/cdmap_white.h
@@ -27,17 +27,13 @@ class CDMapWhite : public CxxTest::TestSuite {
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testUnreachableSaveAndRestore() {
+  void testUnreachableSaveAndRestore()
+  {
     CDHashMap<int, int> map(d_context);
 
     TS_ASSERT_THROWS_NOTHING(map.makeCurrent());
diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h
index f5666173d..2838ae322 100644
--- a/test/unit/context/cdo_black.h
+++ b/test/unit/context/cdo_black.h
@@ -33,17 +33,13 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testIntCDO() {
+  void testIntCDO()
+  {
     // Test that push/pop maintains the original value
     CDO<int> a1(d_context);
     a1 = 5;
diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 63b60edc9..b4be4197c 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -36,12 +36,10 @@ struct MyContextNotifyObj : public ContextNotifyObj {
     ContextNotifyObj(context, pre),
     nCalls(0) {
   }
-  
-  virtual ~MyContextNotifyObj() {}
 
-  void contextNotifyPop() {
-    ++nCalls;
-  }
+  ~MyContextNotifyObj() override {}
+
+  void contextNotifyPop() override { ++nCalls; }
 };
 
 class MyContextObj : public ContextObj {
@@ -75,18 +73,15 @@ public:
     nSaves(0) {
   }
 
-  virtual ~MyContextObj() {
-    destroy();
-  }
+  ~MyContextObj() override { destroy(); }
 
-  ContextObj* save(ContextMemoryManager* pcmm) {
+  ContextObj* save(ContextMemoryManager* pcmm) override
+  {
     ++nSaves;
     return new(pcmm) MyContextObj(*this);
   }
 
-  void restore(ContextObj* contextObj) {
-    nCalls = notify.nCalls;
-  }
+  void restore(ContextObj* contextObj) override { nCalls = notify.nCalls; }
 
   void makeCurrent() {
     ContextObj::makeCurrent();
@@ -99,17 +94,13 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testContextPushPop() {
+  void testContextPushPop()
+  {
     // Test what happens when the context is popped below 0
     // the interface doesn't declare any exceptions
     d_context->push();
diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h
index ed64b5eac..beace137e 100644
--- a/test/unit/context/context_mm_black.h
+++ b/test/unit/context/context_mm_black.h
@@ -33,13 +33,11 @@ private:
 
   ContextMemoryManager* d_cmm;
 
-public:
+ public:
+  void setUp() override { d_cmm = new ContextMemoryManager(); }
 
-  void setUp() {
-    d_cmm = new ContextMemoryManager();
-  }
-
-  void testPushPop() {
+  void testPushPop()
+  {
 #ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 #warning "Using the debug context memory manager, omitting unit tests"
 #else
@@ -96,7 +94,5 @@ public:
 #endif /* __CVC4__CONTEXT__CONTEXT_MM_H */
   }
 
-  void tearDown() {
-    delete d_cmm;
-  }
+  void tearDown() override { delete d_cmm; }
 };
diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h
index 64e6e184b..2c1ef8e71 100644
--- a/test/unit/context/context_white.h
+++ b/test/unit/context/context_white.h
@@ -29,18 +29,14 @@ private:
 
   Context* d_context;
 
-public:
+ public:
+  void setUp() override { d_context = new Context; }
 
-  void setUp() {
-    d_context = new Context;
-  }
-
-  void tearDown() {
-    delete d_context;
-  }
+  void tearDown() override { delete d_context; }
 
-  void testContextSimple() {
-    Scope *s = d_context->getTopScope();
+  void testContextSimple()
+  {
+    Scope* s = d_context->getTopScope();
 
     TS_ASSERT(s == d_context->getBottomScope());
     TS_ASSERT(d_context->getLevel() == 0);
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index afc99ef32..58defe07d 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -42,16 +42,17 @@ private:
   SmtEngine* d_smtEngine;
   SmtScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_exprManager = new ExprManager();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
     d_smtEngine = new SmtEngine(d_exprManager);
     d_scope = new SmtScope(d_smtEngine);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smtEngine;
     delete d_exprManager;
diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index a169855e2..847cbf929 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -61,9 +61,9 @@ class AttributeWhite : public CxxTest::TestSuite {
   TypeNode* d_booleanType;
   SmtEngine* d_smtEngine;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smtEngine = new SmtEngine(d_em);
@@ -71,7 +71,8 @@ public:
     d_booleanType = new TypeNode(d_nm->booleanType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_booleanType;
     delete d_scope;
     delete d_smtEngine;
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index a131aa140..9c604aa52 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -61,19 +61,19 @@ private:
     return vars;
   }
 
+ public:
+  void setUp() override { d_exprManager = new ExprManager; }
 
-public:
-  void setUp() {
-    d_exprManager = new ExprManager;
-  }
-
-
-  void tearDown() {
-    try {
+  void tearDown() override
+  {
+    try
+    {
       delete d_exprManager;
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during tearDown():" << endl << e;
-      throw ;
+      throw;
     }
   }
 
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 4354c5b6a..d8774db82 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -50,12 +50,12 @@ private:
   Expr* r1;
   Expr* r2;
 
-public:
-
-  void setUp() {
-    try {
-
-      char *argv[2];
+ public:
+  void setUp() override
+  {
+    try
+    {
+      char* argv[2];
       argv[0] = strdup("");
       argv[1] = strdup("--output-language=ast");
       Options::parseOptions(&opts, 2, argv);
@@ -64,12 +64,13 @@ public:
 
       d_em = new ExprManager(opts);
 
-      a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
+      a_bool = new Expr(d_em->mkVar("a", d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
       c_bool_and = new Expr(d_em->mkExpr(AND, *a_bool, *b_bool));
       and_op = new Expr(d_em->mkConst(AND));
       plus_op = new Expr(d_em->mkConst(PLUS));
-      fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
+      fun_type = new Type(
+          d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
       fun_op = new Expr(d_em->mkVar("f", *fun_type));
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
       null = new Expr();
@@ -78,13 +79,16 @@ public:
       i2 = new Expr(d_em->mkConst(Rational(23)));
       r1 = new Expr(d_em->mkConst(Rational(1, 5)));
       r2 = new Expr(d_em->mkConst(Rational("0")));
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during setUp():" << endl << e;
       throw;
     }
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     try {
       delete r2;
       delete r1;
diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h
index 5ac503b0e..900f5dac6 100644
--- a/test/unit/expr/kind_black.h
+++ b/test/unit/expr/kind_black.h
@@ -34,13 +34,15 @@ class KindBlack : public CxxTest::TestSuite {
   //easier to define in setup
   int beyond;
   Kind unknown;
-public:
-  void setUp() {
+
+ public:
+  void setUp() override
+  {
     undefined = UNDEFINED_KIND;
     null = NULL_EXPR;
     last = LAST_KIND;
-    beyond = ((int) LAST_KIND) + 1;
-    unknown = (Kind) beyond;
+    beyond = ((int)LAST_KIND) + 1;
+    unknown = (Kind)beyond;
   }
 
   
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index fb468c896..461d59498 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -56,7 +56,8 @@ class NodeBlack : public CxxTest::TestSuite {
   TypeNode* d_realType;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-language=ast");
@@ -70,7 +71,8 @@ class NodeBlack : public CxxTest::TestSuite {
     d_realType = new TypeNode(d_nodeManager->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_realType;
     delete d_booleanType;
     delete d_scope;
diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h
index b8e9d92f6..f4fbbb5d9 100644
--- a/test/unit/expr/node_builder_black.h
+++ b/test/unit/expr/node_builder_black.h
@@ -40,9 +40,9 @@ private:
   TypeNode* d_integerType;
   TypeNode* d_realType;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
 
@@ -52,7 +52,8 @@ public:
     d_realType = new TypeNode(d_nm->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_integerType;
     delete d_booleanType;
     delete d_realType;
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 68c94c176..5da55916b 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -34,14 +34,15 @@ class NodeManagerBlack : public CxxTest::TestSuite {
   NodeManager* d_nodeManager;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nodeManager = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nodeManager;
   }
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index e2b8cbf1c..016ea7793 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -30,14 +30,15 @@ class NodeManagerWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nm;
   }
diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h
index bab7e2b0c..cfc4a6b7a 100644
--- a/test/unit/expr/node_self_iterator_black.h
+++ b/test/unit/expr/node_self_iterator_black.h
@@ -33,16 +33,17 @@ private:
   TypeNode* d_booleanType;
   TypeNode* d_realType;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nodeManager = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nodeManager);
     d_booleanType = new TypeNode(d_nodeManager->booleanType());
     d_realType = new TypeNode(d_nodeManager->realType());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_booleanType;
     delete d_scope;
     delete d_nodeManager;
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index d2d6a265d..09d015e42 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -34,14 +34,15 @@ class NodeWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_nm = new NodeManager(NULL);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_nm;
   }
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 33b5d73c9..2f6f88c27 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -37,18 +37,22 @@ private:
 
   ExprManager* d_exprManager;
 
-public:
-
-  void setUp() {
-    try {
+ public:
+  void setUp() override
+  {
+    try
+    {
       d_exprManager = new ExprManager;
-    } catch(Exception e) {
+    }
+    catch (Exception e)
+    {
       cerr << "Exception during setUp():" << endl << e;
       throw;
     }
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     try {
       delete d_exprManager;
     } catch(Exception e) {
diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index ff05df5da..51cb6a881 100644
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -32,20 +32,20 @@ using namespace std;
 class TypeCardinalityPublic : public CxxTest::TestSuite {
   ExprManager* d_em;
 
-public:
-
-  void setUp() {
-    d_em = new ExprManager();
-  }
-
-  void tearDown() {
-    delete d_em;
-  }
-
-  void testTheBasics() {
-    TS_ASSERT( d_em->booleanType().getCardinality().compare(2) == Cardinality::EQUAL );
-    TS_ASSERT( d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL );
-    TS_ASSERT( d_em->realType().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL );
+ public:
+  void setUp() override { d_em = new ExprManager(); }
+
+  void tearDown() override { delete d_em; }
+
+  void testTheBasics()
+  {
+    TS_ASSERT(d_em->booleanType().getCardinality().compare(2)
+              == Cardinality::EQUAL);
+    TS_ASSERT(
+        d_em->integerType().getCardinality().compare(Cardinality::INTEGERS)
+        == Cardinality::EQUAL);
+    TS_ASSERT(d_em->realType().getCardinality().compare(Cardinality::REALS)
+              == Cardinality::EQUAL);
   }
 
   void testArrays() {
diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 45a48ea99..32b5ca7cb 100644
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -37,16 +37,17 @@ class TypeNodeWhite : public CxxTest::TestSuite {
   NodeManagerScope* d_scope;
   SmtEngine* d_smt;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = d_em->getNodeManager();
     d_smt = new SmtEngine(d_em);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 44b3660c9..cf76bb05a 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -35,7 +35,7 @@ using namespace std;
 class InteractiveShellBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp()
+  void setUp() override
   {
     d_sin = new stringstream;
     d_sout = new stringstream;
@@ -45,7 +45,8 @@ class InteractiveShellBlack : public CxxTest::TestSuite
     d_solver.reset(new api::Solver(&d_options));
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_sin;
     delete d_sout;
   }
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index e7548708e..58ed12a60 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -217,13 +217,9 @@ class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
   void testGoodCvc4Inputs() {
     tryGoodInput(""); // empty string is OK
@@ -307,13 +303,9 @@ class Smt1ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt1ParserTest() : ParserBlack(LANG_SMTLIB_V1) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
   void testGoodSmt1Inputs() {
     tryGoodInput(""); // empty string is OK
@@ -376,15 +368,12 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack {
 public:
   Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
 
-  void setUp() {
-    super::setUp();
-  }
+  void setUp() override { super::setUp(); }
 
-  void tearDown() {
-    super::tearDown();
-  }
+  void tearDown() override { super::tearDown(); }
 
-  virtual void setupContext(Parser& parser) {
+  void setupContext(Parser& parser) override
+  {
     if(dynamic_cast<Smt2*>(&parser) != NULL){
       dynamic_cast<Smt2*>(&parser)->addTheory(Smt2::THEORY_CORE);
     }
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 45baf177f..d83d2681b 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -38,9 +38,9 @@ using namespace std;
 class ParserBuilderBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp() { d_solver.reset(new api::Solver()); }
+  void setUp() override { d_solver.reset(new api::Solver()); }
 
-  void tearDown() {}
+  void tearDown() override {}
 
   void testEmptyFileInput()
   {
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 7d7ee1a3a..f238ba8be 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -177,7 +177,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
  public:
   TheoryBVGaussWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
@@ -251,7 +251,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
     d_z_mul_nine = d_nm->mkNode(kind::BITVECTOR_MULT, d_z, d_nine);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     (void)d_scope;
     d_p = Node::null();
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index be69a7a1d..7e04bb7c5 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -49,31 +49,34 @@ class FakeSatSolver : public SatSolver {
  public:
   FakeSatSolver() : d_nextVar(0), d_addClauseCalled(false) {}
 
-  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) {
+  SatVariable newVar(bool theoryAtom, bool preRegister, bool canErase) override
+  {
     return d_nextVar++;
   }
 
-  SatVariable trueVar() { return d_nextVar++; }
+  SatVariable trueVar() override { return d_nextVar++; }
 
-  SatVariable falseVar() { return d_nextVar++; }
+  SatVariable falseVar() override { return d_nextVar++; }
 
-  ClauseId addClause(SatClause& c, bool lemma) {
+  ClauseId addClause(SatClause& c, bool lemma) override
+  {
     d_addClauseCalled = true;
     return ClauseIdUndef;
   }
 
-  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) {
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+  {
     d_addClauseCalled = true;
     return ClauseIdUndef;
   }
 
-  bool nativeXor() { return false; }
+  bool nativeXor() override { return false; }
 
   void reset() { d_addClauseCalled = false; }
 
   unsigned int addClauseCalled() { return d_addClauseCalled; }
 
-  unsigned getAssertionLevel() const { return 0; }
+  unsigned getAssertionLevel() const override { return 0; }
 
   bool isDecision(Node) const { return false; }
 
@@ -83,19 +86,22 @@ class FakeSatSolver : public SatSolver {
 
   bool spendResource() { return false; }
 
-  void interrupt() {}
+  void interrupt() override {}
 
-  SatValue solve() { return SAT_VALUE_UNKNOWN; }
+  SatValue solve() override { return SAT_VALUE_UNKNOWN; }
 
-  SatValue solve(long unsigned int& resource) { return SAT_VALUE_UNKNOWN; }
+  SatValue solve(long unsigned int& resource) override
+  {
+    return SAT_VALUE_UNKNOWN;
+  }
 
-  SatValue value(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
+  SatValue value(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
 
-  SatValue modelValue(SatLiteral l) { return SAT_VALUE_UNKNOWN; }
+  SatValue modelValue(SatLiteral l) override { return SAT_VALUE_UNKNOWN; }
 
   bool properExplanation(SatLiteral lit, SatLiteral expl) const { return true; }
 
-  bool ok() const { return true; }
+  bool ok() const override { return true; }
 
 }; /* class FakeSatSolver */
 
@@ -122,7 +128,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   SmtScope* d_scope;
   SmtEngine* d_smt;
 
-  void setUp() {
+  void setUp() override
+  {
     d_exprManager = new ExprManager();
     d_smt = new SmtEngine(d_exprManager);
     d_smt->d_logic.lock();
@@ -138,7 +145,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
         d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels());
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_cnfStream;
     delete d_cnfContext;
     delete d_cnfRegistrar;
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 4416ee00a..10cb15f6f 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -43,7 +43,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
  public:
   TheoryEvaluatorWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
@@ -53,7 +53,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     delete d_scope;
     delete d_smt;
diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 2cb1243d5..7661c08b5 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -97,7 +97,8 @@ public:
     }
   }
 
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
@@ -125,7 +126,8 @@ public:
 
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_intType;
     delete d_realType;
     delete d_booleanType;
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 487c6a434..569d7e30b 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -44,9 +44,9 @@ private:
   NodeManager* d_nm;
   SmtScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
@@ -54,7 +54,8 @@ public:
     d_nm = NodeManager::fromExprManager(d_em);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index c830e7813..bc5b36a0b 100644
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -52,14 +52,16 @@ public:
 
   TheoryBVWhite() {}
 
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_smt;
     delete d_em;
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index 4c96f6cb9..018744bd1 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -38,8 +38,8 @@ using namespace CVC4::smt;
 class BvInstantiatorWhite : public CxxTest::TestSuite
 {
  public:
-  void setUp();
-  void tearDown();
+  void setUp() override;
+  void tearDown() override;
 
   void testGetPvCoeff();
   void testNormalizePvMult();
diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h
index fc073b5a4..67dc20541 100644
--- a/test/unit/theory/theory_strings_rewriter_white.h
+++ b/test/unit/theory/theory_strings_rewriter_white.h
@@ -39,7 +39,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
  public:
   TheoryStringsRewriterWhite() {}
 
-  void setUp()
+  void setUp() override
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
@@ -49,7 +49,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite
     d_scope = new SmtScope(d_smt);
   }
 
-  void tearDown()
+  void tearDown() override
   {
     delete d_scope;
     delete d_smt;
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 0fbf9c1d6..c8265a755 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -122,20 +122,19 @@ public:
     return done();
   }
 
-  void check(Effort e) {
+  void check(Effort e) override
+  {
     while(!done()) {
       getWrapper();
     }
   }
 
-  void presolve() {
-    Unimplemented();
-  }
-  void preRegisterTerm(TNode n) {}
-  void propagate(Effort level) {}
-  Node explain(TNode n) { return Node::null(); }
+  void presolve() override { Unimplemented(); }
+  void preRegisterTerm(TNode n) override {}
+  void propagate(Effort level) override {}
+  Node explain(TNode n) override { return Node::null(); }
   Node getValue(TNode n) { return Node::null(); }
-  string identify() const { return "DummyTheory"; }
+  string identify() const override { return "DummyTheory"; }
 };/* class DummyTheory */
 
 class TheoryBlack : public CxxTest::TestSuite {
@@ -155,9 +154,9 @@ class TheoryBlack : public CxxTest::TestSuite {
   Node atom0;
   Node atom1;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
@@ -173,14 +172,15 @@ public:
     d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL;
     d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL;
 
-    d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL),
-                              *d_logicInfo);
+    d_dummy = new DummyTheory(
+        d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo);
     d_outputChannel.clear();
     atom0 = d_nm->mkConst(true);
     atom1 = d_nm->mkConst(false);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     atom1 = Node::null();
     atom0 = Node::null();
     delete d_dummy;
diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index 03b1a2a95..b68941843 100644
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -38,15 +38,16 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
   NodeManager* d_nm;
   NodeManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_scope = new NodeManagerScope(d_nm);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 49a0b995a..c668e8c8f 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -30,12 +30,14 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
   ExprManagerScope* d_scope;
 
  public:
-  void setUp() {
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_scope = new ExprManagerScope(*d_em);
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }
diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h
index 904b78b4b..ce7e854d8 100644
--- a/test/unit/util/binary_heap_black.h
+++ b/test/unit/util/binary_heap_black.h
@@ -25,20 +25,18 @@ using namespace CVC4;
 using namespace std;
 
 class BinaryHeapBlack : public CxxTest::TestSuite {
-public:
+ public:
+  void setUp() override {}
 
-  void setUp() {
-  }
-
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   /**
    * Test a a series of simple heaps (push a few then pop all then do others).
    * Done as a series to test if the heap structure falls into a bad state
    * after prolonged use.
    */
-  void testHeapSeries() {
+  void testHeapSeries()
+  {
     BinaryHeap<int> heap;
 
     // First test a heap of 1 element
diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 04fdc4044..c75368196 100644
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -26,7 +26,7 @@ class BitVectorBlack : public CxxTest::TestSuite {
 
 
 public:
- void setUp()
+ void setUp() override
  {
    zero = BitVector(4);
    one = zero.setBit(0);
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index 7e69e4efe..c2086c415 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -31,16 +31,17 @@ class DatatypeBlack : public CxxTest::TestSuite {
   ExprManager* d_em;
   ExprManagerScope* d_scope;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     d_em = new ExprManager();
     d_scope = new ExprManagerScope(*d_em);
     Debug.on("datatypes");
     Debug.on("groundterms");
   }
 
-  void tearDown() {
+  void tearDown() override
+  {
     delete d_scope;
     delete d_em;
   }
diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h
index 0eb4b0040..ba17d28da 100644
--- a/test/unit/util/exception_black.h
+++ b/test/unit/util/exception_black.h
@@ -25,16 +25,14 @@ using namespace CVC4;
 using namespace std;
 
 class ExceptionBlack : public CxxTest::TestSuite {
-public:
+ public:
+  void setUp() override {}
 
-  void setUp() {
-  }
-
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   // CVC4::Exception is a simple class, just test it all at once.
-  void testExceptions() {
+  void testExceptions()
+  {
     Exception e1;
     Exception e2(string("foo!"));
     Exception e3("bar!");
diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h
index 014970b77..7296de060 100644
--- a/test/unit/util/listener_black.h
+++ b/test/unit/util/listener_black.h
@@ -30,9 +30,9 @@ class ListenerBlack : public CxxTest::TestSuite {
    public:
     EventListener(std::multiset<std::string>& events, std::string name)
         : d_events(events), d_name(name) {}
-    ~EventListener(){}
+    ~EventListener() override {}
 
-    virtual void notify() { d_events.insert(d_name); }
+    void notify() override { d_events.insert(d_name); }
 
    private:
     std::multiset<std::string>& d_events;
@@ -45,13 +45,9 @@ public:
     return std::multiset<std::string>(arr, arr + len);
   }
 
-  void setUp() {
-    d_events.clear();
-  }
+  void setUp() override { d_events.clear(); }
 
-  void tearDown() {
-    d_events.clear();
-  }
+  void tearDown() override { d_events.clear(); }
 
   void testEmptyCollection() {
     // Makes an new collection and tests that it is empty.
diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index c8833ced5..cea30f360 100644
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -33,9 +33,9 @@ class OutputBlack : public CxxTest::TestSuite {
   stringstream d_messageStream;
   stringstream d_warningStream;
 
-public:
-
-  void setUp() {
+ public:
+  void setUp() override
+  {
     DebugChannel.setStream(&d_debugStream);
     TraceChannel.setStream(&d_traceStream);
     NoticeChannel.setStream(&d_noticeStream);
@@ -51,8 +51,7 @@ public:
     d_warningStream.str("");
   }
 
-  void tearDown() {
-  }
+  void tearDown() override {}
 
   void testOutput() {
     Debug.on("foo");