google test: Use ASSERT_* instead of EXPECT_*. (#5765)
authorAina Niemetz <aina.niemetz@gmail.com>
Tue, 12 Jan 2021 16:55:56 +0000 (08:55 -0800)
committerGitHub <noreply@github.com>
Tue, 12 Jan 2021 16:55:56 +0000 (08:55 -0800)
Use ASSERT instead of EXPECT for consistency. There's no real benefit
for us to use EXPECT -- the main difference is that within a test,
EXPECT failures do not terminate the test, while ASSERT failures do.

This further fixes a minor issue in theory_sets_type_rules_white.h
(which is still not migrated to google test yet).

16 files changed:
test/unit/api/datatype_api_black.cpp
test/unit/api/op_black.cpp
test/unit/api/result_black.cpp
test/unit/api/solver_black.cpp
test/unit/api/sort_black.cpp
test/unit/api/term_black.cpp
test/unit/base/map_util_black.cpp
test/unit/context/cdlist_black.cpp
test/unit/context/cdo_black.cpp
test/unit/context/context_black.cpp
test/unit/context/context_white.cpp
test/unit/expr/attribute_black.cpp
test/unit/expr/attribute_white.cpp
test/unit/expr/kind_black.cpp
test/unit/expr/node_algorithm_black.cpp
test/unit/theory/theory_sets_type_rules_white.h

index fad525655fd7756d8cdb80c0dc7abc51383965e6..85831697149f26e20e8eb6615ef0b566f3d1bd06 100644 (file)
@@ -38,7 +38,7 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSort)
   Datatype d = listSort.getDatatype();
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
-  EXPECT_THROW(d[2], CVC4ApiException);
+  ASSERT_THROW(d[2], CVC4ApiException);
   ASSERT_NO_THROW(consConstr.getConstructorTerm());
   ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
@@ -88,24 +88,24 @@ TEST_F(TestApiDatatypeBlack, mkDatatypeSorts)
   for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
   {
     ASSERT_TRUE(dtsorts[i].isDatatype());
-    EXPECT_FALSE(dtsorts[i].getDatatype().isFinite());
-    EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
+    ASSERT_FALSE(dtsorts[i].getDatatype().isFinite());
+    ASSERT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
   }
   // verify the resolution was correct
   Datatype dtTree = dtsorts[0].getDatatype();
   DatatypeConstructor dtcTreeNode = dtTree[0];
-  EXPECT_EQ(dtcTreeNode.getName(), "node");
+  ASSERT_EQ(dtcTreeNode.getName(), "node");
   DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
-  EXPECT_EQ(dtsTreeNodeLeft.getName(), "left");
+  ASSERT_EQ(dtsTreeNodeLeft.getName(), "left");
   // argument type should have resolved to be recursive
-  EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
-  EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
+  ASSERT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
+  ASSERT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
 
   // fails due to empty datatype
   std::vector<DatatypeDecl> dtdeclsBad;
   DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
   dtdeclsBad.push_back(emptyD);
-  EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
+  ASSERT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
 }
 
 TEST_F(TestApiDatatypeBlack, datatypeStructs)
@@ -119,21 +119,21 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs)
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
-  EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
+  ASSERT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  EXPECT_FALSE(dt.isCodatatype());
-  EXPECT_FALSE(dt.isTuple());
-  EXPECT_FALSE(dt.isRecord());
-  EXPECT_FALSE(dt.isFinite());
-  EXPECT_TRUE(dt.isWellFounded());
+  ASSERT_FALSE(dt.isCodatatype());
+  ASSERT_FALSE(dt.isTuple());
+  ASSERT_FALSE(dt.isRecord());
+  ASSERT_FALSE(dt.isFinite());
+  ASSERT_TRUE(dt.isWellFounded());
   // get constructor
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
-  EXPECT_EQ(dcons.getNumSelectors(), 2);
+  ASSERT_EQ(dcons.getNumSelectors(), 2);
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
@@ -145,8 +145,8 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs)
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
-  EXPECT_FALSE(dtEnum.isTuple());
-  EXPECT_TRUE(dtEnum.isFinite());
+  ASSERT_FALSE(dtEnum.isTuple());
+  ASSERT_TRUE(dtEnum.isFinite());
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
@@ -157,29 +157,29 @@ TEST_F(TestApiDatatypeBlack, datatypeStructs)
   dtypeSpecStream.addConstructor(consStream);
   Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
   Datatype dtStream = dtypeSortStream.getDatatype();
-  EXPECT_TRUE(dtStream.isCodatatype());
-  EXPECT_FALSE(dtStream.isFinite());
+  ASSERT_TRUE(dtStream.isCodatatype());
+  ASSERT_FALSE(dtStream.isFinite());
   // codatatypes may be well-founded
-  EXPECT_TRUE(dtStream.isWellFounded());
+  ASSERT_TRUE(dtStream.isWellFounded());
 
   // create tuple
   Sort tupSort = d_solver.mkTupleSort({boolSort});
   Datatype dtTuple = tupSort.getDatatype();
-  EXPECT_TRUE(dtTuple.isTuple());
-  EXPECT_FALSE(dtTuple.isRecord());
-  EXPECT_TRUE(dtTuple.isFinite());
-  EXPECT_TRUE(dtTuple.isWellFounded());
+  ASSERT_TRUE(dtTuple.isTuple());
+  ASSERT_FALSE(dtTuple.isRecord());
+  ASSERT_TRUE(dtTuple.isFinite());
+  ASSERT_TRUE(dtTuple.isWellFounded());
 
   // create record
   std::vector<std::pair<std::string, Sort>> fields = {
       std::make_pair("b", boolSort), std::make_pair("i", intSort)};
   Sort recSort = d_solver.mkRecordSort(fields);
-  EXPECT_TRUE(recSort.isDatatype());
+  ASSERT_TRUE(recSort.isDatatype());
   Datatype dtRecord = recSort.getDatatype();
-  EXPECT_FALSE(dtRecord.isTuple());
-  EXPECT_TRUE(dtRecord.isRecord());
-  EXPECT_FALSE(dtRecord.isFinite());
-  EXPECT_TRUE(dtRecord.isWellFounded());
+  ASSERT_FALSE(dtRecord.isTuple());
+  ASSERT_TRUE(dtRecord.isRecord());
+  ASSERT_FALSE(dtRecord.isFinite());
+  ASSERT_TRUE(dtRecord.isWellFounded());
 }
 
 TEST_F(TestApiDatatypeBlack, datatypeNames)
@@ -189,7 +189,7 @@ TEST_F(TestApiDatatypeBlack, datatypeNames)
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   ASSERT_NO_THROW(dtypeSpec.getName());
-  EXPECT_EQ(dtypeSpec.getName(), std::string("list"));
+  ASSERT_EQ(dtypeSpec.getName(), std::string("list"));
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
@@ -198,22 +198,22 @@ TEST_F(TestApiDatatypeBlack, datatypeNames)
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  EXPECT_EQ(dt.getName(), std::string("list"));
+  ASSERT_EQ(dt.getName(), std::string("list"));
   ASSERT_NO_THROW(dt.getConstructor("nil"));
   ASSERT_NO_THROW(dt["cons"]);
   ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
   ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
 
   DatatypeConstructor dcons = dt[0];
-  EXPECT_EQ(dcons.getName(), std::string("cons"));
+  ASSERT_EQ(dcons.getName(), std::string("cons"));
   ASSERT_NO_THROW(dcons.getSelector("head"));
   ASSERT_NO_THROW(dcons["tail"]);
   ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
-  EXPECT_EQ(dselTail.getName(), std::string("tail"));
-  EXPECT_EQ(dselTail.getRangeSort(), dtypeSort);
+  ASSERT_EQ(dselTail.getName(), std::string("tail"));
+  ASSERT_EQ(dselTail.getRangeSort(), dtypeSort);
 
   // possible to construct null datatype declarations if not using solver
   ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
@@ -236,7 +236,7 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype)
 
   Sort pairType = d_solver.mkDatatypeSort(pairSpec);
 
-  EXPECT_TRUE(pairType.getDatatype().isParametric());
+  ASSERT_TRUE(pairType.getDatatype().isParametric());
 
   v.clear();
   v.push_back(d_solver.getIntegerSort());
@@ -255,46 +255,46 @@ TEST_F(TestApiDatatypeBlack, parametricDatatype)
   v.push_back(d_solver.getRealSort());
   Sort pairIntReal = pairType.instantiate(v);
 
-  EXPECT_NE(pairIntInt, pairRealReal);
-  EXPECT_NE(pairIntReal, pairRealReal);
-  EXPECT_NE(pairRealInt, pairRealReal);
-  EXPECT_NE(pairIntInt, pairIntReal);
-  EXPECT_NE(pairIntInt, pairRealInt);
-  EXPECT_NE(pairIntReal, pairRealInt);
-
-  EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal));
-  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal));
-  EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal));
-  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal));
-  EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt));
-  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt));
-  EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt));
-  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt));
-  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal));
-  EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal));
-  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal));
-  EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal));
-  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt));
-  EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt));
-  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt));
-  EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt));
-
-  EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
-  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
-  EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
-  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
-  EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
-  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
-  EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
-  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
-  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
-  EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
-  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
-  EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
-  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
-  EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
-  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
-  EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
+  ASSERT_NE(pairIntInt, pairRealReal);
+  ASSERT_NE(pairIntReal, pairRealReal);
+  ASSERT_NE(pairRealInt, pairRealReal);
+  ASSERT_NE(pairIntInt, pairIntReal);
+  ASSERT_NE(pairIntInt, pairRealInt);
+  ASSERT_NE(pairIntReal, pairRealInt);
+
+  ASSERT_TRUE(pairRealReal.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealReal));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairRealInt));
+  ASSERT_TRUE(pairRealInt.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairRealInt));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntReal));
+  ASSERT_TRUE(pairIntReal.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairIntInt.isComparableTo(pairIntReal));
+  ASSERT_FALSE(pairRealReal.isComparableTo(pairIntInt));
+  ASSERT_FALSE(pairIntReal.isComparableTo(pairIntInt));
+  ASSERT_FALSE(pairRealInt.isComparableTo(pairIntInt));
+  ASSERT_TRUE(pairIntInt.isComparableTo(pairIntInt));
+
+  ASSERT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
+  ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
+  ASSERT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
+  ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
+  ASSERT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
+  ASSERT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
+  ASSERT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
+  ASSERT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
+  ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
+  ASSERT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
+  ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
+  ASSERT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
+  ASSERT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
+  ASSERT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
+  ASSERT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
+  ASSERT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
 TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
