diff options
Diffstat (limited to 'test/unit/api/term_black.cpp')
-rw-r--r-- | test/unit/api/term_black.cpp | 34 |
1 files changed, 11 insertions, 23 deletions
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp index 7cfbe2527..3c4493ac6 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -885,16 +885,17 @@ TEST_F(TestApiBlackTerm, getBitVector) TEST_F(TestApiBlackTerm, getAbstractValue) { - Term v1 = d_solver.mkAbstractValue(1); - Term v2 = d_solver.mkAbstractValue("15"); - Term v3 = d_solver.mkAbstractValue("18446744073709551617"); - - ASSERT_TRUE(v1.isAbstractValue()); - ASSERT_TRUE(v2.isAbstractValue()); - ASSERT_TRUE(v3.isAbstractValue()); - ASSERT_EQ("1", v1.getAbstractValue()); - ASSERT_EQ("15", v2.getAbstractValue()); - ASSERT_EQ("18446744073709551617", v3.getAbstractValue()); + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + ASSERT_TRUE(d_solver.checkSat().isSat()); + Term vx = d_solver.getValue(x); + Term vy = d_solver.getValue(y); + ASSERT_TRUE(vx.isAbstractValue()); + ASSERT_TRUE(vy.isAbstractValue()); + ASSERT_EQ(vx.getAbstractValue(), vy.getAbstractValue()); } TEST_F(TestApiBlackTerm, getTuple) @@ -994,19 +995,6 @@ TEST_F(TestApiBlackTerm, getSequence) ASSERT_EQ(std::vector<Term>({i1, i1, i2}), s5.getSequenceValue()); } -TEST_F(TestApiBlackTerm, getUninterpretedConst) -{ - Sort s = d_solver.mkUninterpretedSort("test"); - Term t1 = d_solver.mkUninterpretedConst(s, 3); - Term t2 = d_solver.mkUninterpretedConst(s, 5); - - ASSERT_TRUE(t1.isUninterpretedValue()); - ASSERT_TRUE(t2.isUninterpretedValue()); - - ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue()); - ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue()); -} - TEST_F(TestApiBlackTerm, substitute) { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); |