3 files changed, 80 insertions, 0 deletions
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt
new file mode 100644
index 000000000..675f6a7c5
--- /dev/null
+++ b/test/python/CMakeLists.txt
@@ -0,0 +1,44 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Makai Mann and Yoni Zohar
+## This file is part of the CVC4 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.
+##
+#-----------------------------------------------------------------------------#
+# Add Python bindings API tests
+
+# Check if the pytest Python module is installed.
+execute_process(
+  COMMAND
+  ${PYTHON_EXECUTABLE} -c "import pytest"
+  RESULT_VARIABLE
+    RET_PYTEST
+  ERROR_QUIET
+)
+
+if(RET_PYTEST)
+  message(FATAL_ERROR
+      "Could not find pytest for Python "
+      "version ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR}. "
+      "Make sure to install pytest for this Python version "
+      "via \n`${PYTHON_EXECUTABLE} -m pip install pytest'.\nNote: You need to "
+      "have pip installed for this Python version.")
+endif()
+
+macro(cvc4_add_python_api_test name filename)
+
+  #   we create test target 'python/unit/api/myapitest'
+  #   and run it with 'ctest -R "python/unit/api/myapitest"'.
+  add_test (NAME python/unit/api/${name}
+    COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename}
+    # directory for importing the python bindings
+    WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python)
+
+endmacro()
+
+# add specific test files
+cvc4_add_python_api_test(pytest_solver unit/api/test_solver.py)
diff --git a/test/python/unit/api/__init__.py b/test/python/unit/api/__init__.py
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/python/unit/api/__init__.py
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
new file mode 100644
index 000000000..4ab0427c1
--- /dev/null
+++ b/test/python/unit/api/test_solver.py
@@ -0,0 +1,36 @@
+#####################
+## test_solver.py
+## Top contributors (to current version):
+##   Yoni Zohar
+## This file is part of the CVC4 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.
+##
+import pytest
+import pycvc4
+import sys
+
+from pycvc4 import kinds
+
+@pytest.fixture
+def solver():
+    return pycvc4.Solver()
+
+def test_recoverable_exception(solver):
+    solver.setOption("produce-models", "true")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x).notTerm())
+    with pytest.raises(RuntimeError):
+        c = solver.getValue(x)
+
+def test_supports_floating_point(solver):
+    if solver.supportsFloatingPoint():
+      try:
+          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+      except RuntimeError:
+          pytest.fail()
+    else:
+        with pytest.raises(RuntimeError):
+          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)