@@ -346,12 +346,12 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   std::vector<Sort> dtsorts;
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 3);
-  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded());
-  EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
-  EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
-  EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[2].getDatatype().isWellFounded());
+  ASSERT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -378,10 +378,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 1);
   ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
-  EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
+  ASSERT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
             dtsorts[0]);
-  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -416,10 +416,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   // both are well-founded and have nested recursion
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 2);
-  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
-  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -454,10 +454,10 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   // both are well-founded and have nested recursion
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 2);
-  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
-  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -492,8 +492,8 @@ TEST_F(TestApiDatatypeBlack, datatypeSimplyRec)
   // well-founded and has nested recursion
   ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
   ASSERT_EQ(dtsorts.size(), 1);
-  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
-  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  ASSERT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
 TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
@@ -542,9 +542,9 @@ TEST_F(TestApiDatatypeBlack, datatypeSpecializedCons)
   Term testConsTerm;
   // get the specialized constructor term for list[Int]
   ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
-  EXPECT_NE(testConsTerm, nilc.getConstructorTerm());
+  ASSERT_NE(testConsTerm, nilc.getConstructorTerm());
   // error to get the specialized constructor term for Int
-  EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
+  ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
 }  // namespace test
 }  // namespace CVC4
index ca64a322fc0890582f37eb2f834d5d74d602c091..817662d67353fb67a95d2545ac91cded21abb4e0 100644 (file)
@@ -46,7 +46,7 @@ TEST_F(TestApiOpBlack, opFromKind)
   ASSERT_THROW(plus.getIndices<uint32_t>(), CVC4ApiException);
 
   ASSERT_NO_THROW(d_solver.mkOp(PLUS));
-  EXPECT_EQ(plus, d_solver.mkOp(PLUS));
+  ASSERT_EQ(plus, d_solver.mkOp(PLUS));
   ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
 }
 
@@ -58,11 +58,11 @@ TEST_F(TestApiOpBlack, getIndicesString)
   Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
   ASSERT_TRUE(divisible_ot.isIndexed());
   std::string divisible_idx = divisible_ot.getIndices<std::string>();
-  EXPECT_EQ(divisible_idx, "4");
+  ASSERT_EQ(divisible_idx, "4");
 
   Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
   std::string record_update_idx = record_update_ot.getIndices<std::string>();
-  EXPECT_EQ(record_update_idx, "test");
+  ASSERT_EQ(record_update_idx, "test");
   ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
 }
 
@@ -71,7 +71,7 @@ TEST_F(TestApiOpBlack, getIndicesUint)
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   ASSERT_TRUE(bitvector_repeat_ot.isIndexed());
   uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
-  EXPECT_EQ(bitvector_repeat_idx, 5);
+  ASSERT_EQ(bitvector_repeat_idx, 5);
   ASSERT_THROW(
       (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
       CVC4ApiException);
@@ -79,40 +79,40 @@ TEST_F(TestApiOpBlack, getIndicesUint)
   Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
   uint32_t bitvector_zero_extend_idx =
       bitvector_zero_extend_ot.getIndices<uint32_t>();
-  EXPECT_EQ(bitvector_zero_extend_idx, 6);
+  ASSERT_EQ(bitvector_zero_extend_idx, 6);
 
   Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
   uint32_t bitvector_sign_extend_idx =
       bitvector_sign_extend_ot.getIndices<uint32_t>();
-  EXPECT_EQ(bitvector_sign_extend_idx, 7);
+  ASSERT_EQ(bitvector_sign_extend_idx, 7);
 
   Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
   uint32_t bitvector_rotate_left_idx =
       bitvector_rotate_left_ot.getIndices<uint32_t>();
-  EXPECT_EQ(bitvector_rotate_left_idx, 8);
+  ASSERT_EQ(bitvector_rotate_left_idx, 8);
 
   Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
   uint32_t bitvector_rotate_right_idx =
       bitvector_rotate_right_ot.getIndices<uint32_t>();
-  EXPECT_EQ(bitvector_rotate_right_idx, 9);
+  ASSERT_EQ(bitvector_rotate_right_idx, 9);
 
   Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
   uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
-  EXPECT_EQ(int_to_bitvector_idx, 10);
+  ASSERT_EQ(int_to_bitvector_idx, 10);
 
   Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
   uint32_t floatingpoint_to_ubv_idx =
       floatingpoint_to_ubv_ot.getIndices<uint32_t>();
-  EXPECT_EQ(floatingpoint_to_ubv_idx, 11);
+  ASSERT_EQ(floatingpoint_to_ubv_idx, 11);
 
   Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
   uint32_t floatingpoint_to_sbv_idx =
       floatingpoint_to_sbv_ot.getIndices<uint32_t>();
-  EXPECT_EQ(floatingpoint_to_sbv_idx, 13);
+  ASSERT_EQ(floatingpoint_to_sbv_idx, 13);
 
   Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
   uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
-  EXPECT_EQ(tuple_update_idx, 5);
+  ASSERT_EQ(tuple_update_idx, 5);
   ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
 }
 
@@ -180,7 +180,7 @@ TEST_F(TestApiOpBlack, opScopingToString)
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
   std::string op_repr = bitvector_repeat_ot.toString();
   Solver solver2;
-  EXPECT_EQ(bitvector_repeat_ot.toString(), op_repr);
+  ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr);
 }
 }  // namespace test
 }  // namespace CVC4
index bb60ab7ac10c0279978b811f45689f3c47884456..52cb68b253a45368dbb6ae2ba829aa8219b142df 100644 (file)
@@ -50,8 +50,8 @@ TEST_F(TestApiResultBlack, eq)
   CVC4::api::Result res2 = d_solver.checkSat();
   CVC4::api::Result res3 = d_solver.checkSat();
   res = res2;
-  EXPECT_EQ(res, res2);
-  EXPECT_EQ(res3, res2);
+  ASSERT_EQ(res, res2);
+  ASSERT_EQ(res3, res2);
 }
 
 TEST_F(TestApiResultBlack, isSat)
@@ -115,7 +115,7 @@ TEST_F(TestApiResultBlack, isEntailmentUnknown)
   CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
   ASSERT_FALSE(res.isEntailed());
   ASSERT_TRUE(res.isEntailmentUnknown());
-  EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
+  ASSERT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
 }
 }  // namespace test
 }  // namespace CVC4
index e7610265ecf989c9a8353eeac6f2570ce381a9db..5592c7d3dfe7f898ff353b9bf900d8b2813f66ae 100644 (file)
@@ -343,11 +343,11 @@ TEST_F(TestApiSolverBlack, mkBitVector)
   ASSERT_THROW(d_solver.mkBitVector("20", 2), CVC4ApiException);
   ASSERT_THROW(d_solver.mkBitVector(8, "101010101", 2), CVC4ApiException);
   ASSERT_THROW(d_solver.mkBitVector(8, "-256", 10), CVC4ApiException);
-  EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
-  EXPECT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
-  EXPECT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
-  EXPECT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
-  EXPECT_EQ(d_solver.mkBitVector(8, "-1", 10),
+  ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("10", 10));
+  ASSERT_EQ(d_solver.mkBitVector("1010", 2), d_solver.mkBitVector("a", 16));
+  ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
+  ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
+  ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10),
             d_solver.mkBitVector(8, "FF", 16));
 }
 
@@ -672,9 +672,9 @@ TEST_F(TestApiSolverBlack, mkString)
 {
   ASSERT_NO_THROW(d_solver.mkString(""));
   ASSERT_NO_THROW(d_solver.mkString("asdfasdf"));
-  EXPECT_EQ(d_solver.mkString("asdf\\nasdf").toString(),
+  ASSERT_EQ(d_solver.mkString("asdf\\nasdf").toString(),
             "\"asdf\\u{5c}nasdf\"");
-  EXPECT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
+  ASSERT_EQ(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(),
             "\"asdf\\u{5c}nasdf\"");
 }
 
@@ -685,7 +685,7 @@ TEST_F(TestApiSolverBlack, mkChar)
   ASSERT_THROW(d_solver.mkChar(""), CVC4ApiException);
   ASSERT_THROW(d_solver.mkChar("0g0"), CVC4ApiException);
   ASSERT_THROW(d_solver.mkChar("100000"), CVC4ApiException);
-  EXPECT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
+  ASSERT_EQ(d_solver.mkChar("abc"), d_solver.mkChar("ABC"));
 }
 
 TEST_F(TestApiSolverBlack, mkTerm)
@@ -1237,8 +1237,8 @@ TEST_F(TestApiSolverBlack, uFIteration)
   uint32_t idx = 0;
   for (auto c : fxy)
   {
-    EXPECT_LT(idx, 3);
-    EXPECT_EQ(c, expected_children[idx]);
+    ASSERT_LT(idx, 3);
+    ASSERT_EQ(c, expected_children[idx]);
     idx++;
   }
 }
@@ -1264,7 +1264,7 @@ TEST_F(TestApiSolverBlack, getOp)
   ASSERT_FALSE(a.hasOp());
   ASSERT_THROW(a.getOp(), CVC4ApiException);
   ASSERT_TRUE(exta.hasOp());
-  EXPECT_EQ(exta.getOp(), ext);
+  ASSERT_EQ(exta.getOp(), ext);
 
   // Test Datatypes -- more complicated
   DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
@@ -1287,13 +1287,13 @@ TEST_F(TestApiSolverBlack, getOp)
   Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
 
   ASSERT_TRUE(listnil.hasOp());
-  EXPECT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(listnil.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
 
   ASSERT_TRUE(listcons1.hasOp());
-  EXPECT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(listcons1.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
 
   ASSERT_TRUE(listhead.hasOp());
-  EXPECT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 
 TEST_F(TestApiSolverBlack, getOption)
@@ -1784,12 +1784,12 @@ TEST_F(TestApiSolverBlack, simplify)
   ASSERT_NO_THROW(d_solver.simplify(b));
   Term x_eq_x = d_solver.mkTerm(EQUAL, x, x);
   ASSERT_NO_THROW(d_solver.simplify(x_eq_x));
-  EXPECT_NE(d_solver.mkTrue(), x_eq_x);
-  EXPECT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
+  ASSERT_NE(d_solver.mkTrue(), x_eq_x);
+  ASSERT_EQ(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
   Term x_eq_b = d_solver.mkTerm(EQUAL, x, b);
   ASSERT_NO_THROW(d_solver.simplify(x_eq_b));
-  EXPECT_NE(d_solver.mkTrue(), x_eq_b);
-  EXPECT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
+  ASSERT_NE(d_solver.mkTrue(), x_eq_b);
+  ASSERT_NE(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
   Solver slv;
   ASSERT_THROW(slv.simplify(x), CVC4ApiException);
 
@@ -1797,12 +1797,12 @@ TEST_F(TestApiSolverBlack, simplify)
   ASSERT_NO_THROW(d_solver.simplify(i1));
   Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23"));
   ASSERT_NO_THROW(d_solver.simplify(i2));
-  EXPECT_NE(i1, i2);
-  EXPECT_NE(i1, d_solver.simplify(i2));
+  ASSERT_NE(i1, i2);
+  ASSERT_NE(i1, d_solver.simplify(i2));
   Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
   ASSERT_NO_THROW(d_solver.simplify(i3));
-  EXPECT_NE(i1, i3);
-  EXPECT_EQ(i1, d_solver.simplify(i3));
+  ASSERT_NE(i1, i3);
+  ASSERT_EQ(i1, d_solver.simplify(i3));
 
   Datatype consList = consListSort.getDatatype();
   Term dt1 = d_solver.mkTerm(
index ea87441fe954c33d9f0ae1b54fe08e9181707663..16190b76d5a18bd772cdf0cbc03f8cba351220be 100644 (file)
@@ -56,7 +56,7 @@ TEST_F(TestApiSortBlack, datatypeSorts)
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  EXPECT_FALSE(dtypeSort.isConstructor());
+  ASSERT_FALSE(dtypeSort.isConstructor());
   ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC4ApiException);
   ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC4ApiException);
   ASSERT_THROW(dtypeSort.getConstructorArity(), CVC4ApiException);
@@ -65,30 +65,30 @@ TEST_F(TestApiSortBlack, datatypeSorts)
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
   Sort consSort = consTerm.getSort();
-  EXPECT_TRUE(consSort.isConstructor());
-  EXPECT_FALSE(consSort.isTester());
-  EXPECT_FALSE(consSort.isSelector());
-  EXPECT_EQ(consSort.getConstructorArity(), 2);
+  ASSERT_TRUE(consSort.isConstructor());
+  ASSERT_FALSE(consSort.isTester());
+  ASSERT_FALSE(consSort.isSelector());
+  ASSERT_EQ(consSort.getConstructorArity(), 2);
   std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts();
-  EXPECT_EQ(consDomSorts[0], intSort);
-  EXPECT_EQ(consDomSorts[1], dtypeSort);
-  EXPECT_EQ(consSort.getConstructorCodomainSort(), dtypeSort);
+  ASSERT_EQ(consDomSorts[0], intSort);
+  ASSERT_EQ(consDomSorts[1], dtypeSort);
+  ASSERT_EQ(consSort.getConstructorCodomainSort(), dtypeSort);
 
   // get tester
   Term isConsTerm = dcons.getTesterTerm();
-  EXPECT_TRUE(isConsTerm.getSort().isTester());
-  EXPECT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort);
+  ASSERT_TRUE(isConsTerm.getSort().isTester());
+  ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort);
   Sort booleanSort = d_solver.getBooleanSort();
-  EXPECT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort);
+  ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort);
   ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC4ApiException);
   ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC4ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
   Term tailTerm = dselTail.getSelectorTerm();
-  EXPECT_TRUE(tailTerm.getSort().isSelector());
-  EXPECT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort);
-  EXPECT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort);
+  ASSERT_TRUE(tailTerm.getSort().isSelector());
+  ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort);
+  ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort);
   ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC4ApiException);
   ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException);
 }
@@ -170,7 +170,7 @@ TEST_F(TestApiSortBlack, getSetElementSort)
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
   ASSERT_NO_THROW(setSort.getSetElementSort());
   Sort elementSort = setSort.getSetElementSort();
-  EXPECT_EQ(elementSort, d_solver.getIntegerSort());
+  ASSERT_EQ(elementSort, d_solver.getIntegerSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException);
 }
@@ -180,7 +180,7 @@ TEST_F(TestApiSortBlack, getBagElementSort)
   Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
   ASSERT_NO_THROW(bagSort.getBagElementSort());
   Sort elementSort = bagSort.getBagElementSort();
-  EXPECT_EQ(elementSort, d_solver.getIntegerSort());
+  ASSERT_EQ(elementSort, d_solver.getIntegerSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException);
 }
@@ -188,10 +188,10 @@ TEST_F(TestApiSortBlack, getBagElementSort)
 TEST_F(TestApiSortBlack, getSequenceElementSort)
 {
   Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
-  EXPECT_TRUE(seqSort.isSequence());
+  ASSERT_TRUE(seqSort.isSequence());
   ASSERT_NO_THROW(seqSort.getSequenceElementSort());
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  EXPECT_FALSE(bvSort.isSequence());
+  ASSERT_FALSE(bvSort.isSequence());
   ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException);
 }
 
@@ -206,7 +206,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortName)
 TEST_F(TestApiSortBlack, isUninterpretedSortParameterized)
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
-  EXPECT_FALSE(uSort.isUninterpretedSortParameterized());
+  ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
   Sort sSort = d_solver.mkSortConstructorSort("s", 1);
   Sort siSort = sSort.instantiate({uSort});
   ASSERT_TRUE(siSort.isUninterpretedSortParameterized());
@@ -220,7 +220,7 @@ TEST_F(TestApiSortBlack, getUninterpretedSortParamSorts)
   ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
   Sort siSort = sSort.instantiate({uSort, uSort});
-  EXPECT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
+  ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
   Sort bvSort = d_solver.mkBitVectorSort(32);
   ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException);
 }
@@ -345,24 +345,24 @@ TEST_F(TestApiSortBlack, sortSubtyping)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort realSort = d_solver.getRealSort();
-  EXPECT_TRUE(intSort.isSubsortOf(realSort));
-  EXPECT_FALSE(realSort.isSubsortOf(intSort));
-  EXPECT_TRUE(intSort.isComparableTo(realSort));
-  EXPECT_TRUE(realSort.isComparableTo(intSort));
+  ASSERT_TRUE(intSort.isSubsortOf(realSort));
+  ASSERT_FALSE(realSort.isSubsortOf(intSort));
+  ASSERT_TRUE(intSort.isComparableTo(realSort));
+  ASSERT_TRUE(realSort.isComparableTo(intSort));
 
   Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
   Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
-  EXPECT_FALSE(arraySortII.isComparableTo(intSort));
+  ASSERT_FALSE(arraySortII.isComparableTo(intSort));
   // we do not support subtyping for arrays
-  EXPECT_FALSE(arraySortII.isComparableTo(arraySortIR));
+  ASSERT_FALSE(arraySortII.isComparableTo(arraySortIR));
 
   Sort setSortI = d_solver.mkSetSort(intSort);
   Sort setSortR = d_solver.mkSetSort(realSort);
   // we don't support subtyping for sets
-  EXPECT_FALSE(setSortI.isComparableTo(setSortR));
-  EXPECT_FALSE(setSortI.isSubsortOf(setSortR));
-  EXPECT_FALSE(setSortR.isComparableTo(setSortI));
-  EXPECT_FALSE(setSortR.isSubsortOf(setSortI));
+  ASSERT_FALSE(setSortI.isComparableTo(setSortR));
+  ASSERT_FALSE(setSortI.isSubsortOf(setSortR));
+  ASSERT_FALSE(setSortR.isComparableTo(setSortI));
+  ASSERT_FALSE(setSortR.isSubsortOf(setSortI));
 }
 
 TEST_F(TestApiSortBlack, sortScopedToString)
@@ -370,11 +370,11 @@ TEST_F(TestApiSortBlack, sortScopedToString)
   std::string name = "uninterp-sort";
   Sort bvsort8 = d_solver.mkBitVectorSort(8);
   Sort uninterp_sort = d_solver.mkUninterpretedSort(name);
-  EXPECT_EQ(bvsort8.toString(), "(_ BitVec 8)");
-  EXPECT_EQ(uninterp_sort.toString(), name);
+  ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)");
+  ASSERT_EQ(uninterp_sort.toString(), name);
   Solver solver2;
-  EXPECT_EQ(bvsort8.toString(), "(_ BitVec 8)");
-  EXPECT_EQ(uninterp_sort.toString(), name);
+  ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)");
+  ASSERT_EQ(uninterp_sort.toString(), name);
 }
 
 }  // namespace test
index 6b032ebd6849ba3bfed3b802d7f6d213724f147f..50d67688da1a384e76303d15a4a4a0554ccdf533 100644 (file)
@@ -46,10 +46,10 @@ TEST_F(TestApiTermBlack, getId)
   Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
   ASSERT_NO_THROW(x.getId());
   Term y = x;
-  EXPECT_EQ(x.getId(), y.getId());
+  ASSERT_EQ(x.getId(), y.getId());
 
   Term z = d_solver.mkVar(d_solver.getIntegerSort(), "z");
-  EXPECT_NE(x.getId(), z.getId());
+  ASSERT_NE(x.getId(), z.getId());
 }
 
 TEST_F(TestApiTermBlack, getKind)
@@ -91,7 +91,7 @@ TEST_F(TestApiTermBlack, getKind)
   Sort seqSort = d_solver.mkSequenceSort(intSort);
   Term s = d_solver.mkConst(seqSort, "s");
   Term ss = d_solver.mkTerm(SEQ_CONCAT, s, s);
-  EXPECT_EQ(ss.getKind(), SEQ_CONCAT);
+  ASSERT_EQ(ss.getKind(), SEQ_CONCAT);
 }
 
 TEST_F(TestApiTermBlack, getSort)
@@ -106,37 +106,37 @@ TEST_F(TestApiTermBlack, getSort)
   ASSERT_THROW(n.getSort(), CVC4ApiException);
   Term x = d_solver.mkVar(bvSort, "x");
   ASSERT_NO_THROW(x.getSort());
