6 files changed, 149 insertions, 5 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 893ea5c95..6168a8e22 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -86,3 +86,8 @@ if(TARGET CVC4::cvc4jar)
 
   add_subdirectory(api/java)
 endif()
+
+if(CVC4_BINDINGS_PYTHON)
+  # If legacy Python API has been built
+  add_subdirectory(api/python)
+endif()
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 5550974c9..50c52868b 100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -16,11 +16,9 @@
 ### A simple demonstration of the Python interface.  Compare to the
 ### C++ interface in simple_vc_cxx.cpp; they are quite similar.
 ###
-### To run, use something like:
+### To run from a build directory, use something like:
 ###
-###   ln -s ../builds/src/bindings/python/CVC4.py CVC4.py
-###   ln -s ../builds/src/bindings/python/.libs/CVC4.so _CVC4.so
-###   ./SimpleVC.py
+###   PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py
 ####
 
 import CVC4
@@ -61,4 +59,3 @@ def main():
 
 if __name__ == '__main__':
   sys.exit(main())
-
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 108ae3cd3..31f62db56 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -5,6 +5,7 @@ set(EXAMPLES_API_JAVA
   #CVC4Streams
   Combination
   Datatypes
+  Exceptions
   FloatingPointArith
   HelloWorld
   LinearArith
diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java
new file mode 100644
index 000000000..d3ddb85cc
--- /dev/null
+++ b/examples/api/java/Exceptions.java
@@ -0,0 +1,56 @@
+/*********************                                                        */
+/*! \file Exceptions.java
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief Catching CVC4 exceptions via the Java API.
+ **
+ ** A simple demonstration of catching CVC4 execptions via the Java API.
+ **/
+
+import edu.stanford.CVC4.*;
+
+public class Exceptions {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
+
+    ExprManager em = new ExprManager();
+    SmtEngine smt = new SmtEngine(em);
+
+    smt.setOption("produce-models", new SExpr(true));
+
+    // Setting an invalid option
+    try {
+      smt.setOption("non-existing", new SExpr(true));
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Creating a term with an invalid type
+    try {
+      Type integer = em.integerType();
+      Expr x = em.mkVar("x", integer);
+      Expr invalidExpr = em.mkExpr(Kind.AND, x, x);
+      smt.checkSat(invalidExpr);
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+
+    // Asking for a model after unsat result
+    try {
+      smt.checkSat(em.mkConst(false));
+      smt.getModel();
+      System.exit(1);
+    } catch (edu.stanford.CVC4.Exception e) {
+      System.out.println(e.toString());
+    }
+  }
+}
diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt
new file mode 100644
index 000000000..6e255c5b1
--- /dev/null
+++ b/examples/api/python/CMakeLists.txt
@@ -0,0 +1,27 @@
+set(EXAMPLES_API_PYTHON
+  exceptions
+)
+
+find_package(PythonInterp REQUIRED)
+
+# Find Python bindings in the corresponding python-*/site-packages directory.
+# Lookup Python module directory and store path in PYTHON_MODULE_PATH.
+execute_process(COMMAND
+                  ${PYTHON_EXECUTABLE} -c
+                    "from distutils.sysconfig import get_python_lib;\
+                     print(get_python_lib(plat_specific=True,\
+                             prefix='${CMAKE_PREFIX_PATH}/../..'))"
+                OUTPUT_VARIABLE PYTHON_MODULE_PATH
+                OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+foreach(example ${EXAMPLES_API_PYTHON})
+  set(example_test example/api/python/${example})
+  add_test(
+    NAME ${example_test}
+    COMMAND
+      "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/api/python/${example}.py"
+  )
+  set_tests_properties(${example_test} PROPERTIES
+    LABELS "example"
+    ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH})
+endforeach()
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
new file mode 100644
index 000000000..780f75bf7
--- /dev/null
+++ b/examples/api/python/exceptions.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python
+
+#####################
+## \file exceptions.py
+## \verbatim
+## Top contributors (to current version):
+##   Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.\endverbatim
+##
+## \brief Catching CVC4 exceptions with the legacy Python API.
+##
+## A simple demonstration of catching CVC4 execptions with the legacy Python
+## API.
+
+import CVC4
+import sys
+
+
+def main():
+    em = CVC4.ExprManager()
+    smt = CVC4.SmtEngine(em)
+
+    smt.setOption("produce-models", CVC4.SExpr("true"))
+
+    # Setting an invalid option
+    try:
+        smt.setOption("non-existing", CVC4.SExpr("true"))
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Creating a term with an invalid type
+    try:
+        integer = em.integerType()
+        x = em.mkVar("x", integer)
+        invalidExpr = em.mkExpr(CVC4.AND, x, x)
+        smt.checkSat(invalidExpr)
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    # Asking for a model after unsat result
+    try:
+        smt.checkSat(em.mkBoolConst(False))
+        smt.getModel()
+        return 1
+    except CVC4.Exception as e:
+        print(e.toString())
+
+    return 0
+
+
+if __name__ == '__main__':
+    sys.exit(main())