summaryrefslogtreecommitdiff
path: root/test/unit/api/op_black.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/api/op_black.cpp')
-rw-r--r--test/unit/api/op_black.cpp14
1 files changed, 0 insertions, 14 deletions
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 7183fa7a7..8c4e31c22 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -50,7 +50,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
{
Op plus = d_solver.mkOp(PLUS);
Op divisible = d_solver.mkOp(DIVISIBLE, 4);
- Op record_update = d_solver.mkOp(RECORD_UPDATE, "test");
Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5);
Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
@@ -60,7 +59,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
Op iand = d_solver.mkOp(IAND, 3);
Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
- Op tuple_update = d_solver.mkOp(TUPLE_UPDATE, 5);
Op floatingpoint_to_fp_ieee_bitvector =
d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
Op floatingpoint_to_fp_floatingpoint =
@@ -76,7 +74,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
ASSERT_EQ(0, plus.getNumIndices());
ASSERT_EQ(1, divisible.getNumIndices());
- ASSERT_EQ(1, record_update.getNumIndices());
ASSERT_EQ(1, bitvector_repeat.getNumIndices());
ASSERT_EQ(1, bitvector_zero_extend.getNumIndices());
ASSERT_EQ(1, bitvector_sign_extend.getNumIndices());
@@ -86,7 +83,6 @@ TEST_F(TestApiBlackOp, getNumIndices)
ASSERT_EQ(1, iand.getNumIndices());
ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices());
ASSERT_EQ(1, floatingopint_to_sbv.getNumIndices());
- ASSERT_EQ(1, tuple_update.getNumIndices());
ASSERT_EQ(2, floatingpoint_to_fp_ieee_bitvector.getNumIndices());
ASSERT_EQ(2, floatingpoint_to_fp_floatingpoint.getNumIndices());
ASSERT_EQ(2, floatingpoint_to_fp_real.getNumIndices());
@@ -105,11 +101,6 @@ TEST_F(TestApiBlackOp, getIndicesString)
ASSERT_TRUE(divisible_ot.isIndexed());
std::string divisible_idx = divisible_ot.getIndices<std::string>();
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>();
- ASSERT_EQ(record_update_idx, "test");
- ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException);
}
TEST_F(TestApiBlackOp, getIndicesUint)
@@ -155,11 +146,6 @@ TEST_F(TestApiBlackOp, getIndicesUint)
uint32_t floatingpoint_to_sbv_idx =
floatingpoint_to_sbv_ot.getIndices<uint32_t>();
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>();
- ASSERT_EQ(tuple_update_idx, 5);
- ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException);
}
TEST_F(TestApiBlackOp, getIndicesPairUint)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback