Merge branch 'master' into fix6520fix6520

5 files changed, 530 insertions, 137 deletions

diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index 87ddbb5d6..7f05bf130 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -39,5 +39,4 @@ macro(cvc5_add_python_api_test name filename)
 endmacro()
 
 cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py)
-cvc5_add_python_api_test(pytest_grammar test_grammar.py)
 cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py)
diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
deleted file mode 100644
index f83bee548..000000000
--- a/test/api/python/test_grammar.py
+++ /dev/null
@@ -1,130 +0,0 @@
-###############################################################################
-# Top contributors (to current version):
-#   Yoni Zohar, Makai Mann, Mudathir Mohamed
-#
-# This file is part of the cvc5 project.
-#
-# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
-# in the top-level source directory and their institutional affiliations.
-# All rights reserved.  See the file COPYING in the top-level source
-# directory for licensing information.
-# #############################################################################
-#
-# Translated from test/unit/api/grammar_black.h
-##
-
-import pytest
-
-import pycvc5
-from pycvc5 import kinds
-
-def test_add_rule():
-  solver = pycvc5.Solver()
-  boolean = solver.getBooleanSort()
-  integer = solver.getIntegerSort()
-
-  nullTerm = pycvc5.Term(solver)
-  start = solver.mkVar(boolean)
-  nts = solver.mkVar(boolean)
-
-  # expecting no error
-  g = solver.mkSygusGrammar([], [start])
-
-  g.addRule(start, solver.mkBoolean(False))
-
-  # expecting errors
-  with pytest.raises(Exception):
-    g.addRule(nullTerm, solver.mkBoolean(false))
-  with pytest.raises(Exception):
-    g.addRule(start, nullTerm)
-  with pytest.raises(Exception):
-    g.addRule(nts, solver.mkBoolean(false))
-  with pytest.raises(Exception):
-    g.addRule(start, solver.mkInteger(0))
-
-  # expecting no errors
-  solver.synthFun("f", {}, boolean, g)
-
-  # expecting an error
-  with pytest.raises(Exception):
-    g.addRule(start, solver.mkBoolean(false))
-
-def test_add_rules():
-  solver = pycvc5.Solver()
-  boolean = solver.getBooleanSort()
-  integer = solver.getIntegerSort()
-
-  nullTerm = pycvc5.Term(solver)
-  start = solver.mkVar(boolean)
-  nts = solver.mkVar(boolean)
-
-  g = solver.mkSygusGrammar([], [start])
-
-  g.addRules(start, {solver.mkBoolean(False)})
-
-  #Expecting errors
-  with pytest.raises(Exception):
-    g.addRules(nullTerm, solver.mkBoolean(False))
-  with pytest.raises(Exception):
-    g.addRules(start, {nullTerm})
-  with pytest.raises(Exception):
-    g.addRules(nts, {solver.mkBoolean(False)})
-  with pytest.raises(Exception):
-    g.addRules(start, {solver.mkInteger(0)})
-  #Expecting no errors
-  solver.synthFun("f", {}, boolean, g)
-
-  #Expecting an error
-  with pytest.raises(Exception):
-    g.addRules(start, solver.mkBoolean(False))
-
-def testAddAnyConstant():
-  solver = pycvc5.Solver()
-  boolean = solver.getBooleanSort()
-
-  nullTerm = pycvc5.Term(solver)
-  start = solver.mkVar(boolean)
-  nts = solver.mkVar(boolean)
-
-  g = solver.mkSygusGrammar({}, {start})
-
-  g.addAnyConstant(start)
-  g.addAnyConstant(start)
-
-  with pytest.raises(Exception):
-    g.addAnyConstant(nullTerm)
-  with pytest.raises(Exception):
-    g.addAnyConstant(nts)
-
-  solver.synthFun("f", {}, boolean, g)
-
-  with pytest.raises(Exception):
-    g.addAnyConstant(start)
-
-
-def testAddAnyVariable():
-  solver = pycvc5.Solver()
-  boolean = solver.getBooleanSort()
-
-  nullTerm = pycvc5.Term(solver)
-  x = solver.mkVar(boolean)
-  start = solver.mkVar(boolean)
-  nts = solver.mkVar(boolean)
-
-  g1 = solver.mkSygusGrammar({x}, {start})
-  g2 = solver.mkSygusGrammar({}, {start})
-
-  g1.addAnyVariable(start)
-  g1.addAnyVariable(start)
-  g2.addAnyVariable(start)
-
-  with pytest.raises(Exception):
-    g1.addAnyVariable(nullTerm)
-  with pytest.raises(Exception):
-    g1.addAnyVariable(nts)
-
-  solver.synthFun("f", {}, boolean, g1)
-
-  with pytest.raises(Exception):
-    g1.addAnyVariable(start)
-
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
index b7de1cbb0..6091e3275 100644
--- a/test/python/CMakeLists.txt
+++ b/test/python/CMakeLists.txt
@@ -30,3 +30,4 @@ endmacro()
 cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py)
 cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py)
 cvc5_add_python_api_test(pytest_term unit/api/test_term.py)
+cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py)
diff --git a/test/python/unit/api/test_grammar.py b/test/python/unit/api/test_grammar.py
new file mode 100644
index 000000000..db567a6ba
--- /dev/null
+++ b/test/python/unit/api/test_grammar.py
@@ -0,0 +1,137 @@
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Makai Mann, Mudathir Mohamed
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Translated from test/unit/api/grammar_black.h
+##
+
+import pytest
+
+import pycvc5
+from pycvc5 import kinds, Term
+
+
+@pytest.fixture
+def solver():
+    return pycvc5.Solver()
+
+
+def test_add_rule(solver):
+    boolean = solver.getBooleanSort()
+    integer = solver.getIntegerSort()
+
+    null_term = Term(solver)
+    start = solver.mkVar(boolean)
+    nts = solver.mkVar(boolean)
+
+    # expecting no error
+    g = solver.mkSygusGrammar([], [start])
+
+    g.addRule(start, solver.mkBoolean(False))
+
+    # expecting errors
+    with pytest.raises(RuntimeError):
+        g.addRule(null_term, solver.mkBoolean(False))
+    with pytest.raises(RuntimeError):
+        g.addRule(start, null_term)
+    with pytest.raises(RuntimeError):
+        g.addRule(nts, solver.mkBoolean(False))
+    with pytest.raises(RuntimeError):
+        g.addRule(start, solver.mkInteger(0))
+    with pytest.raises(RuntimeError):
+        g.addRule(start, nts)
+
+    # expecting no errors
+    solver.synthFun("f", {}, boolean, g)
+
+    # expecting an error
+    with pytest.raises(RuntimeError):
+        g.addRule(start, solver.mkBoolean(False))
+
+
+def test_add_rules(solver):
+    boolean = solver.getBooleanSort()
+    integer = solver.getIntegerSort()
+
+    null_term = Term(solver)
+    start = solver.mkVar(boolean)
+    nts = solver.mkVar(boolean)
+
+    g = solver.mkSygusGrammar([], [start])
+
+    g.addRules(start, {solver.mkBoolean(False)})
+
+    #Expecting errors
+    with pytest.raises(RuntimeError):
+        g.addRules(null_term, [solver.mkBoolean(False)])
+    with pytest.raises(RuntimeError):
+        g.addRules(start, [null_term])
+    with pytest.raises(RuntimeError):
+        g.addRules(nts, [solver.mkBoolean(False)])
+    with pytest.raises(RuntimeError):
+        g.addRules(start, [solver.mkInteger(0)])
+    with pytest.raises(RuntimeError):
+        g.addRules(start, [nts])
+    #Expecting no errors
+    solver.synthFun("f", {}, boolean, g)
+
+    #Expecting an error
+    with pytest.raises(RuntimeError):
+        g.addRules(start, solver.mkBoolean(False))
+
+
+def test_add_any_constant(solver):
+    boolean = solver.getBooleanSort()
+
+    null_term = Term(solver)
+    start = solver.mkVar(boolean)
+    nts = solver.mkVar(boolean)
+
+    g = solver.mkSygusGrammar({}, {start})
+
+    g.addAnyConstant(start)
+    g.addAnyConstant(start)
+
+    with pytest.raises(RuntimeError):
+        g.addAnyConstant(null_term)
+    with pytest.raises(RuntimeError):
+        g.addAnyConstant(nts)
+
+    solver.synthFun("f", {}, boolean, g)
+
+    with pytest.raises(RuntimeError):
+        g.addAnyConstant(start)
+
+
+def test_add_any_variable(solver):
+    boolean = solver.getBooleanSort()
+
+    null_term = Term(solver)
+    x = solver.mkVar(boolean)
+    start = solver.mkVar(boolean)
+    nts = solver.mkVar(boolean)
+
+    g1 = solver.mkSygusGrammar({x}, {start})
+    g2 = solver.mkSygusGrammar({}, {start})
+
+    g1.addAnyVariable(start)
+    g1.addAnyVariable(start)
+    g2.addAnyVariable(start)
+
+    with pytest.raises(RuntimeError):
+        g1.addAnyVariable(null_term)
+    with pytest.raises(RuntimeError):
+        g1.addAnyVariable(nts)
+
+    solver.synthFun("f", {}, boolean, g1)
+
+    with pytest.raises(RuntimeError):
+        g1.addAnyVariable(start)
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 74eda63bc..15e669f02 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -1,6 +1,6 @@
 ###############################################################################
 # Top contributors (to current version):
