Exception Handling
examples/api/cpp/exceptions.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Catching cvc5 exceptions via the C++ API.
11 *
12 * A simple demonstration of catching cvc5 exceptions via the C++ API.
13 */
14
15#include <cvc5/cvc5.h>
16
17#include <iostream>
18
19int main()
20{
21 cvc5::TermManager tm;
22 cvc5::Solver solver(tm);
23
24 solver.setOption("produce-models", "true");
25
26 // Setting an invalid option
27 try
28 {
29 solver.setOption("non-existing", "true");
30 return 1;
31 }
32 catch (const std::exception& e)
33 {
34 std::cout << e.what() << std::endl;
35 }
36
37 // Creating a term with an invalid type
38 try
39 {
40 cvc5::Sort integer = tm.getIntegerSort();
41 cvc5::Term x = tm.mkVar(integer, "x");
42 cvc5::Term invalidTerm = tm.mkTerm(cvc5::Kind::AND, {x, x});
43 solver.checkSatAssuming(invalidTerm);
44 return 1;
45 }
46 catch (const std::exception& e)
47 {
48 std::cout << e.what() << std::endl;
49 }
50
51 // Asking for a model after unsat result
52 try
53 {
54 solver.checkSatAssuming(tm.mkBoolean(false));
55 solver.getModel({}, {});
56 return 1;
57 }
58 catch (const std::exception& e)
59 {
60 std::cout << e.what() << std::endl;
61 }
62
63 return 0;
64}
examples/api/java/Exceptions.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Catching cvc5 exceptions via the Java API.
11 *
12 * A simple demonstration of catching cvc5 execptions via the Java API.
13 */
14
15import io.github.cvc5.*;
16
17public class Exceptions
18{
19 public static void main(String[] args)
20 {
21 TermManager tm = new TermManager();
22 Solver solver = new Solver(tm);
23 {
24 solver.setOption("produce-models", "true");
25
26 // Setting an invalid option
27 try
28 {
29 solver.setOption("non-existing", "true");
30 System.exit(1);
31 }
32 catch (Exception e)
33 {
34 System.out.println(e.toString());
35 }
36
37 // Creating a term with an invalid type
38 try
39 {
40 Sort integer = tm.getIntegerSort();
41 Term x = tm.mkVar(integer, "x");
42 Term invalidTerm = tm.mkTerm(Kind.AND, x, x);
43 solver.checkSatAssuming(invalidTerm);
44 System.exit(1);
45 }
46 catch (Exception e)
47 {
48 System.out.println(e.toString());
49 }
50
51 // Asking for a model after unsat result
52 try
53 {
54 solver.checkSatAssuming(tm.mkBoolean(false));
55 solver.getModel(new Sort[] {}, new Term[] {});
56 System.exit(1);
57 }
58 catch (Exception e)
59 {
60 System.out.println(e.toString());
61 }
62 }
63 Context.deletePointers();
64 }
65}
examples/api/python/exceptions.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# Catching cvc5 exceptions with the legacy Python API.
12#
13# A simple demonstration of catching cvc5 exceptions with the legacy Python API.
14##
15
16import cvc5
17from cvc5 import Kind
18import sys
19
20
21def main():
22 tm = cvc5.TermManager()
23 slv = cvc5.Solver(tm)
24
25 slv.setOption("produce-models", "true")
26
27 # Setting an invalid option
28 try:
29 slv.setOption("non-existing", "true")
30 return 1
31 except:
32 pass
33
34 # Creating a term with an invalid type
35 try:
36 integer = tm.getIntegerSort()
37 x = tm.mkConst("x", integer)
38 invalidTerm = em.mkTerm(AND, x, x)
39 slv.checkSat(invalidTerm)
40 return 1
41 except:
42 pass
43
44 # Asking for a model after unsat result
45 try:
46 slv.checkSat(tm.mkBoolean(False))
47 slv.getModel()
48 return 1
49 except:
50 pass
51
52 return 0
53
54
55if __name__ == '__main__':
56 sys.exit(main())
cvc5_pythonic_api:/test/pgms/example_exceptions.py
1from cvc5_pythonic_api import *
2
3if __name__ == '__main__':
4 s = Solver()
5 s.set("produce-models", True)
6 try:
7 # invalid option
8 s.set("non-existing-option", True)
9 except:
10 pass
11
12 try:
13 # type error
14 Int("x") + BitVec("a", 5)
15 except:
16 pass
17
18 s += BoolVal(False)
19 s.check()
20 try:
21 s.model()
22 except:
23 pass