-  EXPECT_EQ(x.getSort(), bvSort);
+  ASSERT_EQ(x.getSort(), bvSort);
   Term y = d_solver.mkVar(bvSort, "y");
   ASSERT_NO_THROW(y.getSort());
-  EXPECT_EQ(y.getSort(), bvSort);
+  ASSERT_EQ(y.getSort(), bvSort);
 
   Term f = d_solver.mkVar(funSort1, "f");
   ASSERT_NO_THROW(f.getSort());
-  EXPECT_EQ(f.getSort(), funSort1);
+  ASSERT_EQ(f.getSort(), funSort1);
   Term p = d_solver.mkVar(funSort2, "p");
   ASSERT_NO_THROW(p.getSort());
-  EXPECT_EQ(p.getSort(), funSort2);
+  ASSERT_EQ(p.getSort(), funSort2);
 
   Term zero = d_solver.mkInteger(0);
   ASSERT_NO_THROW(zero.getSort());
-  EXPECT_EQ(zero.getSort(), intSort);
+  ASSERT_EQ(zero.getSort(), intSort);
 
   Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
   ASSERT_NO_THROW(f_x.getSort());
-  EXPECT_EQ(f_x.getSort(), intSort);
+  ASSERT_EQ(f_x.getSort(), intSort);
   Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
   ASSERT_NO_THROW(f_y.getSort());
-  EXPECT_EQ(f_y.getSort(), intSort);
+  ASSERT_EQ(f_y.getSort(), intSort);
   Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
   ASSERT_NO_THROW(sum.getSort());
-  EXPECT_EQ(sum.getSort(), intSort);
+  ASSERT_EQ(sum.getSort(), intSort);
   Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
   ASSERT_NO_THROW(p_0.getSort());
-  EXPECT_EQ(p_0.getSort(), boolSort);
+  ASSERT_EQ(p_0.getSort(), boolSort);
   Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
   ASSERT_NO_THROW(p_f_y.getSort());
-  EXPECT_EQ(p_f_y.getSort(), boolSort);
+  ASSERT_EQ(p_f_y.getSort(), boolSort);
 }
 
 TEST_F(TestApiTermBlack, getOp)
@@ -158,13 +158,13 @@ TEST_F(TestApiTermBlack, getOp)
   Term extb = d_solver.mkTerm(ext, b);
 
   ASSERT_TRUE(ab.hasOp());
-  EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
   ASSERT_FALSE(ab.getOp().isIndexed());
   // can compare directly to a Kind (will invoke Op constructor)
-  EXPECT_EQ(ab.getOp(), Op(&d_solver, SELECT));
+  ASSERT_EQ(ab.getOp(), Op(&d_solver, SELECT));
   ASSERT_TRUE(extb.hasOp());
   ASSERT_TRUE(extb.getOp().isIndexed());
-  EXPECT_EQ(extb.getOp(), ext);
+  ASSERT_EQ(extb.getOp(), ext);
 
   Term f = d_solver.mkConst(funsort, "f");
   Term fx = d_solver.mkTerm(APPLY_UF, f, x);
@@ -172,10 +172,10 @@ TEST_F(TestApiTermBlack, getOp)
   ASSERT_FALSE(f.hasOp());
   ASSERT_THROW(f.getOp(), CVC4ApiException);
   ASSERT_TRUE(fx.hasOp());
-  EXPECT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
+  ASSERT_EQ(fx.getOp(), Op(&d_solver, APPLY_UF));
   std::vector<Term> children(fx.begin(), fx.end());
   // testing rebuild from op and children
-  EXPECT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
+  ASSERT_EQ(fx, d_solver.mkTerm(fx.getOp(), children));
 
   // Test Datatypes Ops
   Sort sort = d_solver.mkParamSort("T");
@@ -208,15 +208,15 @@ TEST_F(TestApiTermBlack, getOp)
   ASSERT_TRUE(headTerm.hasOp());
   ASSERT_TRUE(tailTerm.hasOp());
 
-  EXPECT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  EXPECT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
-  EXPECT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
-  EXPECT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  ASSERT_EQ(nilTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(consTerm.getOp(), Op(&d_solver, APPLY_CONSTRUCTOR));
+  ASSERT_EQ(headTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
+  ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
 
   // Test rebuilding
   children.clear();
   children.insert(children.begin(), headTerm.begin(), headTerm.end());
-  EXPECT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
+  ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children));
 }
 
 TEST_F(TestApiTermBlack, isNull)
@@ -635,7 +635,7 @@ TEST_F(TestApiTermBlack, termAssignment)
   Term t1 = d_solver.mkInteger(1);
   Term t2 = t1;
   t2 = d_solver.mkInteger(2);
-  EXPECT_EQ(t1, d_solver.mkInteger(1));
+  ASSERT_EQ(t1, d_solver.mkInteger(1));
 }
 
 TEST_F(TestApiTermBlack, termCompare)
@@ -654,8 +654,8 @@ TEST_F(TestApiTermBlack, termChildren)
   // simple term 2+3
   Term two = d_solver.mkInteger(2);
   Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
-  EXPECT_EQ(t1[0], two);
-  EXPECT_EQ(t1.getNumChildren(), 2);
+  ASSERT_EQ(t1[0], two);
+  ASSERT_EQ(t1.getNumChildren(), 2);
   Term tnull;
   ASSERT_THROW(tnull.getNumChildren(), CVC4ApiException);
 
@@ -666,8 +666,8 @@ TEST_F(TestApiTermBlack, termChildren)
   Term t2 = d_solver.mkTerm(APPLY_UF, f, two);
   // due to our higher-order view of terms, we treat f as a child of APPLY_UF
   ASSERT_EQ(t2.getNumChildren(), 2);
-  EXPECT_EQ(t2[0], f);
-  EXPECT_EQ(t2[1], two);
+  ASSERT_EQ(t2[0], f);
+  ASSERT_EQ(t2[1], two);
   ASSERT_THROW(tnull[0], CVC4ApiException);
 }
 
@@ -685,64 +685,64 @@ TEST_F(TestApiTermBlack, getInteger)
   Term int10 = d_solver.mkInteger("18446744073709551615");
   Term int11 = d_solver.mkInteger("18446744073709551616");
 
-  EXPECT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
+  ASSERT_TRUE(!int1.isInt32() && !int1.isUInt32() && !int1.isInt64()
               && !int1.isUInt64() && int1.isInteger());
-  EXPECT_EQ(int1.getInteger(), "-18446744073709551616");
-  EXPECT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
+  ASSERT_EQ(int1.getInteger(), "-18446744073709551616");
+  ASSERT_TRUE(!int2.isInt32() && !int2.isUInt32() && !int2.isInt64()
               && !int2.isUInt64() && int2.isInteger());
-  EXPECT_EQ(int2.getInteger(), "-18446744073709551615");
-  EXPECT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
+  ASSERT_EQ(int2.getInteger(), "-18446744073709551615");
+  ASSERT_TRUE(!int3.isInt32() && !int3.isUInt32() && int3.isInt64()
               && !int3.isUInt64() && int3.isInteger());
-  EXPECT_EQ(int3.getInt64(), -4294967296);
-  EXPECT_EQ(int3.getInteger(), "-4294967296");
-  EXPECT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
+  ASSERT_EQ(int3.getInt64(), -4294967296);
+  ASSERT_EQ(int3.getInteger(), "-4294967296");
+  ASSERT_TRUE(!int4.isInt32() && !int4.isUInt32() && int4.isInt64()
               && !int4.isUInt64() && int4.isInteger());
-  EXPECT_EQ(int4.getInt64(), -4294967295);
-  EXPECT_EQ(int4.getInteger(), "-4294967295");
-  EXPECT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
+  ASSERT_EQ(int4.getInt64(), -4294967295);
+  ASSERT_EQ(int4.getInteger(), "-4294967295");
+  ASSERT_TRUE(int5.isInt32() && !int5.isUInt32() && int5.isInt64()
               && !int5.isUInt64() && int5.isInteger());
-  EXPECT_EQ(int5.getInt32(), -10);
-  EXPECT_EQ(int5.getInt64(), -10);
-  EXPECT_EQ(int5.getInteger(), "-10");
-  EXPECT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
+  ASSERT_EQ(int5.getInt32(), -10);
+  ASSERT_EQ(int5.getInt64(), -10);
+  ASSERT_EQ(int5.getInteger(), "-10");
+  ASSERT_TRUE(int6.isInt32() && int6.isUInt32() && int6.isInt64()
               && int6.isUInt64() && int6.isInteger());
-  EXPECT_EQ(int6.getInt32(), 0);
-  EXPECT_EQ(int6.getUInt32(), 0);
-  EXPECT_EQ(int6.getInt64(), 0);
-  EXPECT_EQ(int6.getUInt64(), 0);
-  EXPECT_EQ(int6.getInteger(), "0");
-  EXPECT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
+  ASSERT_EQ(int6.getInt32(), 0);
+  ASSERT_EQ(int6.getUInt32(), 0);
+  ASSERT_EQ(int6.getInt64(), 0);
+  ASSERT_EQ(int6.getUInt64(), 0);
+  ASSERT_EQ(int6.getInteger(), "0");
+  ASSERT_TRUE(int7.isInt32() && int7.isUInt32() && int7.isInt64()
               && int7.isUInt64() && int7.isInteger());
-  EXPECT_EQ(int7.getInt32(), 10);
-  EXPECT_EQ(int7.getUInt32(), 10);
-  EXPECT_EQ(int7.getInt64(), 10);
-  EXPECT_EQ(int7.getUInt64(), 10);
-  EXPECT_EQ(int7.getInteger(), "10");
-  EXPECT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
+  ASSERT_EQ(int7.getInt32(), 10);
+  ASSERT_EQ(int7.getUInt32(), 10);
+  ASSERT_EQ(int7.getInt64(), 10);
+  ASSERT_EQ(int7.getUInt64(), 10);
+  ASSERT_EQ(int7.getInteger(), "10");
+  ASSERT_TRUE(!int8.isInt32() && int8.isUInt32() && int8.isInt64()
               && int8.isUInt64() && int8.isInteger());
-  EXPECT_EQ(int8.getUInt32(), 4294967295);
-  EXPECT_EQ(int8.getInt64(), 4294967295);
-  EXPECT_EQ(int8.getUInt64(), 4294967295);
-  EXPECT_EQ(int8.getInteger(), "4294967295");
-  EXPECT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
+  ASSERT_EQ(int8.getUInt32(), 4294967295);
+  ASSERT_EQ(int8.getInt64(), 4294967295);
+  ASSERT_EQ(int8.getUInt64(), 4294967295);
+  ASSERT_EQ(int8.getInteger(), "4294967295");
+  ASSERT_TRUE(!int9.isInt32() && !int9.isUInt32() && int9.isInt64()
               && int9.isUInt64() && int9.isInteger());
-  EXPECT_EQ(int9.getInt64(), 4294967296);
-  EXPECT_EQ(int9.getUInt64(), 4294967296);
-  EXPECT_EQ(int9.getInteger(), "4294967296");
-  EXPECT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
+  ASSERT_EQ(int9.getInt64(), 4294967296);
+  ASSERT_EQ(int9.getUInt64(), 4294967296);
+  ASSERT_EQ(int9.getInteger(), "4294967296");
+  ASSERT_TRUE(!int10.isInt32() && !int10.isUInt32() && !int10.isInt64()
               && int10.isUInt64() && int10.isInteger());
-  EXPECT_EQ(int10.getUInt64(), 18446744073709551615ull);
-  EXPECT_EQ(int10.getInteger(), "18446744073709551615");
-  EXPECT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
+  ASSERT_EQ(int10.getUInt64(), 18446744073709551615ull);
+  ASSERT_EQ(int10.getInteger(), "18446744073709551615");
+  ASSERT_TRUE(!int11.isInt32() && !int11.isUInt32() && !int11.isInt64()
               && !int11.isUInt64() && int11.isInteger());
-  EXPECT_EQ(int11.getInteger(), "18446744073709551616");
+  ASSERT_EQ(int11.getInteger(), "18446744073709551616");
 }
 
 TEST_F(TestApiTermBlack, getString)
 {
   Term s1 = d_solver.mkString("abcde");
-  EXPECT_TRUE(s1.isString());
-  EXPECT_EQ(s1.getString(), L"abcde");
+  ASSERT_TRUE(s1.isString());
+  ASSERT_EQ(s1.getString(), L"abcde");
 }
 
 TEST_F(TestApiTermBlack, substitute)
@@ -753,8 +753,8 @@ TEST_F(TestApiTermBlack, substitute)
   Term xpx = d_solver.mkTerm(PLUS, x, x);
   Term onepone = d_solver.mkTerm(PLUS, one, one);
 
-  EXPECT_EQ(xpx.substitute(x, one), onepone);
-  EXPECT_EQ(onepone.substitute(one, x), xpx);
+  ASSERT_EQ(xpx.substitute(x, one), onepone);
+  ASSERT_EQ(onepone.substitute(one, x), xpx);
   // incorrect due to type
   ASSERT_THROW(xpx.substitute(one, ttrue), CVC4ApiException);
 
@@ -768,7 +768,7 @@ TEST_F(TestApiTermBlack, substitute)
   rs.push_back(y);
   es.push_back(y);
   rs.push_back(one);
-  EXPECT_EQ(xpy.substitute(es, rs), xpone);
+  ASSERT_EQ(xpy.substitute(es, rs), xpone);
 
   // incorrect substitution due to arity
   rs.pop_back();
@@ -804,8 +804,8 @@ TEST_F(TestApiTermBlack, constArray)
   Term one = d_solver.mkInteger(1);
   Term constarr = d_solver.mkConstArray(arrsort, one);
 
-  EXPECT_EQ(constarr.getKind(), CONST_ARRAY);
-  EXPECT_EQ(constarr.getConstArrayBase(), one);
+  ASSERT_EQ(constarr.getKind(), CONST_ARRAY);
+  ASSERT_EQ(constarr.getConstArrayBase(), one);
   ASSERT_THROW(a.getConstArrayBase(), CVC4ApiException);
 
   arrsort =
@@ -825,7 +825,7 @@ TEST_F(TestApiTermBlack, constSequenceElements)
   Sort seqsort = d_solver.mkSequenceSort(realsort);
   Term s = d_solver.mkEmptySequence(seqsort);
 
-  EXPECT_EQ(s.getKind(), CONST_SEQUENCE);
+  ASSERT_EQ(s.getKind(), CONST_SEQUENCE);
   // empty sequence has zero elements
   std::vector<Term> cs = s.getConstSequenceElements();
   ASSERT_TRUE(cs.empty());
@@ -840,9 +840,9 @@ TEST_F(TestApiTermBlack, termScopedToString)
 {
   Sort intsort = d_solver.getIntegerSort();
   Term x = d_solver.mkConst(intsort, "x");
-  EXPECT_EQ(x.toString(), "x");
+  ASSERT_EQ(x.toString(), "x");
   Solver solver2;
-  EXPECT_EQ(x.toString(), "x");
+  ASSERT_EQ(x.toString(), "x");
 }
 }  // namespace test
 }  // namespace CVC4
index c8c98818f75073d5395f758c1966f28ac9474c66..6c0a2e3b5405d38547269ca9ab068704bef7e40f 100644 (file)
@@ -66,13 +66,13 @@ TEST_F(TestMapBlack, map)
   ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
   ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
 
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
   if (std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
     *found_value = "new value";
   }
-  EXPECT_EQ(FindOrDie(map, "other"), "new value");
+  ASSERT_EQ(FindOrDie(map, "other"), "new value");
 }
 
 TEST_F(TestMapBlack, constant_map)
@@ -83,10 +83,10 @@ TEST_F(TestMapBlack, constant_map)
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
   ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key.");
 }
 
@@ -97,13 +97,13 @@ TEST_F(TestMapBlack, unordered_map)
   ASSERT_TRUE(CVC4::ContainsKey(map, "key"));
   ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
 
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
   if (std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
     *found_value = "new value";
   }
-  EXPECT_EQ(FindOrDie(map, "other"), "new value");
+  ASSERT_EQ(FindOrDie(map, "other"), "new value");
 }
 
 TEST_F(TestMapBlack, const_unordered_map)
@@ -115,10 +115,10 @@ TEST_F(TestMapBlack, const_unordered_map)
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
   ASSERT_DEATH(FindOrDie(map, "asdf"), "The map does not contain the key.");
 }
 
@@ -155,10 +155,10 @@ TEST_F(TestMapBlack, CDHashMap)
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
 }
 
 TEST_F(TestMapBlack, const_CDHashMap)
@@ -173,10 +173,10 @@ TEST_F(TestMapBlack, const_CDHashMap)
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
 }
 
 TEST_F(TestMapBlack, CDInsertHashMap)
@@ -190,10 +190,10 @@ TEST_F(TestMapBlack, CDInsertHashMap)
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
 }
 
 TEST_F(TestMapBlack, const_CDInsertHashMap)
@@ -207,10 +207,10 @@ TEST_F(TestMapBlack, const_CDInsertHashMap)
   ASSERT_FALSE(CVC4::ContainsKey(map, "non key"));
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
-    EXPECT_EQ(*found_value, "entry");
+    ASSERT_EQ(*found_value, "entry");
   }
-  EXPECT_EQ(FindOrNull(map, "non key"), nullptr);
-  EXPECT_EQ(FindOrDie(map, "other"), "entry");
+  ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
+  ASSERT_EQ(FindOrDie(map, "other"), "entry");
 }
 }  // namespace test
 }  // namespace CVC4
index 71da10d0cb17833057d76e8e5497d3c9b578cb8d..47db6c758b3179d7951d5b1f50a3529cd7e1f643 100644 (file)
@@ -53,22 +53,22 @@ class TestContextCDListBlack : public TestContext
     ASSERT_TRUE(list.empty());
     for (int32_t i = 0; i < n; ++i)
     {
-      EXPECT_EQ(list.size(), (uint32_t)i);
+      ASSERT_EQ(list.size(), (uint32_t)i);
       list.push_back(i);
       ASSERT_FALSE(list.empty());
-      EXPECT_EQ(list.back(), i);
+      ASSERT_EQ(list.back(), i);
       int32_t i2 = 0;
       for (CDList<int32_t>::const_iterator j = list.begin(); j != list.end();
            ++j)
       {
-        EXPECT_EQ(*j, i2++);
+        ASSERT_EQ(*j, i2++);
       }
     }
-    EXPECT_EQ(list.size(), (uint32_t)n);
+    ASSERT_EQ(list.size(), (uint32_t)n);
 
     for (int32_t i = 0; i < n; ++i)
     {
-      EXPECT_EQ(list[i], i);
+      ASSERT_EQ(list[i], i);
     }
   }
 };
@@ -114,25 +114,25 @@ TEST_F(TestContextCDListBlack, destructor_called)
   listF.push_back(shouldAlsoRemainFalseDSO);
   listF.push_back(aThirdFalseDSO);
 
-  EXPECT_EQ(shouldRemainFalse, false);
-  EXPECT_EQ(shouldFlipToTrue, false);
-  EXPECT_EQ(alsoFlipToTrue, false);
-  EXPECT_EQ(shouldAlsoRemainFalse, false);
-  EXPECT_EQ(aThirdFalse, false);
+  ASSERT_EQ(shouldRemainFalse, false);
+  ASSERT_EQ(shouldFlipToTrue, false);
+  ASSERT_EQ(alsoFlipToTrue, false);
+  ASSERT_EQ(shouldAlsoRemainFalse, false);
+  ASSERT_EQ(aThirdFalse, false);
 
   d_context->pop();
 
-  EXPECT_EQ(shouldRemainFalse, false);
-  EXPECT_EQ(shouldFlipToTrue, true);
-  EXPECT_EQ(alsoFlipToTrue, true);
-  EXPECT_EQ(shouldAlsoRemainFalse, false);
-  EXPECT_EQ(aThirdFalse, false);
+  ASSERT_EQ(shouldRemainFalse, false);
+  ASSERT_EQ(shouldFlipToTrue, true);
+  ASSERT_EQ(alsoFlipToTrue, true);
+  ASSERT_EQ(shouldAlsoRemainFalse, false);
+  ASSERT_EQ(aThirdFalse, false);
 }
 
 TEST_F(TestContextCDListBlack, empty_iterator)
 {
   CDList<int>* list = new (true) CDList<int>(d_context.get());
-  EXPECT_EQ(list->begin(), list->end());
+  ASSERT_EQ(list->begin(), list->end());
   list->deleteSelf();
 }
 
