3 files changed, 65 insertions, 3 deletions
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 8c4e31c22..fd45b1c22 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -92,6 +92,52 @@ TEST_F(TestApiBlackOp, getNumIndices)
   ASSERT_EQ(2, regexp_loop.getNumIndices());
 }
 
+TEST_F(TestApiBlackOp, subscriptOperator)
+{
+  Op plus = d_solver.mkOp(PLUS);
+  Op divisible = d_solver.mkOp(DIVISIBLE, 4);
+  Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4);
+  Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4);
+  Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 4);
+  Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 4);
+  Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 4);
+  Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 4);
+  Op iand = d_solver.mkOp(IAND, 4);
+  Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 4);
+  Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 4);
+  Op floatingpoint_to_fp_ieee_bitvector =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 5);
+  Op floatingpoint_to_fp_floatingpoint =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 5);
+  Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 5);
+  Op floatingpoint_to_fp_signed_bitvector =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 5);
+  Op floatingpoint_to_fp_unsigned_bitvector =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 5);
+  Op floatingpoint_to_fp_generic =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 5);
+  Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 4, 5);
+
+  ASSERT_THROW(plus[0], CVC5ApiException);
+  ASSERT_EQ(4, divisible[0].getUInt32Value());
+  ASSERT_EQ(4, bitvector_repeat[0].getUInt32Value());
+  ASSERT_EQ(4, bitvector_zero_extend[0].getUInt32Value());
+  ASSERT_EQ(4, bitvector_sign_extend[0].getUInt32Value());
+  ASSERT_EQ(4, bitvector_rotate_left[0].getUInt32Value());
+  ASSERT_EQ(4, bitvector_rotate_right[0].getUInt32Value());
+  ASSERT_EQ(4, int_to_bitvector[0].getUInt32Value());
+  ASSERT_EQ(4, iand[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_ubv[0].getUInt32Value());
+  ASSERT_EQ(4, floatingopint_to_sbv[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_ieee_bitvector[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_floatingpoint[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_real[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_signed_bitvector[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_unsigned_bitvector[0].getUInt32Value());
+  ASSERT_EQ(4, floatingpoint_to_fp_generic[0].getUInt32Value());
+  ASSERT_EQ(4, regexp_loop[0].getUInt32Value());
+}
+
 TEST_F(TestApiBlackOp, getIndicesString)
 {
   Op x;
@@ -207,6 +253,22 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
                CVC5ApiException);
 }
 
+TEST_F(TestApiBlackOp, getIndicesVector)
+{
+  std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
+  Op tuple_project_op = d_solver.mkOp(TUPLE_PROJECT, indices);
+
+  ASSERT_TRUE(tuple_project_op.isIndexed());
+  std::vector<Term> tuple_project_extract_indices =
+      tuple_project_op.getIndices<std::vector<Term>>();
+  ASSERT_THROW(tuple_project_op.getIndices<std::string>(), CVC5ApiException);
+  for (size_t i = 0; i < indices.size(); i++)
+  {
+    ASSERT_EQ(indices[i], tuple_project_extract_indices[i].getUInt32Value());
+    ASSERT_EQ(indices[i], tuple_project_op[i].getUInt32Value());
+  }
+}
+
 TEST_F(TestApiBlackOp, opScopingToString)
 {
   Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 522270de4..787dd77ca 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -27,6 +27,7 @@
 #include "expr/node_manager.h"
 #include "expr/node_value.h"
 #include "expr/skolem_manager.h"
+#include "options/options_public.h"
 #include "smt/smt_engine.h"
 #include "test_node.h"
 #include "theory/rewriter.h"
@@ -68,7 +69,7 @@ class TestNodeBlackNode : public TestNode
     argv[0] = strdup("");
     argv[1] = strdup("--output-lang=ast");
     std::string progName;
-    Options::parseOptions(&opts, 2, argv, progName);
+    options::parse(opts, 2, argv, progName);
     free(argv[0]);
     free(argv[1]);
     d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index 766d696a1..d8ae8e468 100644
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -53,13 +53,12 @@ TEST_F(TestTheoryBlack, array_const)
   arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
   ASSERT_TRUE(arr.isConst());
   Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
-  ASSERT_FALSE(arr2.isConst());
   arr2 = Rewriter::rewrite(arr2);
   ASSERT_TRUE(arr2.isConst());
   arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+  arr2 = Rewriter::rewrite(arr2);
   ASSERT_TRUE(arr2.isConst());
   arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
-  ASSERT_FALSE(arr2.isConst());
   arr2 = Rewriter::rewrite(arr2);
   ASSERT_TRUE(arr2.isConst());