Merge branch 'master' into fix1649fix1649

4 files changed, 67 insertions, 28 deletions

diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
index d153b8a91..6f9d8206d 100644
--- a/test/unit/api/java/cvc5/SolverTest.java
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -623,6 +623,11 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
   }
 
+  @Test void mkSepEmp()
+  {
+    assertDoesNotThrow(() -> d_solver.mkSepEmp());
+  }
+
   @Test void mkSepNil()
   {
     assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort()));
@@ -2342,4 +2347,4 @@ class SolverTest
             + "\"Z\")))",
         projection.toString());
   }
-}
\ No newline at end of file
+}
diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java
index f2f9edaed..1ea703268 100644
--- a/test/unit/api/java/cvc5/SortTest.java
+++ b/test/unit/api/java/cvc5/SortTest.java
@@ -458,28 +458,28 @@ class SortTest
     assertThrows(CVC5ApiException.class, () -> bvSort.getSortConstructorArity());
   }
 
-  @Test void getBVSize() throws CVC5ApiException
+  @Test void getBitVectorSize() throws CVC5ApiException
   {
     Sort bvSort = d_solver.mkBitVectorSort(32);
-    assertDoesNotThrow(() -> bvSort.getBVSize());
+    assertDoesNotThrow(() -> bvSort.getBitVectorSize());
     Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    assertThrows(CVC5ApiException.class, () -> setSort.getBVSize());
+    assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize());
   }
 
-  @Test void getFPExponentSize() throws CVC5ApiException
+  @Test void getFloatingPointExponentSize() throws CVC5ApiException
   {
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-    assertDoesNotThrow(() -> fpSort.getFPExponentSize());
+    assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize());
     Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize());
+    assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize());
   }
 
-  @Test void getFPSignificandSize() throws CVC5ApiException
+  @Test void getFloatingPointSignificandSize() throws CVC5ApiException
   {
     Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-    assertDoesNotThrow(() -> fpSort.getFPSignificandSize());
+    assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize());
     Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-    assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize());
+    assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize());
   }
 
   @Test void getDatatypeParamSorts() throws CVC5ApiException
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 19113ae13..c9527c2d4 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -376,15 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode)
   ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO));
 }
 
-TEST_F(TestApiBlackSolver, mkUninterpretedConst)
-{
-  ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
-  ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException);
-  Solver slv;
-  ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1),
-               CVC5ApiException);
-}
-
 TEST_F(TestApiBlackSolver, mkAbstractValue)
 {
   ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1")));
@@ -606,6 +597,8 @@ TEST_F(TestApiBlackSolver, mkRegexpSigma)
       d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
 }
 
+TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); }
+
 TEST_F(TestApiBlackSolver, mkSepNil)
 {
   ASSERT_NO_THROW(d_solver.mkSepNil(d_solver.getBooleanSort()));
@@ -1234,6 +1227,23 @@ TEST_F(TestApiBlackSolver, getAbduct)
   ASSERT_EQ(output2, truen);
 }
 
+TEST_F(TestApiBlackSolver, getAbduct2)
+{
+  d_solver.setLogic("QF_LIA");
+  d_solver.setOption("incremental", "false");
+  Sort intSort = d_solver.getIntegerSort();
+  Term zero = d_solver.mkInteger(0);
+  Term x = d_solver.mkConst(intSort, "x");
+  Term y = d_solver.mkConst(intSort, "y");
+  // Assumptions for abduction: x > 0
+  d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
+  // Conjecture for abduction: y > 0
+  Term conj = d_solver.mkTerm(GT, y, zero);
+  Term output;
+  // Fails due to option not set
+  ASSERT_THROW(d_solver.getAbduct(conj, output), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, getInterpolant)
 {
   d_solver.setLogic("QF_LIA");
@@ -2536,5 +2546,21 @@ TEST_F(TestApiBlackSolver, Output)
   ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf());
 }
 
+
+TEST_F(TestApiBlackSolver, issue7000)
+{
+  Sort s1 = d_solver.getIntegerSort();
+  Sort s2 = d_solver.mkFunctionSort(s1, s1);
+  Sort s3 = d_solver.getRealSort();
+  Term t4 = d_solver.mkPi();
+  Term t7 = d_solver.mkConst(s3, "_x5");
+  Term t37 = d_solver.mkConst(s2, "_x32");
+  Term t59 = d_solver.mkConst(s2, "_x51");
+  Term t72 = d_solver.mkTerm(EQUAL, t37, t59);
+  Term t74 = d_solver.mkTerm(GT, t4, t7);
+  // throws logic exception since logic is not higher order by default
+  ASSERT_THROW(d_solver.checkEntailed({t72, t74, t72, t72}), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index 757bacad6..d0c755cf7 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -61,6 +61,14 @@ TEST_F(TestApiBlackSort, operators_comparison)
   ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort());
 }
 
+TEST_F(TestApiBlackSort, isNull)
+{
+  Sort x;
+  ASSERT_TRUE(x.isNull());
+  x = d_solver.getBooleanSort();
+  ASSERT_FALSE(x.isNull());
+}
+
 TEST_F(TestApiBlackSort, isBoolean)
 {
   ASSERT_TRUE(d_solver.getBooleanSort().isBoolean());
@@ -470,28 +478,28 @@ TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
   ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSort, getBVSize)
+TEST_F(TestApiBlackSort, getBitVectorSize)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);
-  ASSERT_NO_THROW(bvSort.getBVSize());
+  ASSERT_NO_THROW(bvSort.getBitVectorSize());
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  ASSERT_THROW(setSort.getBVSize(), CVC5ApiException);
+  ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSort, getFPExponentSize)
+TEST_F(TestApiBlackSort, getFloatingPointExponentSize)
 {
   Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  ASSERT_NO_THROW(fpSort.getFPExponentSize());
+  ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize());
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  ASSERT_THROW(setSort.getFPExponentSize(), CVC5ApiException);
+  ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSort, getFPSignificandSize)
+TEST_F(TestApiBlackSort, getFloatingPointSignificandSize)
 {
   Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-  ASSERT_NO_THROW(fpSort.getFPSignificandSize());
+  ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize());
   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-  ASSERT_THROW(setSort.getFPSignificandSize(), CVC5ApiException);
+  ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException);
 }
 
 TEST_F(TestApiBlackSort, getDatatypeParamSorts)