index 440d95d4028ce72324216034d2b50ed15247ec4a..cbf6a1cd9580fb48a3d25f3c6c4af4242caf825e 100644 (file)
@@ -37,14 +37,14 @@ TEST_F(TestContextCDOBlack, cdo)
   // Test that push/pop maintains the original value
   CDO<int> a1(d_context.get());
   a1 = 5;
-  EXPECT_EQ(d_context->getLevel(), 0);
+  ASSERT_EQ(d_context->getLevel(), 0);
   d_context->push();
   a1 = 10;
-  EXPECT_EQ(d_context->getLevel(), 1);
-  EXPECT_EQ(a1, 10);
+  ASSERT_EQ(d_context->getLevel(), 1);
+  ASSERT_EQ(a1, 10);
   d_context->pop();
-  EXPECT_EQ(d_context->getLevel(), 0);
-  EXPECT_EQ(a1, 5);
+  ASSERT_EQ(d_context->getLevel(), 0);
+  ASSERT_EQ(a1, 5);
 }
 
 }  // namespace test
index 6dfdba0c36fae91aa6a9ac66b0ba45093e16352a..7a8fa10a38c8bbe29596bedc0ebbe9ff64ec2b2a 100644 (file)
@@ -117,10 +117,10 @@ TEST_F(TestContextBlack, pre_post_notify)
   {
     MyContextNotifyObj c(d_context.get(), true), d(d_context.get(), false);
 
-    EXPECT_EQ(a.d_ncalls, 0);
-    EXPECT_EQ(b.d_ncalls, 0);
-    EXPECT_EQ(c.d_ncalls, 0);
-    EXPECT_EQ(d.d_ncalls, 0);
+    ASSERT_EQ(a.d_ncalls, 0);
+    ASSERT_EQ(b.d_ncalls, 0);
+    ASSERT_EQ(c.d_ncalls, 0);
+    ASSERT_EQ(d.d_ncalls, 0);
 
     MyContextObj w(d_context.get(), a);
     MyContextObj x(d_context.get(), b);
@@ -134,15 +134,15 @@ TEST_F(TestContextBlack, pre_post_notify)
     y.makeCurrent();
     z.makeCurrent();
 
-    EXPECT_EQ(a.d_ncalls, 0);
-    EXPECT_EQ(b.d_ncalls, 0);
-    EXPECT_EQ(c.d_ncalls, 0);
-    EXPECT_EQ(d.d_ncalls, 0);
+    ASSERT_EQ(a.d_ncalls, 0);
+    ASSERT_EQ(b.d_ncalls, 0);
+    ASSERT_EQ(c.d_ncalls, 0);
+    ASSERT_EQ(d.d_ncalls, 0);
 
-    EXPECT_EQ(w.d_ncalls, 0);
-    EXPECT_EQ(x.d_ncalls, 0);
-    EXPECT_EQ(y.d_ncalls, 0);
-    EXPECT_EQ(z.d_ncalls, 0);
+    ASSERT_EQ(w.d_ncalls, 0);
+    ASSERT_EQ(x.d_ncalls, 0);
+    ASSERT_EQ(y.d_ncalls, 0);
+    ASSERT_EQ(z.d_ncalls, 0);
 
     d_context->push();
 
@@ -151,39 +151,39 @@ TEST_F(TestContextBlack, pre_post_notify)
     y.makeCurrent();
     z.makeCurrent();
 
-    EXPECT_EQ(a.d_ncalls, 0);
-    EXPECT_EQ(b.d_ncalls, 0);
-    EXPECT_EQ(c.d_ncalls, 0);
-    EXPECT_EQ(d.d_ncalls, 0);
+    ASSERT_EQ(a.d_ncalls, 0);
+    ASSERT_EQ(b.d_ncalls, 0);
+    ASSERT_EQ(c.d_ncalls, 0);
+    ASSERT_EQ(d.d_ncalls, 0);
 
-    EXPECT_EQ(w.d_ncalls, 0);
-    EXPECT_EQ(x.d_ncalls, 0);
-    EXPECT_EQ(y.d_ncalls, 0);
-    EXPECT_EQ(z.d_ncalls, 0);
+    ASSERT_EQ(w.d_ncalls, 0);
+    ASSERT_EQ(x.d_ncalls, 0);
+    ASSERT_EQ(y.d_ncalls, 0);
+    ASSERT_EQ(z.d_ncalls, 0);
 
     d_context->pop();
 
-    EXPECT_EQ(a.d_ncalls, 1);
-    EXPECT_EQ(b.d_ncalls, 1);
-    EXPECT_EQ(c.d_ncalls, 1);
-    EXPECT_EQ(d.d_ncalls, 1);
+    ASSERT_EQ(a.d_ncalls, 1);
+    ASSERT_EQ(b.d_ncalls, 1);
+    ASSERT_EQ(c.d_ncalls, 1);
+    ASSERT_EQ(d.d_ncalls, 1);
 
-    EXPECT_EQ(w.d_ncalls, 1);
-    EXPECT_EQ(x.d_ncalls, 0);
-    EXPECT_EQ(y.d_ncalls, 1);
-    EXPECT_EQ(z.d_ncalls, 0);
+    ASSERT_EQ(w.d_ncalls, 1);
+    ASSERT_EQ(x.d_ncalls, 0);
+    ASSERT_EQ(y.d_ncalls, 1);
+    ASSERT_EQ(z.d_ncalls, 0);
 
     d_context->pop();
 
-    EXPECT_EQ(a.d_ncalls, 2);
-    EXPECT_EQ(b.d_ncalls, 2);
-    EXPECT_EQ(c.d_ncalls, 2);
-    EXPECT_EQ(d.d_ncalls, 2);
+    ASSERT_EQ(a.d_ncalls, 2);
+    ASSERT_EQ(b.d_ncalls, 2);
+    ASSERT_EQ(c.d_ncalls, 2);
+    ASSERT_EQ(d.d_ncalls, 2);
 
-    EXPECT_EQ(w.d_ncalls, 2);
-    EXPECT_EQ(x.d_ncalls, 1);
-    EXPECT_EQ(y.d_ncalls, 2);
-    EXPECT_EQ(z.d_ncalls, 1);
+    ASSERT_EQ(w.d_ncalls, 2);
+    ASSERT_EQ(x.d_ncalls, 1);
+    ASSERT_EQ(y.d_ncalls, 2);
+    ASSERT_EQ(z.d_ncalls, 1);
   }
   catch (Exception& e)
   {
@@ -211,28 +211,28 @@ TEST_F(TestContextBlack, top_scope_context_obj)
   MyContextObj x(true, d_context.get(), n);
   MyContextObj y(false, d_context.get(), n);
 
-  EXPECT_EQ(x.d_nsaves, 0);
-  EXPECT_EQ(y.d_nsaves, 0);
+  ASSERT_EQ(x.d_nsaves, 0);
+  ASSERT_EQ(y.d_nsaves, 0);
 
   x.makeCurrent();
   y.makeCurrent();
 
-  EXPECT_EQ(x.d_nsaves, 0);
-  EXPECT_EQ(y.d_nsaves, 1);
+  ASSERT_EQ(x.d_nsaves, 0);
+  ASSERT_EQ(y.d_nsaves, 1);
 
   d_context->push();
 
   x.makeCurrent();
   y.makeCurrent();
 
-  EXPECT_EQ(x.d_nsaves, 1);
-  EXPECT_EQ(y.d_nsaves, 2);
+  ASSERT_EQ(x.d_nsaves, 1);
+  ASSERT_EQ(y.d_nsaves, 2);
 
   d_context->pop();
   d_context->pop();
 
-  EXPECT_EQ(x.d_nsaves, 1);
-  EXPECT_EQ(y.d_nsaves, 2);
+  ASSERT_EQ(x.d_nsaves, 1);
+  ASSERT_EQ(y.d_nsaves, 2);
 }
 
 }  // namespace test
index c8ea5984811f80b768b4741a94792f5dfd0e1e1e..a6ea4d8801c651b690908852d3b652570572abf6 100644 (file)
@@ -32,152 +32,152 @@ TEST_F(TestContextWhite, simple)
 {
   Scope* s = d_context->getTopScope();
 
-  EXPECT_EQ(s, d_context->getBottomScope());
-  EXPECT_EQ(d_context->getLevel(), 0);
-  EXPECT_EQ(d_context->d_scopeList.size(), 1);
+  ASSERT_EQ(s, d_context->getBottomScope());
+  ASSERT_EQ(d_context->getLevel(), 0);
+  ASSERT_EQ(d_context->d_scopeList.size(), 1);
 
-  EXPECT_EQ(s->d_pContext, d_context.get());
-  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(s->d_level, 0);
-  EXPECT_EQ(s->d_pContextObjList, nullptr);
+  ASSERT_EQ(s->d_pContext, d_context.get());
+  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(s->d_level, 0);
+  ASSERT_EQ(s->d_pContextObjList, nullptr);
 
   CDO<int> a(d_context.get());
 
-  EXPECT_EQ(s->d_pContext, d_context.get());
-  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(s->d_level, 0);
-  EXPECT_EQ(s->d_pContextObjList, &a);
+  ASSERT_EQ(s->d_pContext, d_context.get());
+  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(s->d_level, 0);
+  ASSERT_EQ(s->d_pContextObjList, &a);
 
-  EXPECT_EQ(a.d_pScope, s);
-  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList);
+  ASSERT_EQ(a.d_pScope, s);
+  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &s->d_pContextObjList);
 
   CDO<int> b(d_context.get());
 
-  EXPECT_EQ(s->d_pContext, d_context.get());
-  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(s->d_level, 0);
-  EXPECT_EQ(s->d_pContextObjList, &b);
+  ASSERT_EQ(s->d_pContext, d_context.get());
+  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(s->d_level, 0);
+  ASSERT_EQ(s->d_pContextObjList, &b);
 
-  EXPECT_EQ(a.d_pScope, s);
-  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+  ASSERT_EQ(a.d_pScope, s);
+  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
 
