1 files changed, 58 insertions, 0 deletions
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())