-#   Yoni Zohar
+#   Yoni Zohar, Ying Sheng
 #
 # This file is part of the cvc5 project.
 #
@@ -17,10 +17,12 @@ import sys
 
 from pycvc5 import kinds
 
+
 @pytest.fixture
 def solver():
     return pycvc5.Solver()
 
+
 def test_recoverable_exception(solver):
     solver.setOption("produce-models", "true")
     x = solver.mkConst(solver.getBooleanSort(), "x")
@@ -28,12 +30,396 @@ def test_recoverable_exception(solver):
     with pytest.raises(RuntimeError):
         c = solver.getValue(x)
 
+
 def test_supports_floating_point(solver):
     if solver.supportsFloatingPoint():
-      try:
-          solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
-      except RuntimeError:
-          pytest.fail()
+        solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+
+
+def test_get_boolean_sort(solver):
+    solver.getBooleanSort()
+
+
+def test_get_integer_sort(solver):
+    solver.getIntegerSort()
+
+
+def test_get_real_sort(solver):
+    solver.getRealSort()
+
+
+def test_get_reg_exp_sort(solver):
+    solver.getRegExpSort()
+
+
+def test_get_string_sort(solver):
+    solver.getStringSort()
+
+
+def test_get_rounding_mode_sort(solver):
+    if solver.supportsFloatingPoint():
+        solver.getRoundingModeSort()
+    else:
+        with pytest.raises(RuntimeError):
+            solver.getRoundingModeSort()
+
+
+def test_mk_array_sort(solver):
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    bvSort = solver.mkBitVectorSort(32)
+    solver.mkArraySort(boolSort, boolSort)
+    solver.mkArraySort(intSort, intSort)
+    solver.mkArraySort(realSort, realSort)
+    solver.mkArraySort(bvSort, bvSort)
+    solver.mkArraySort(boolSort, intSort)
+    solver.mkArraySort(realSort, bvSort)
+
+    if (solver.supportsFloatingPoint()):
+        fpSort = solver.mkFloatingPointSort(3, 5)
+        solver.mkArraySort(fpSort, fpSort)
+        solver.mkArraySort(bvSort, fpSort)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkArraySort(boolSort, boolSort)
+
+
+def test_mk_bit_vector_sort(solver):
+    solver.mkBitVectorSort(32)
+    with pytest.raises(RuntimeError):
+        solver.mkBitVectorSort(0)
+
+
+def test_mk_floating_point_sort(solver):
+    if solver.supportsFloatingPoint():
+        solver.mkFloatingPointSort(4, 8)
+        with pytest.raises(RuntimeError):
+            solver.mkFloatingPointSort(0, 8)
+        with pytest.raises(RuntimeError):
+            solver.mkFloatingPointSort(4, 0)
     else:
         with pytest.raises(RuntimeError):