-  EXPECT_EQ(b.d_pScope, s);
-  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(b.d_pContextObjNext, &a);
-  EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
+  ASSERT_EQ(b.d_pScope, s);
+  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(b.d_pContextObjNext, &a);
+  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
 
   d_context->push();
   Scope* t = d_context->getTopScope();
-  EXPECT_NE(s, t);
+  ASSERT_NE(s, t);
 
-  EXPECT_EQ(s, d_context->getBottomScope());
-  EXPECT_EQ(d_context->getLevel(), 1);
-  EXPECT_EQ(d_context->d_scopeList.size(), 2);
+  ASSERT_EQ(s, d_context->getBottomScope());
+  ASSERT_EQ(d_context->getLevel(), 1);
+  ASSERT_EQ(d_context->d_scopeList.size(), 2);
 
-  EXPECT_EQ(s->d_pContext, d_context.get());
-  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(s->d_level, 0);
-  EXPECT_EQ(s->d_pContextObjList, &b);
+  ASSERT_EQ(s->d_pContext, d_context.get());
+  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(s->d_level, 0);
+  ASSERT_EQ(s->d_pContextObjList, &b);
 
-  EXPECT_EQ(t->d_pContext, d_context.get());
-  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(t->d_level, 1);
-  EXPECT_EQ(t->d_pContextObjList, nullptr);
+  ASSERT_EQ(t->d_pContext, d_context.get());
+  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(t->d_level, 1);
+  ASSERT_EQ(t->d_pContextObjList, nullptr);
 
-  EXPECT_EQ(a.d_pScope, s);
-  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+  ASSERT_EQ(a.d_pScope, s);
+  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
 
-  EXPECT_EQ(b.d_pScope, s);
-  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(b.d_pContextObjNext, &a);
-  EXPECT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
+  ASSERT_EQ(b.d_pScope, s);
+  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(b.d_pContextObjNext, &a);
+  ASSERT_EQ(b.d_ppContextObjPrev, &s->d_pContextObjList);
 
   a = 5;
 
-  EXPECT_EQ(t->d_pContext, d_context.get());
-  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(t->d_level, 1);
-  EXPECT_EQ(t->d_pContextObjList, &a);
+  ASSERT_EQ(t->d_pContext, d_context.get());
+  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(t->d_level, 1);
+  ASSERT_EQ(t->d_pContextObjList, &a);
 
-  EXPECT_EQ(a.d_pScope, t);
-  EXPECT_NE(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList);
+  ASSERT_EQ(a.d_pScope, t);
+  ASSERT_NE(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &t->d_pContextObjList);
 
   b = 3;
 
-  EXPECT_EQ(t->d_pContext, d_context.get());
-  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(t->d_level, 1);
-  EXPECT_EQ(t->d_pContextObjList, &b);
+  ASSERT_EQ(t->d_pContext, d_context.get());
+  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(t->d_level, 1);
+  ASSERT_EQ(t->d_pContextObjList, &b);
 
-  EXPECT_EQ(a.d_pScope, t);
-  EXPECT_NE(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+  ASSERT_EQ(a.d_pScope, t);
+  ASSERT_NE(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
 
-  EXPECT_EQ(b.d_pScope, t);
-  EXPECT_NE(b.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(b.d_pContextObjNext, &a);
-  EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
+  ASSERT_EQ(b.d_pScope, t);
+  ASSERT_NE(b.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(b.d_pContextObjNext, &a);
+  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
 
   d_context->push();
   Scope* u = d_context->getTopScope();
-  EXPECT_NE(u, t);
-  EXPECT_NE(u, s);
+  ASSERT_NE(u, t);
+  ASSERT_NE(u, s);
 
   CDO<int> c(d_context.get());
   c = 4;
 
-  EXPECT_EQ(c.d_pScope, u);
-  EXPECT_NE(c.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(c.d_pContextObjNext, nullptr);
-  EXPECT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList);
+  ASSERT_EQ(c.d_pScope, u);
+  ASSERT_NE(c.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(c.d_pContextObjNext, nullptr);
+  ASSERT_EQ(c.d_ppContextObjPrev, &u->d_pContextObjList);
 
   d_context->pop();
 
-  EXPECT_EQ(t->d_pContext, d_context.get());
-  EXPECT_EQ(t->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(t->d_level, 1);
-  EXPECT_EQ(t->d_pContextObjList, &b);
+  ASSERT_EQ(t->d_pContext, d_context.get());
+  ASSERT_EQ(t->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(t->d_level, 1);
+  ASSERT_EQ(t->d_pContextObjList, &b);
 
-  EXPECT_EQ(a.d_pScope, t);
-  EXPECT_NE(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+  ASSERT_EQ(a.d_pScope, t);
+  ASSERT_NE(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
 
-  EXPECT_EQ(b.d_pScope, t);
-  EXPECT_NE(b.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(b.d_pContextObjNext, &a);
-  EXPECT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
+  ASSERT_EQ(b.d_pScope, t);
+  ASSERT_NE(b.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(b.d_pContextObjNext, &a);
+  ASSERT_EQ(b.d_ppContextObjPrev, &t->d_pContextObjList);
 
   d_context->pop();
 
-  EXPECT_EQ(s->d_pContext, d_context.get());
-  EXPECT_EQ(s->d_pCMM, d_context->d_pCMM);
-  EXPECT_EQ(s->d_level, 0);
-  EXPECT_EQ(s->d_pContextObjList, &c);
-
-  EXPECT_EQ(a.d_pScope, s);
-  EXPECT_EQ(a.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(a.d_pContextObjNext, nullptr);
-  EXPECT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
-
-  EXPECT_EQ(b.d_pScope, s);
-  EXPECT_EQ(b.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(b.d_pContextObjNext, &a);
-  EXPECT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext);
-
-  EXPECT_EQ(c.d_pScope, s);
-  EXPECT_EQ(c.d_pContextObjRestore, nullptr);
-  EXPECT_EQ(c.d_pContextObjNext, &b);
-  EXPECT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
+  ASSERT_EQ(s->d_pContext, d_context.get());
+  ASSERT_EQ(s->d_pCMM, d_context->d_pCMM);
+  ASSERT_EQ(s->d_level, 0);
+  ASSERT_EQ(s->d_pContextObjList, &c);
+
+  ASSERT_EQ(a.d_pScope, s);
+  ASSERT_EQ(a.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(a.d_pContextObjNext, nullptr);
+  ASSERT_EQ(a.d_ppContextObjPrev, &b.d_pContextObjNext);
+
+  ASSERT_EQ(b.d_pScope, s);
+  ASSERT_EQ(b.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(b.d_pContextObjNext, &a);
+  ASSERT_EQ(b.d_ppContextObjPrev, &c.d_pContextObjNext);
+
+  ASSERT_EQ(c.d_pScope, s);
+  ASSERT_EQ(c.d_pContextObjRestore, nullptr);
+  ASSERT_EQ(c.d_pContextObjNext, &b);
+  ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
 }
 }  // namespace test
 }  // namespace CVC4
index cd2745a07a26b7c3cbe3253998362b263bbcadde..da15f6b63d6dfd78463afe7a43ab554996fb0099 100644 (file)
@@ -64,7 +64,7 @@ TEST_F(TestExprBlackAttribute, ints)
   ASSERT_FALSE(node->getAttribute(attr, data0));
   node->setAttribute(attr, val);
   ASSERT_TRUE(node->getAttribute(attr, data1));
-  EXPECT_EQ(data1, val);
+  ASSERT_EQ(data1, val);
 
   delete node;
 }
@@ -82,7 +82,7 @@ TEST_F(TestExprBlackAttribute, tnodes)
   ASSERT_FALSE(node->getAttribute(attr, data0));
   node->setAttribute(attr, val);
   ASSERT_TRUE(node->getAttribute(attr, data1));
-  EXPECT_EQ(data1, val);
+  ASSERT_EQ(data1, val);
 
   delete node;
 }
@@ -100,7 +100,7 @@ TEST_F(TestExprBlackAttribute, strings)
   ASSERT_FALSE(node->getAttribute(attr, data0));
   node->setAttribute(attr, val);
   ASSERT_TRUE(node->getAttribute(attr, data1));
-  EXPECT_EQ(data1, val);
+  ASSERT_EQ(data1, val);
 
   delete node;
 }
@@ -116,10 +116,10 @@ TEST_F(TestExprBlackAttribute, bools)
 
   BoolAttribute attr;
   ASSERT_TRUE(node->getAttribute(attr, data0));
-  EXPECT_EQ(false, data0);
+  ASSERT_EQ(false, data0);
   node->setAttribute(attr, val);
   ASSERT_TRUE(node->getAttribute(attr, data1));
-  EXPECT_EQ(data1, val);
+  ASSERT_EQ(data1, val);
 
   delete node;
 }
index 1403fbe21b981baab37f53c141dad67fa9fd1b6a..ab99b842f87f5968857adc3b8387c2ff528d576f 100644 (file)
@@ -80,33 +80,33 @@ TEST_F(TestExprWhiteAttribute, attribute_ids)
   // those that have already been assigned.
 
   unsigned lastId = attr::LastAttributeId<std::string, false>::getId();
-  EXPECT_LT(VarNameAttr::s_id, lastId);
-  EXPECT_LT(TestStringAttr1::s_id, lastId);
-  EXPECT_LT(TestStringAttr2::s_id, lastId);
+  ASSERT_LT(VarNameAttr::s_id, lastId);
+  ASSERT_LT(TestStringAttr1::s_id, lastId);
+  ASSERT_LT(TestStringAttr2::s_id, lastId);
 
-  EXPECT_NE(VarNameAttr::s_id, TestStringAttr1::s_id);
-  EXPECT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
-  EXPECT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
+  ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id);
+  ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id);
+  ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id);
 
   lastId = attr::LastAttributeId<bool, false>::getId();
-  EXPECT_LT(TestFlag1::s_id, lastId);
-  EXPECT_LT(TestFlag2::s_id, lastId);
-  EXPECT_LT(TestFlag3::s_id, lastId);
-  EXPECT_LT(TestFlag4::s_id, lastId);
-  EXPECT_LT(TestFlag5::s_id, lastId);
-  EXPECT_NE(TestFlag1::s_id, TestFlag2::s_id);
-  EXPECT_NE(TestFlag1::s_id, TestFlag3::s_id);
-  EXPECT_NE(TestFlag1::s_id, TestFlag4::s_id);
-  EXPECT_NE(TestFlag1::s_id, TestFlag5::s_id);
-  EXPECT_NE(TestFlag2::s_id, TestFlag3::s_id);
-  EXPECT_NE(TestFlag2::s_id, TestFlag4::s_id);
-  EXPECT_NE(TestFlag2::s_id, TestFlag5::s_id);
-  EXPECT_NE(TestFlag3::s_id, TestFlag4::s_id);
-  EXPECT_NE(TestFlag3::s_id, TestFlag5::s_id);
-  EXPECT_NE(TestFlag4::s_id, TestFlag5::s_id);
+  ASSERT_LT(TestFlag1::s_id, lastId);
+  ASSERT_LT(TestFlag2::s_id, lastId);
+  ASSERT_LT(TestFlag3::s_id, lastId);
+  ASSERT_LT(TestFlag4::s_id, lastId);
+  ASSERT_LT(TestFlag5::s_id, lastId);
+  ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id);
+  ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id);
+  ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id);
 
   lastId = attr::LastAttributeId<TypeNode, false>::getId();
-  EXPECT_LT(TypeAttr::s_id, lastId);
+  ASSERT_LT(TypeAttr::s_id, lastId);
 }
 
 TEST_F(TestExprWhiteAttribute, attributes)
@@ -305,25 +305,25 @@ TEST_F(TestExprWhiteAttribute, attributes)
   Debug("boolattr") << "set flag 5 on unnamed to T\n";
   unnamed.setAttribute(TestFlag5(), true);
 
-  EXPECT_EQ(a.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "");
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "a");
-  EXPECT_EQ(b.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "b");
-  EXPECT_EQ(c.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c");
-  EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
 
   ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
 
@@ -386,25 +386,25 @@ TEST_F(TestExprWhiteAttribute, attributes)
   b.setAttribute(TestStringAttr1(), "bar");
   c.setAttribute(TestStringAttr1(), "baz");
 
-  EXPECT_EQ(a.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "");
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "a");
-  EXPECT_EQ(b.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "b");
-  EXPECT_EQ(c.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
 
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c");
-  EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
 
   ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
 
@@ -422,25 +422,25 @@ TEST_F(TestExprWhiteAttribute, attributes)
   b.setAttribute(VarNameAttr(), "c");
   c.setAttribute(VarNameAttr(), "a");
 
-  EXPECT_EQ(c.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(c.getAttribute(VarNameAttr()), "");
-
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "a");
-  EXPECT_EQ(a.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(a.getAttribute(VarNameAttr()), "");
-
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "b");
-  EXPECT_EQ(b.getAttribute(VarNameAttr()), "c");
-  EXPECT_NE(b.getAttribute(VarNameAttr()), "");
-
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "a");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "b");
-  EXPECT_NE(unnamed.getAttribute(VarNameAttr()), "c");
-  EXPECT_EQ(unnamed.getAttribute(VarNameAttr()), "");
+  ASSERT_EQ(c.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(c.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "a");
+  ASSERT_EQ(a.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(a.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "b");
+  ASSERT_EQ(b.getAttribute(VarNameAttr()), "c");
+  ASSERT_NE(b.getAttribute(VarNameAttr()), "");
+
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b");
+  ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c");
+  ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), "");
 
   ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
 }
index 93b7c15cbd3a4b9a51eb4ef1db2012597c0a37fb..a5bba4d99da937aa9583b6f217f0b80246a52238 100644 (file)
@@ -57,16 +57,16 @@ class TestExprBlackKind : public TestExprBlack
 
 TEST_F(TestExprBlackKind, equality)
 {
-  EXPECT_EQ(undefined, UNDEFINED_KIND);
-  EXPECT_EQ(last, LAST_KIND);
+  ASSERT_EQ(undefined, UNDEFINED_KIND);
+  ASSERT_EQ(last, LAST_KIND);
 }
 
 TEST_F(TestExprBlackKind, order)
 {
-  EXPECT_LT((int32_t)undefined, (int32_t)null);
-  EXPECT_LT((int32_t)null, (int32_t)last);
-  EXPECT_LT((int32_t)undefined, (int32_t)last);
-  EXPECT_LT((int32_t)last, (int32_t)unknown);
+  ASSERT_LT((int32_t)undefined, (int32_t)null);
+  ASSERT_LT((int32_t)null, (int32_t)last);
+  ASSERT_LT((int32_t)undefined, (int32_t)last);
+  ASSERT_LT((int32_t)last, (int32_t)unknown);
 }
 
 TEST_F(TestExprBlackKind, output)
@@ -84,7 +84,7 @@ TEST_F(TestExprBlackKind, output_concat)
       << "NULL"
       << "LAST_KIND"
       << "?";
-  EXPECT_EQ(act.str(), exp.str());
+  ASSERT_EQ(act.str(), exp.str());
 }
 }  // namespace test
 }  // namespace CVC4
index dd1982b1cc1d2bab524c592769ea525ef6f29780..95018d9f164ef96a0e5da93ef0f5438a625966f2 100644 (file)
@@ -43,8 +43,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols1)
   Node n = d_nodeManager->mkNode(NOT, x);
   std::unordered_set<Node, NodeHashFunction> syms;
   getSymbols(n, syms);
-  EXPECT_EQ(syms.size(), 1);
-  EXPECT_NE(syms.find(x), syms.end());
+  ASSERT_EQ(syms.size(), 1);
+  ASSERT_NE(syms.find(x), syms.end());
 }
 
 TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
@@ -74,10 +74,10 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_symbols2)
   getSymbols(res, syms);
 
   // assertions
-  EXPECT_EQ(syms.size(), 2);
-  EXPECT_NE(syms.find(x), syms.end());
-  EXPECT_NE(syms.find(y), syms.end());
-  EXPECT_EQ(syms.find(var), syms.end());
+  ASSERT_EQ(syms.size(), 2);
+  ASSERT_NE(syms.find(x), syms.end());
+  ASSERT_NE(syms.find(y), syms.end());
+  ASSERT_EQ(syms.find(var), syms.end());
 }
 
 TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
@@ -104,34 +104,34 @@ TEST_F(TestNodeBlackNodeAlgorithm, get_operators_map)
 
   // Verify result
   // We should have only integer, bv and boolean as types
-  EXPECT_EQ(result.size(), 3);
-  EXPECT_NE(result.find(*d_intTypeNode), result.end());
-  EXPECT_NE(result.find(*d_boolTypeNode), result.end());
-  EXPECT_NE(result.find(*d_bvTypeNode), result.end());
+  ASSERT_EQ(result.size(), 3);
+  ASSERT_NE(result.find(*d_intTypeNode), result.end());
+  ASSERT_NE(result.find(*d_boolTypeNode), result.end());
+  ASSERT_NE(result.find(*d_bvTypeNode), result.end());
 
   // in integers, we should only have plus and mult as operators
-  EXPECT_EQ(result[*d_intTypeNode].size(), 2);
-  EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
+  ASSERT_EQ(result[*d_intTypeNode].size(), 2);
+  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(PLUS)),
             result[*d_intTypeNode].end());
-  EXPECT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
+  ASSERT_NE(result[*d_intTypeNode].find(d_nodeManager->operatorOf(MULT)),
             result[*d_intTypeNode].end());
 
   // in booleans, we should only have "=" and "and" as an operator.
-  EXPECT_EQ(result[*d_boolTypeNode].size(), 2);
-  EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
+  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
+  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(EQUAL)),
             result[*d_boolTypeNode].end());
-  EXPECT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
+  ASSERT_NE(result[*d_boolTypeNode].find(d_nodeManager->operatorOf(AND)),
             result[*d_boolTypeNode].end());
 
   // in bv, we should only have "extract" as an operator.
-  EXPECT_EQ(result[*d_boolTypeNode].size(), 2);
+  ASSERT_EQ(result[*d_boolTypeNode].size(), 2);
   Node extractOp1 =
       d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(1, 0));
   Node extractOp2 =
       d_nodeManager->mkConst<BitVectorExtract>(BitVectorExtract(3, 2));
-  EXPECT_NE(result[*d_bvTypeNode].find(extractOp1),
+  ASSERT_NE(result[*d_bvTypeNode].find(extractOp1),
             result[*d_bvTypeNode].end());
-  EXPECT_NE(result[*d_bvTypeNode].find(extractOp2),
+  ASSERT_NE(result[*d_bvTypeNode].find(extractOp2),
             result[*d_bvTypeNode].end());
 }
 
@@ -150,15 +150,15 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
 
   // check reflexivity
   ASSERT_TRUE(match(n1, n1, subs));
-  EXPECT_EQ(subs.size(), 0);
+  ASSERT_EQ(subs.size(), 0);
 
   Node n2 = d_nodeManager->mkNode(MULT, two, a);
   subs.clear();
 
   // check instance
   ASSERT_TRUE(match(n1, n2, subs));
-  EXPECT_EQ(subs.size(), 1);
-  EXPECT_EQ(subs[x], a);
+  ASSERT_EQ(subs.size(), 1);
+  ASSERT_EQ(subs[x], a);
 
   // should return false for flipped arguments (match is not symmetric)
   ASSERT_FALSE(match(n2, n1, subs));
@@ -195,8 +195,8 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
 
   // implementation: check if the cache works correctly
   ASSERT_TRUE(match(n1, n2, subs));
-  EXPECT_EQ(subs.size(), 1);
-  EXPECT_EQ(subs[x], a);
+  ASSERT_EQ(subs.size(), 1);
+  ASSERT_EQ(subs[x], a);
 }
 }  // namespace test
 }  // namespace CVC4
index 59f8186acc4b0305ab6df5d6de0960caaab9b1bb..4d60dea529a0f2e4eec8d7ef2264df83f7e8505e 100644 (file)
@@ -64,7 +64,7 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
     //    (singleton (singleton_op Int) 1)
     //    (as emptyset (Set Real)))
     TS_ASSERT_THROWS(d_slv->mkTerm(UNION, singletonInt, emptyReal),
-                     CVC4ApiException);
+                     CVC4ApiException&);
     // (union
     //    (singleton (singleton_op Real) 1)
     //    (as emptyset (Set Real)))