-          solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
+            solver.mkFloatingPointSort(4, 8)
+
+
+def test_mk_datatype_sort(solver):
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    solver.mkDatatypeSort(dtypeSpec)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSort(dtypeSpec)
+
+    throwsDtypeSpec = solver.mkDatatypeDecl("list")
+    with pytest.raises(RuntimeError):
+        solver.mkDatatypeSort(throwsDtypeSpec)
+
+
+def test_mk_datatype_sorts(solver):
+    slv = pycvc5.Solver()
+
+    dtypeSpec1 = solver.mkDatatypeDecl("list1")
+    cons1 = solver.mkDatatypeConstructorDecl("cons1")
+    cons1.addSelector("head1", solver.getIntegerSort())
+    dtypeSpec1.addConstructor(cons1)
+    nil1 = solver.mkDatatypeConstructorDecl("nil1")
+    dtypeSpec1.addConstructor(nil1)
+
+    dtypeSpec2 = solver.mkDatatypeDecl("list2")
+    cons2 = solver.mkDatatypeConstructorDecl("cons2")
+    cons2.addSelector("head2", solver.getIntegerSort())
+    dtypeSpec2.addConstructor(cons2)
+    nil2 = solver.mkDatatypeConstructorDecl("nil2")
+    dtypeSpec2.addConstructor(nil2)
+
+    decls = [dtypeSpec1, dtypeSpec2]
+    solver.mkDatatypeSorts(decls, [])
+
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSorts(decls, [])
+
+    throwsDtypeSpec = solver.mkDatatypeDecl("list")
+    throwsDecls = [throwsDtypeSpec]
+    with pytest.raises(RuntimeError):
+        solver.mkDatatypeSorts(throwsDecls, [])
+
+    # with unresolved sorts
+    unresList = solver.mkUninterpretedSort("ulist")
+    unresSorts = [unresList]
+    ulist = solver.mkDatatypeDecl("ulist")
+    ucons = solver.mkDatatypeConstructorDecl("ucons")
+    ucons.addSelector("car", unresList)
+    ucons.addSelector("cdr", unresList)
+    ulist.addConstructor(ucons)
+    unil = solver.mkDatatypeConstructorDecl("unil")
+    ulist.addConstructor(unil)
+    udecls = [ulist]
+
+    solver.mkDatatypeSorts(udecls, unresSorts)
+    with pytest.raises(RuntimeError):
+        slv.mkDatatypeSorts(udecls, unresSorts)
+
+
+def test_mk_function_sort(solver):
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+
+    # function arguments are allowed
+    solver.mkFunctionSort(funSort, solver.getIntegerSort())
+
+    # non-first-class arguments are not allowed
+    reSort = solver.getRegExpSort()
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort(reSort, solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort(solver.getIntegerSort(), funSort)
+
+    solver.mkFunctionSort([solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort()],\
+            solver.getIntegerSort())
+    funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+
+    # function arguments are allowed
+    solver.mkFunctionSort([funSort2, solver.mkUninterpretedSort("u")],\
+            solver.getIntegerSort())
+
+    with pytest.raises(RuntimeError):
+        solver.mkFunctionSort([solver.getIntegerSort(),\
+                solver.mkUninterpretedSort("u")],\
+                funSort2)
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(slv.mkUninterpretedSort("u"),\
+                solver.getIntegerSort())
+    sorts1 = [solver.getBooleanSort(),\
+            slv.getIntegerSort(),\
+            solver.getIntegerSort()]
+    sorts2 = [slv.getBooleanSort(), slv.getIntegerSort()]
+    slv.mkFunctionSort(sorts2, slv.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(sorts1, slv.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        slv.mkFunctionSort(sorts2, solver.getIntegerSort())
+
+
+def test_mk_param_sort(solver):
+    solver.mkParamSort("T")
+    solver.mkParamSort("")
+
+
+def test_mk_predicate_sort(solver):
+    solver.mkPredicateSort([solver.getIntegerSort()])
+    with pytest.raises(RuntimeError):
+        solver.mkPredicateSort([])
+
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+            solver.getIntegerSort())
+    # functions as arguments are allowed
+    solver.mkPredicateSort([solver.getIntegerSort(), funSort])
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkPredicateSort([solver.getIntegerSort()])
+
+
+def test_mk_record_sort(solver):
+    fields = [("b", solver.getBooleanSort()),\
+              ("bv", solver.mkBitVectorSort(8)),\
+              ("i", solver.getIntegerSort())]
+    empty = []
+    solver.mkRecordSort(fields)
+    solver.mkRecordSort(empty)
+    recSort = solver.mkRecordSort(fields)
+    recSort.getDatatype()
+
+
+def test_mk_set_sort(solver):
+    solver.mkSetSort(solver.getBooleanSort())
+    solver.mkSetSort(solver.getIntegerSort())
+    solver.mkSetSort(solver.mkBitVectorSort(4))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkSetSort(solver.mkBitVectorSort(4))
+
+
+def test_mk_sequence_sort(solver):
+    solver.mkSequenceSort(solver.getBooleanSort())
+    solver.mkSequenceSort(\
+            solver.mkSequenceSort(solver.getIntegerSort()))
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkSequenceSort(solver.getIntegerSort())
+
+
+def test_mk_uninterpreted_sort(solver):
+    solver.mkUninterpretedSort("u")
+    solver.mkUninterpretedSort("")
+
+
+def test_mk_sortConstructor_sort(solver):
+    solver.mkSortConstructorSort("s", 2)
+    solver.mkSortConstructorSort("", 2)
+    with pytest.raises(RuntimeError):
+        solver.mkSortConstructorSort("", 0)
+
+
+def test_mk_tuple_sort(solver):
+    solver.mkTupleSort([solver.getIntegerSort()])
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
+                                    solver.getIntegerSort())
+    with pytest.raises(RuntimeError):
+        solver.mkTupleSort([solver.getIntegerSort(), funSort])
+
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkTupleSort([solver.getIntegerSort()])
+
+
+def test_mk_var(solver):
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    funSort = solver.mkFunctionSort(intSort, boolSort)
+    solver.mkVar(boolSort)
+    solver.mkVar(funSort)
+    solver.mkVar(boolSort, "b")
+    solver.mkVar(funSort, "")
+    with pytest.raises(RuntimeError):
+        solver.mkVar(pycvc5.Sort(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkVar(pycvc5.Sort(solver), "a")
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkVar(boolSort, "x")
+
+
+def test_mk_boolean(solver):
+    solver.mkBoolean(True)
+    solver.mkBoolean(False)
+
+
+def test_mk_rounding_mode(solver):
+    if solver.supportsFloatingPoint():
+        solver.mkRoundingMode(pycvc5.RoundTowardZero)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkRoundingMode(pycvc5.RoundTowardZero)
+
+
+def test_mk_uninterpreted_const(solver):
+    solver.mkUninterpretedConst(solver.getBooleanSort(), 1)
+    with pytest.raises(RuntimeError):
+        solver.mkUninterpretedConst(pycvc5.Sort(solver), 1)
+    slv = pycvc5.Solver()
+    with pytest.raises(RuntimeError):
+        slv.mkUninterpretedConst(solver.getBooleanSort(), 1)
+
+
+def test_mk_floating_point(solver):
+    t1 = solver.mkBitVector(8)
+    t2 = solver.mkBitVector(4)
+    t3 = solver.mkInteger(2)
+    if (solver.supportsFloatingPoint()):
+        solver.mkFloatingPoint(3, 5, t1)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkFloatingPoint(3, 5, t1)
+
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(0, 5, pycvc5.Term(solver))
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(0, 5, t1)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 0, t1)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 5, t2)
+    with pytest.raises(RuntimeError):
+        solver.mkFloatingPoint(3, 5, t2)
+
+    if (solver.supportsFloatingPoint()):
+        slv = pycvc5.Solver()
+        with pytest.raises(RuntimeError):
+            slv.mkFloatingPoint(3, 5, t1)
+
+
+def test_mk_empty_set(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkSetSort(solver.getBooleanSort())
+    solver.mkEmptySet(pycvc5.Sort(solver))
+    solver.mkEmptySet(s)
+    with pytest.raises(RuntimeError):
+        solver.mkEmptySet(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptySet(s)
+
+
+def test_mk_empty_sequence(solver):
+    slv = pycvc5.Solver()
+    s = solver.mkSequenceSort(solver.getBooleanSort())
+    solver.mkEmptySequence(s)
+    solver.mkEmptySequence(solver.getBooleanSort())
+    with pytest.raises(RuntimeError):
+        slv.mkEmptySequence(s)
+
+
+def test_mk_false(solver):
+    solver.mkFalse()
+    solver.mkFalse()
+
+
+def test_mk_nan(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkNaN(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkNaN(3, 5)
+
+
+def test_mk_neg_zero(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkNegZero(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkNegZero(3, 5)
+
+
+def test_mk_neg_inf(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkNegInf(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkNegInf(3, 5)
+
+
+def test_mk_pos_inf(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkPosInf(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkPosInf(3, 5)
+
+
+def test_mk_pos_zero(solver):
+    if (solver.supportsFloatingPoint()):
+        solver.mkPosZero(3, 5)
+    else:
+        with pytest.raises(RuntimeError):
+            solver.mkPosZero(3, 5)
+
+
+def test_mk_pi(solver):
+    solver.mkPi()